deffunc H₁( Ordinal, set ) -> object = [{$2},{}];
deffunc H₂( Ordinal, Sequence) -> object = [(rng $2),{}];
consider L being Sequence such that
A1: dom L = succ A and
A2: ( 0 in succ A implies L . 0 = 0_No ) and
A3: for A1 being Ordinal st succ A1 in succ A holds
L . (succ A1) = H₁(A1,L . A1) and
A4: for A1 being Ordinal st A1 in succ A & A1 <> 0 & A1 is limit_ordinal holds
L . A1 = H₂(A1,L | A1) from ORDINAL2:sch 5();
take L . A ; :: thesis: ex S being Sequence st
( L . A = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) )
take L ; :: thesis: ( L . A = L . A & dom L = succ A & ( for O being Ordinal st succ O in succ A holds
L . (succ O) = [{(L . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
L . O = [(rng (L | O)),{}] ) )
thus ( L . A = L . A & dom L = succ A & ( for O being Ordinal st succ O in succ A holds
L . (succ O) = [{(L . O)},{}] ) ) by A1, A3; :: thesis: for O being Ordinal st O in succ A & O is limit_ordinal holds
L . O = [(rng (L | O)),{}]
let O be Ordinal; :: thesis: ( O in succ A & O is limit_ordinal implies L . O = [(rng (L | O)),{}] )
assume A5: ( O in succ A & O is limit_ordinal ) ; :: thesis: L . O = [(rng (L | O)),{}]

per cases ( O = 0 or O <> 0 ) ;

suppose O = 0 ; :: thesis: L . O = [(rng (L | O)),{}]

hence L . O = [(rng (L | O)),{}] by A2, A5; :: thesis: verum

end;

suppose O <> 0 ; :: thesis: L . O = [(rng (L | O)),{}]

hence L . O = [(rng (L | O)),{}] by A5, A4; :: thesis: verum

end;

end;