let A, B be Ordinal; :: thesis: ( A <> {} implies ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A ) )
assume A1: A <> {} ; :: thesis: ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )
defpred S₁[ Ordinal] means ex C, D being Ordinal st
( $1 = (C *^ A) +^ D & D in A );
A2: S₁[ {} ]

proof

take C = {} ; :: thesis: ex D being Ordinal st
( {} = (C *^ A) +^ D & D in A )
take D = {} ; :: thesis: ( {} = (C *^ A) +^ D & D in A )
thus {} = {} +^ {} by ORDINAL2:44
.= (C *^ A) +^ D by ORDINAL2:52 ; :: thesis: D in A
thus D in A by A1, Th10; :: thesis: verum

end;

A3: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
given C, D being Ordinal such that A4: ( B = (C *^ A) +^ D & D in A ) ; :: thesis: S₁[ succ B]

A5: now

assume A6: succ D in A ; :: thesis: ex C1 being Ordinal ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
take C1 = C; :: thesis: ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
take D1 = succ D; :: thesis: ( (C1 *^ A) +^ D1 = succ B & D1 in A )
thus (C1 *^ A) +^ D1 = succ B by A4, ORDINAL2:45; :: thesis: D1 in A
thus D1 in A by A6; :: thesis: verum

end;

now

assume not succ D in A ; :: thesis: ex C1 being set ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
then ( A c= succ D & succ D c= A ) by A4, ORDINAL1:26, ORDINAL1:33;
then A7: A = succ D by XBOOLE_0:def 10;
take C1 = succ C; :: thesis: ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
take D1 = {} ; :: thesis: ( (C1 *^ A) +^ D1 = succ B & D1 in A )
thus (C1 *^ A) +^ D1 = C1 *^ A by ORDINAL2:44
.= (C *^ A) +^ A by ORDINAL2:53
.= succ B by A4, A7, ORDINAL2:45 ; :: thesis: D1 in A
thus D1 in A by A1, Th10; :: thesis: verum

end;

hence S₁[ succ B] by A5; :: thesis: verum

end;

A8: for B being Ordinal st B <> {} & B is limit_ordinal & ( for A being Ordinal st A in B holds
S₁[A] ) holds
S₁[B]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for A being Ordinal st A in B holds
S₁[A] ) implies S₁[B] )
assume A9: ( B <> {} & B is limit_ordinal & ( for A being Ordinal st A in B holds
S₁[A] ) ) ; :: thesis: S₁[B]
{} in A by A1, Th10;
then ( succ {} c= A & B *^ 1 = B ) by ORDINAL1:33, ORDINAL2:56;
then A10: B c= B *^ A by ORDINAL2:59;
A11: ( B = B *^ A implies ( B = (B *^ A) +^ {} & {} in A ) ) by A1, Th10, ORDINAL2:44;
defpred S₂[ Ordinal] means ( $1 in B & B in $1 *^ A );

now

assume B <> B *^ A ; :: thesis: S₁[B]
then B c< B *^ A by A10, XBOOLE_0:def 8;
then B in B *^ A by ORDINAL1:21;
then A12: ex C being Ordinal st S₂[C] by A9, Th49;
consider C being Ordinal such that
A13: S₂[C] and
A14: for C1 being Ordinal st S₂[C1] holds
C c= C1 from ORDINAL1:sch 1(A12);

now

assume C is limit_ordinal ; :: thesis: contradiction
then consider C1 being Ordinal such that
A15: ( C1 in C & B in C1 *^ A ) by A13, Th49;
C1 in B by A13, A15, ORDINAL1:19;
hence contradiction by A14, A15, ORDINAL1:7; :: thesis: verum

end;

then consider C1 being Ordinal such that
A16: C = succ C1 by ORDINAL1:42;
C1 in C by A16, ORDINAL1:10;
then ( C1 in B & not C c= C1 ) by A13, ORDINAL1:7, ORDINAL1:19;
then not B in C1 *^ A by A14;
then C1 *^ A c= B by ORDINAL1:26;
then consider D being Ordinal such that
A17: B = (C1 *^ A) +^ D by Th30;
thus S₁[B] :: thesis: verum

proof

take C1 ; :: thesis: ex D being Ordinal st
( B = (C1 *^ A) +^ D & D in A )
take D ; :: thesis: ( B = (C1 *^ A) +^ D & D in A )
thus B = (C1 *^ A) +^ D by A17; :: thesis: D in A
(C1 *^ A) +^ D in (C1 *^ A) +^ A by A13, A16, A17, ORDINAL2:53;
hence D in A by Th25; :: thesis: verum

end;

end;

hence S₁[B] by A11; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A2, A3, A8);
hence ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A ) ; :: thesis: verum