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