let g1, g2 be Ordinal-Sequence-valued Sequence; :: thesis: ( dom g1 = On U & g1 . 0 = U exp omega & ( for b being Ordinal 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 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
A14: dom g1 = On U and
A15: g1 . 0 = U exp omega and
A16: for b being Ordinal st succ b in On U holds
g1 . (succ b) = criticals (g1 . b) and
A17: for l being limit_ordinal non empty Ordinal st l in On U holds
g1 . l = criticals (g1 | l) and
A18: dom g2 = On U and
A19: g2 . 0 = U exp omega and
A20: for b being Ordinal st succ b in On U holds
g2 . (succ b) = criticals (g2 . b) and
A21: for l being limit_ordinal non empty Ordinal st l in On U holds
g2 . l = criticals (g2 | l) ; :: thesis: g1 = g2
deffunc H₁( set , Ordinal-Sequence) -> Ordinal-Sequence = criticals $2;
deffunc H₂( set , Ordinal-Sequence-valued Sequence) -> Ordinal-Sequence = criticals $2;
A22: ( 0 in On U implies g1 . 0 = U exp omega ) by A15;
A23: for b being Ordinal st succ b in On U holds
g1 . (succ b) = H₁(b,g1 . b) by A16;
A24: for a being Ordinal st a in On U & a <> 0 & a is limit_ordinal holds
g1 . a = H₂(a,g1 | a) by A17;
A25: ( 0 in On U implies g2 . 0 = U exp omega ) by A19;
A26: for b being Ordinal st succ b in On U holds
g2 . (succ b) = H₁(b,g2 . b) by A20;
A27: for a being Ordinal st a in On U & a <> 0 & a is limit_ordinal holds
g2 . a = H₂(a,g2 | a) by A21;
thus g1 = g2 from ORDINAL2:sch 4(A14, A22, A23, A24, A18, A25, A26, A27); :: thesis: verum