let A, B be Ordinal; :: thesis: ( A <> {} implies 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 );
assume A1: A <> {} ; :: thesis: ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )
A2: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for A1 being Ordinal st A1 in B holds
S₁[A1] ) holds
S₁[B]

proof

{} in A by A1, Th8;
then A3: succ 0 c= A by ORDINAL1:21;
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for A1 being Ordinal st A1 in B holds
S₁[A1] ) implies S₁[B] )
assume that
B <> 0 and
A4: B is limit_ordinal and
for A1 being Ordinal st A1 in B holds
S₁[A1] ; :: thesis: S₁[B]
defpred S₂[ Ordinal] means ( $1 in B & B in $1 *^ A );
B *^ 1 = B by ORDINAL2:39;
then A5: B c= B *^ A by A3, ORDINAL2:42;

A6: now :: thesis: ( B <> B *^ A implies S₁[B] )

assume B <> B *^ A ; :: thesis: S₁[B]
then B c< B *^ A by A5;
then B in B *^ A by ORDINAL1:11;
then A7: ex C being Ordinal st S₂[C] by A4, Th41;
consider C being Ordinal such that
A8: S₂[C] and
A9: for C1 being Ordinal st S₂[C1] holds
C c= C1 from ORDINAL1:sch 1(A7);

now :: thesis: not C is limit_ordinal

assume C is limit_ordinal ; :: thesis: contradiction
then consider C1 being Ordinal such that
A10: C1 in C and
A11: B in C1 *^ A by A8, Th41;
C1 in B by A8, A10, ORDINAL1:10;
hence contradiction by A9, A10, A11, ORDINAL1:5; :: thesis: verum

end;

then consider C1 being Ordinal such that
A12: C = succ C1 by ORDINAL1:29;
A13: C1 in C by A12, ORDINAL1:6;
then C1 in B by A8, ORDINAL1:10;
then not B in C1 *^ A by A9, A13, ORDINAL1:5;
then consider D being Ordinal such that
A14: B = (C1 *^ A) +^ D by Th27, ORDINAL1:16;
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 A14; :: thesis: D in A
(C1 *^ A) +^ D in (C1 *^ A) +^ A by A8, A12, A14, ORDINAL2:36;
hence D in A by Th22; :: thesis: verum

end;

end;

( B = B *^ A implies ( B = (B *^ A) +^ {} & {} in A ) ) by A1, Th8, ORDINAL2:27;
hence S₁[B] by A6; :: thesis: verum

end;

A15: 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 A16: B = (C *^ A) +^ D and
A17: D in A ; :: thesis: S₁[ succ B]

A18: now :: thesis: ( not succ D in A implies ex C1 being set ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A ) )

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 A19: A c= succ D by ORDINAL1:16;
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 )
succ D c= A by A17, ORDINAL1:21;
then A20: A = succ D by A19;
thus (C1 *^ A) +^ D1 = C1 *^ A by ORDINAL2:27
.= (C *^ A) +^ A by ORDINAL2:36
.= succ B by A16, A20, ORDINAL2:28 ; :: thesis: D1 in A
thus D1 in A by A1, Th8; :: thesis: verum

end;

now :: thesis: ( succ D in A implies ex C1 being Ordinal ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A ) )

assume A21: 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 A16, ORDINAL2:28; :: thesis: D1 in A
thus D1 in A by A21; :: thesis: verum

end;

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

end;

A22: S₁[ 0 ]

proof

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

end;

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