let g1, g2 be Ordinal-Sequence-valued T-Sequence; ( dom g1 = On U & g1 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
g1 . (succ b) = criticals (g1 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
g1 . l = criticals (g1 | l) ) & dom g2 = On U & g2 . 0 = U exp omega & ( for b being ordinal number st succ b in On U holds
g2 . (succ b) = criticals (g2 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
g2 . l = criticals (g2 | l) ) implies g1 = g2 )
assume that
01:
dom g1 = On U
and
A1:
g1 . 0 = U exp omega
and
B1:
for b being ordinal number st succ b in On U holds
g1 . (succ b) = criticals (g1 . b)
and
C1:
for l being limit_ordinal non empty Ordinal st l in On U holds
g1 . l = criticals (g1 | l)
and
05:
dom g2 = On U
and
A2:
g2 . 0 = U exp omega
and
B2:
for b being ordinal number st succ b in On U holds
g2 . (succ b) = criticals (g2 . b)
and
C2:
for l being limit_ordinal non empty Ordinal st l in On U holds
g2 . l = criticals (g2 | l)
; g1 = g2
deffunc H1( set , Ordinal-Sequence) -> Ordinal-Sequence = criticals $2;
deffunc H2( set , Ordinal-Sequence-valued T-Sequence) -> Ordinal-Sequence = criticals $2;
02:
( {} in On U implies g1 . {} = U exp omega )
by A1;
03:
for b being ordinal number st succ b in On U holds
g1 . (succ b) = H1(b,g1 . b)
by B1;
04:
for a being ordinal number st a in On U & a <> {} & a is limit_ordinal holds
g1 . a = H2(a,g1 | a)
by C1;
06:
( {} in On U implies g2 . {} = U exp omega )
by A2;
07:
for b being ordinal number st succ b in On U holds
g2 . (succ b) = H1(b,g2 . b)
by B2;
08:
for a being ordinal number st a in On U & a <> {} & a is limit_ordinal holds
g2 . a = H2(a,g2 | a)
by C2;
thus
g1 = g2
from ORDINAL2:sch 4(01, 02, 03, 04, 05, 06, 07, 08); verum