let A, B be Ordinal; :: thesis: ( A c= B implies ex C being Ordinal st B = A +^ C )
defpred S1[ Ordinal] means ( A c= $1 implies ex C being Ordinal st $1 = A +^ C );
A1: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; :: thesis: ( S1[B] implies S1[ 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
S1[C] ) holds
S1[B]
proof
deffunc H1( Ordinal) -> set = A +^ $1;
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[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 S2[ 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 S2[C] by A9;
consider C being Ordinal such that
A11: ( S2[C] & ( for D being Ordinal st S2[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 = H1(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 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: S1[ 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 S1[B] from ORDINAL2:sch 1(A21, A1, A6);
 hence ( A c= B implies ex C being Ordinal st B = A +^ C ) ; :: thesis: verum