let A, C be Ordinal; :: thesis: ( C <> {} implies exp (C,A) <> {} )
defpred S1[ Ordinal] means exp (C,\$1) <> {} ;
assume A1: C <> {} ; :: thesis: exp (C,A) <> {}
A2: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; :: thesis: ( S1[A] implies S1[ succ A] )
assume A3: exp (C,A) <> {} ; :: thesis: S1[ succ A]
exp (C,(succ A)) = C *^ (exp (C,A)) by ORDINAL2:44;
hence S1[ succ A] by ; :: thesis: verum
end;
A4: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[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: S1[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 ;
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 ;
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 ;
fi . B = exp (C,B) by A8, A9, A14;
hence contradiction by A7, A8, A14, A15; :: thesis: verum
end;
A16: S1[ 0 ] by ORDINAL2:43;
for A being Ordinal holds S1[A] from hence exp (C,A) <> {} ; :: thesis: verum