deffunc H₁( set , set ) -> set = {} ;
consider L being T-Sequence such that
A1: dom L = NAT and
A2: ( {} in NAT implies L . {} = 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 <> {} & 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))
succ n in NAT ;
hence L . (n + 1) = F₂(n,(L . n)) by A3; :: thesis: verum