let A, B be Ordinal; :: thesis: ( A c= B implies ex C being Ordinal st B = A +^ C )
defpred S₁[ Ordinal] means ( A c= $1 implies ex C being Ordinal st $1 = A +^ C );
A1: 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
A2: ( A c= B implies ex C being Ordinal st B = A +^ C ) and
A3: A c= succ B ; :: thesis: ex C being Ordinal st succ B = A +^ C

A4: now :: thesis: ( A <> succ B implies ex C being Ordinal st succ B = A +^ C )

assume A <> succ B ; :: thesis: ex C being Ordinal st succ B = A +^ C
then A c< succ B by A3;
then A in succ B by ORDINAL1:11;
then consider C being Ordinal such that
A5: B = A +^ C by A2, ORDINAL1:22;
succ B = A +^ (succ C) by A5, ORDINAL2:28;
hence ex C being Ordinal st succ B = A +^ C ; :: thesis: verum

end;

( A = succ B implies succ B = A +^ {} ) by ORDINAL2:27;
hence ex C being Ordinal st succ B = A +^ C by A4; :: thesis: verum

end;

A6: 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

deffunc H₁( Ordinal) -> set = A +^ $1;
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
B <> 0 and
A7: B is limit_ordinal and
for C being Ordinal st C in B & A c= C holds
ex D being Ordinal st C = A +^ D and
A8: A c= B ; :: thesis: ex C being Ordinal st B = A +^ C
defpred S₂[ Ordinal] means B c= A +^ $1;
A9: B = {} +^ B by ORDINAL2:30;
{} +^ B c= A +^ B by ORDINAL2:34, XBOOLE_1:2;
then A10: ex C being Ordinal st S₂[C] by A9;
consider C being Ordinal such that
A11: ( S₂[C] & ( for D being Ordinal st S₂[D] holds
C c= D ) ) from ORDINAL1:sch 1(A10);
consider L being Ordinal-Sequence such that
A12: ( dom L = C & ( for D being Ordinal st D in C holds
L . D = H₁(D) ) ) from ORDINAL2:sch 3();

A13: now :: thesis: ( C <> {} implies ex C being Ordinal st B = A +^ C )

for D being Ordinal st D in rng L holds
D in B

proof

let D be Ordinal; :: thesis: ( D in rng L implies D in B )
assume D in rng L ; :: thesis: D in B
then consider y being object such that
A14: y in dom L and
A15: D = L . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A14;
A16: not C c= y by A12, A14, ORDINAL1:5;
L . y = A +^ y by A12, A14;
hence D in B by A11, A15, A16, ORDINAL1:16; :: thesis: verum

end;

then A17: sup (rng L) c= B by ORDINAL2:20;
A18: C is limit_ordinal

proof

assume not C is limit_ordinal ; :: thesis: contradiction
then consider D being Ordinal such that
A19: C = succ D by ORDINAL1:29;
not C c= D by A19, ORDINAL1:5, ORDINAL1:6;
then A +^ D in B by A11, ORDINAL1:16;
then A20: succ (A +^ D) c= B by ORDINAL1:21;
succ (A +^ D) = A +^ (succ D) by ORDINAL2:28;
then B = succ (A +^ D) by A11, A19, A20;
hence contradiction by A7, ORDINAL1:29; :: thesis: verum

end;

assume C <> {} ; :: thesis: ex C being Ordinal st B = A +^ C
then A +^ C = sup L by A12, A18, ORDINAL2:29
.= sup (rng L) ;
then B = A +^ C by A11, A17;
hence ex C being Ordinal st B = A +^ C ; :: thesis: verum

end;

( C = {} implies B = A +^ {} ) by A8, A11, ORDINAL2:27;
hence ex C being Ordinal st B = A +^ C by A13; :: thesis: verum

end;

A21: S₁[ 0 ]

proof

assume A c= 0 ; :: thesis: ex C being Ordinal st 0 = A +^ C
then A = {} by XBOOLE_1:3;
then {} = A +^ {} by ORDINAL2:30;
hence ex C being Ordinal st 0 = A +^ C ; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A21, A1, A6);
hence ( A c= B implies ex C being Ordinal st B = A +^ C ) ; :: thesis: verum