deffunc H₁( set , set ) -> set = 0 ;
consider L being Sequence such that
A1: dom L = omega and
A2: ( 0 in omega implies L . 0 = F₁() ) and
A3: for A being Ordinal st succ A in omega holds
L . (succ A) = F₂(A,(L . A)) and
for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds
L . A = H₁(A,L | A) from ORDINAL2:sch 5();
take L ; :: thesis: ( dom L = omega & L . 0 = F₁() & ( for n being Nat holds L . (succ n) = F₂(n,(L . n)) ) )
thus dom L = omega by A1; :: thesis: ( L . 0 = F₁() & ( for n being Nat holds L . (succ n) = F₂(n,(L . n)) ) )
0 in omega by ORDINAL1:def 12;
hence L . 0 = F₁() by A2; :: thesis: for n being Nat holds L . (succ n) = F₂(n,(L . n))
let n be Nat; :: thesis: L . (succ n) = F₂(n,(L . n))
succ n in omega by ORDINAL1:def 12;
hence L . (succ n) = F₂(n,(L . n)) by A3; :: thesis: verum