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: S₁[ {} ]

proof

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

end;

A2: 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
A3: ( A c= B implies ex C being Ordinal st B = A +^ C ) and
A4: A c= succ B ; :: thesis: ex C being Ordinal st succ B = A +^ C
A5: ( A = succ B implies succ B = A +^ {} ) by ORDINAL2:44;

now

assume A <> succ B ; :: thesis: ex C being Ordinal st succ B = A +^ C
then A c< succ B by A4, XBOOLE_0:def 8;
then A in succ B by ORDINAL1:21;
then consider C being Ordinal such that
A6: B = A +^ C by A3, ORDINAL1:34;
succ B = A +^ (succ C) by A6, ORDINAL2:45;
hence ex C being Ordinal st succ B = A +^ C ; :: thesis: verum

end;

hence ex C being Ordinal st succ B = A +^ C by A5; :: thesis: verum

end;

A7: for B being Ordinal st B <> {} & 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 <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₁[C] ) implies S₁[B] )
assume that
A8: ( B <> {} & 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
A9: A c= B ; :: thesis: ex C being Ordinal st B = A +^ C
defpred S₂[ Ordinal] means B c= A +^ $1;
{} c= A by XBOOLE_1:2;
then ( {} +^ B c= A +^ B & B = {} +^ B ) by ORDINAL2:47, ORDINAL2:51;
then A10: ex C being Ordinal st S₂[C] ;
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);
deffunc H₁( Ordinal) -> set = A +^ $1;
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

assume C = {} ; :: thesis: B = A +^ {}
then A +^ C = A by ORDINAL2:44;
hence B = A by A9, A11, XBOOLE_0:def 10
.= A +^ {} by ORDINAL2:44 ;
:: thesis: verum

end;

now

assume A14: C <> {} ; :: thesis: ex C being Ordinal st B = A +^ C
C is limit_ordinal

proof

assume not C is limit_ordinal ; :: thesis: contradiction
then consider D being Ordinal such that
A15: C = succ D by ORDINAL1:42;
not C c= D by A15, ORDINAL1:7, ORDINAL1:10;
then A +^ D in B by A11, ORDINAL1:26;
then ( succ (A +^ D) = A +^ (succ D) & succ (A +^ D) c= B ) by ORDINAL1:33, ORDINAL2:45;
then B = succ (A +^ D) by A11, A15, XBOOLE_0:def 10;
hence contradiction by A8, ORDINAL1:42; :: thesis: verum

end;

then A16: A +^ C = sup L by A12, A14, ORDINAL2:46
.= sup (rng L) ;
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 set such that
A17: ( y in dom L & D = L . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A17;
( L . y = A +^ y & not C c= y ) by A12, A17, ORDINAL1:7;
hence D in B by A11, A17, ORDINAL1:26; :: thesis: verum

end;

then sup (rng L) c= B by ORDINAL2:28;
then B = A +^ C by A11, A16, XBOOLE_0:def 10;
hence ex C being Ordinal st B = A +^ C ; :: thesis: verum

end;

hence ex C being Ordinal st B = A +^ C by A13; :: thesis: verum

end;

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