--- a/cardinal.agda	Wed Aug 21 16:43:29 2019 +0900
+++ b/cardinal.agda	Thu Aug 22 12:41:41 2019 +0900
@@ -94,8 +94,12 @@
 
 func→od∈Func :  (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom 
 func→od∈Func f dom  = record { proj1 = {!!} ; proj2 = {!!} } where
-   lemma :  (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom 
-   lemma = {!!} -- func→od∈Func-1 ( od→func {dom} {{!!}} {od→ord (func→od f {!!} )} {!!} )
+   f<F :  def (Func dom (Ord (sup-o (λ x → f x)))) (od→ord (func→od f dom))
+   f<F = {!!}
+   odfunc : Func←cd {dom} f<F
+   odfunc = ( od→func {dom} {Ord (sup-o (λ x → f x))} {od→ord (func→od f dom)} f<F )
+   lemma :  Func dom (Ord (sup-o ( func-1 odfunc ) )) ∋  func→od (func-1 odfunc ) dom
+   lemma = func→od∈Func-1 odfunc
 
 -- contra position of sup-o<
 --