reconsider o = omega as non trivial Ordinal ;
deffunc H₁( set , set ) -> Ordinal-Sequence = criticals (OS@ $2);
deffunc H₂( set , set ) -> Ordinal-Sequence = criticals (OSV@ $2);
consider L being T-Sequence such that
A1: dom L = On U and
A2: ( {} in On U implies L . {} = U exp o ) and
A3: for b being ordinal number st succ b in On U holds
L . (succ b) = H₁(b,L . b) and
A4: for b being ordinal number st b in On U & b <> {} & b is limit_ordinal holds
L . b = H₂(b,L | b) from ORDINAL2:sch 5();
defpred S₁[ Ordinal] means ( $1 in On U implies L . $1 is Ordinal-Sequence );
00: S₁[ {} ] by A2;
01: for b being ordinal number st S₁[b] holds
S₁[ succ b]

proof

let b be ordinal number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume that
B1: S₁[b] and
B2: succ b in On U ; :: thesis: L . (succ b) is Ordinal-Sequence
b in succ b by ORDINAL1:6;
then reconsider f = L . b as Ordinal-Sequence by B1, B2, ORDINAL1:10;
L . (succ b) = H₁(b,f) by A3, B2
.= criticals f by OSc ;
hence L . (succ b) is Ordinal-Sequence ; :: thesis: verum

end;

02: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) implies S₁[b] )
assume that
C1: ( b <> {} & b is limit_ordinal ) and
for c being ordinal number st c in b holds
S₁[c] and
C3: b in On U ; :: thesis: L . b is Ordinal-Sequence
L . b = H₂(b,L | b) by A4, C1, C3;
hence L . b is Ordinal-Sequence ; :: thesis: verum

end;

03: for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(00, 01, 02);
L is Ordinal-Sequence-valued

proof

let x be set ; :: according to ORDINAL6:def 9 :: thesis: ( x in rng L implies x is Ordinal-Sequence )
assume x in rng L ; :: thesis: x is Ordinal-Sequence
then ex y being set st
( y in dom L & x = L . y ) by FUNCT_1:def 3;
hence x is Ordinal-Sequence by A1, 03; :: thesis: verum

end;

then reconsider L = L as Ordinal-Sequence-valued T-Sequence ;
take L ; :: thesis: ( dom L = On U & L . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
L . (succ b) = criticals (L . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
L . l = criticals (L | l) ) )
0-element_of U in On U by ORDINAL1:def 9;
hence ( dom L = On U & L . 0 = U exp omega ) by A1, A2; :: thesis: ( ( for b being ordinal number st succ b in On U holds
L . (succ b) = criticals (L . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
L . l = criticals (L | l) ) )

hereby :: thesis: for l being limit_ordinal non empty Ordinal st l in On U holds
L . l = criticals (L | l)

let b be ordinal number ; :: thesis: ( succ b in On U implies L . (succ b) = criticals (L . b) )
assume E1: succ b in On U ; :: thesis: L . (succ b) = criticals (L . b)
reconsider f = L . b as Ordinal-Sequence ;
thus L . (succ b) = H₁(b,f) by E1, A3
.= criticals (L . b) by OSc ; :: thesis: verum

end;

let l be limit_ordinal non empty Ordinal; :: thesis: ( l in On U implies L . l = criticals (L | l) )
assume l in On U ; :: thesis: L . l = criticals (L | l)
hence L . l = H₂(l,L | l) by A4
.= criticals (L | l) by OSVc ;
:: thesis: verum