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 Sequence such that
A1: dom L = On U and
A2: ( 0 in On U implies L . 0 = U exp o ) and
A3: for b being Ordinal st succ b in On U holds
L . (succ b) = H₁(b,L . b) and
A4: for b being Ordinal st b in On U & b <> 0 & 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 );
A5: S₁[ 0 ] by A2;
A6: for b being Ordinal st S₁[b] holds
S₁[ succ b]

proof

let b be Ordinal; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume that
A7: S₁[b] and
A8: 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 A7, A8, ORDINAL1:10;
L . (succ b) = H₁(b,f) by A3, A8
.= criticals f by Def13 ;
hence L . (succ b) is Ordinal-Sequence ; :: thesis: verum

end;

A9: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) holds
S₁[b]

proof

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

end;

A12: for b being Ordinal holds S₁[b] from ORDINAL2:sch 1(A5, A6, A9);
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 object st
( y in dom L & x = L . y ) by FUNCT_1:def 3;
hence x is Ordinal-Sequence by A1, A12; :: thesis: verum

end;

then reconsider L = L as Ordinal-Sequence-valued Sequence ;
take L ; :: thesis: ( dom L = On U & L . 0 = U exp omega & ( for b being Ordinal 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 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; :: thesis: ( succ b in On U implies L . (succ b) = criticals (L . b) )
assume A13: 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 A13, A3
.= criticals (L . b) by Def13 ; :: 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 Def14 ;
:: thesis: verum