let a, b be Ordinal; :: thesis: for n being Nat st a in exp (omega,b) holds
n *^ a in exp (omega,b)
let n be Nat; :: thesis: ( a in exp (omega,b) implies n *^ a in exp (omega,b) )
assume a in exp (omega,b) ; :: thesis: n *^ a in exp (omega,b)
then for c being Ordinal st c in dom (n --> a) holds
(n --> a) . c in exp (omega,b) by FUNCOP_1:7;
then Sum^ (n --> a) in exp (omega,b) by Th41;
hence n *^ a in exp (omega,b) by Th26; :: thesis: verum