let A, C be Ordinal; :: thesis: ( C <> {} implies exp (C,A) <> {} )

defpred S_{1}[ Ordinal] means exp (C,$1) <> {} ;

assume A1: C <> {} ; :: thesis: exp (C,A) <> {}

A2: for A being Ordinal st S_{1}[A] holds

S_{1}[ succ A]

S_{1}[B] ) holds

S_{1}[A]
_{1}[ 0 ]
by ORDINAL2:43;

for A being Ordinal holds S_{1}[A]
from ORDINAL2:sch 1(A16, A2, A4);

hence exp (C,A) <> {} ; :: thesis: verum

defpred S

assume A1: C <> {} ; :: thesis: exp (C,A) <> {}

A2: for A being Ordinal st S

S

proof

A4:
for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
let A be Ordinal; :: thesis: ( S_{1}[A] implies S_{1}[ succ A] )

assume A3: exp (C,A) <> {} ; :: thesis: S_{1}[ succ A]

exp (C,(succ A)) = C *^ (exp (C,A)) by ORDINAL2:44;

hence S_{1}[ succ A]
by A1, A3, ORDINAL3:31; :: thesis: verum

end;assume A3: exp (C,A) <> {} ; :: thesis: S

exp (C,(succ A)) = C *^ (exp (C,A)) by ORDINAL2:44;

hence S

S

S

proof

A16:
S
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds

S_{1}[B] ) implies S_{1}[A] )

assume that

A5: A <> 0 and

A6: A is limit_ordinal and

A7: for B being Ordinal st B in A holds

exp (C,B) <> {} ; :: thesis: S_{1}[A]

consider fi being Ordinal-Sequence such that

A8: dom fi = A and

A9: for B being Ordinal st B in A holds

fi . B = exp (C,B) and

A10: ex D being Ordinal st D is_limes_of fi by A5, A6, Lm8;

A11: exp (C,A) = lim fi by A5, A6, A8, A9, ORDINAL2:45;

assume A12: exp (C,A) = {} ; :: thesis: contradiction

consider D being Ordinal such that

A13: D is_limes_of fi by A10;

lim fi = D by A13, ORDINAL2:def 10;

then consider B being Ordinal such that

A14: B in dom fi and

A15: for D being Ordinal st B c= D & D in dom fi holds

fi . D = {} by A11, A13, A12, ORDINAL2:def 9;

fi . B = exp (C,B) by A8, A9, A14;

hence contradiction by A7, A8, A14, A15; :: thesis: verum

end;S

assume that

A5: A <> 0 and

A6: A is limit_ordinal and

A7: for B being Ordinal st B in A holds

exp (C,B) <> {} ; :: thesis: S

consider fi being Ordinal-Sequence such that

A8: dom fi = A and

A9: for B being Ordinal st B in A holds

fi . B = exp (C,B) and

A10: ex D being Ordinal st D is_limes_of fi by A5, A6, Lm8;

A11: exp (C,A) = lim fi by A5, A6, A8, A9, ORDINAL2:45;

assume A12: exp (C,A) = {} ; :: thesis: contradiction

consider D being Ordinal such that

A13: D is_limes_of fi by A10;

lim fi = D by A13, ORDINAL2:def 10;

then consider B being Ordinal such that

A14: B in dom fi and

A15: for D being Ordinal st B c= D & D in dom fi holds

fi . D = {} by A11, A13, A12, ORDINAL2:def 9;

fi . B = exp (C,B) by A8, A9, A14;

hence contradiction by A7, A8, A14, A15; :: thesis: verum

for A being Ordinal holds S

hence exp (C,A) <> {} ; :: thesis: verum