deffunc H₁( set , set ) -> set = {} ;
consider L being T-Sequence such that
A1: dom L = omega and
A2: ( {} in omega implies L . {} = 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 <> {} & A is limit_ordinal holds
L . A = H₁(A,L | A) from ORDINAL2:sch 5();
take L ; :: thesis: ( dom L = omega & L . {} = F₁() & ( for n being natural number holds L . (succ n) = F₂(n,(L . n)) ) )
thus dom L = omega by A1; :: thesis: ( L . {} = F₁() & ( for n being natural number holds L . (succ n) = F₂(n,(L . n)) ) )
{} in omega by ORDINAL1:def 12;
hence L . {} = F₁() by A2; :: thesis: for n being natural number holds L . (succ n) = F₂(n,(L . n))
let n be natural number ; :: 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