let A be finite Ordinal-Sequence; :: thesis: for b being Ordinal st dom A = 0 & ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) holds
Sum^ A in exp (omega,b)
let b be Ordinal; :: thesis: ( dom A = 0 & ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) implies Sum^ A in exp (omega,b) )
assume that
A2: dom A = 0 and
for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ; :: thesis: Sum^ A in exp (omega,b)
A = {} by A2;
then Sum^ A in 1 by ORDINAL5:52, CARD_1:49, TARSKI:def 1;
then A3: Sum^ A in exp (omega,0) by ORDINAL2:43;

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
let A be finite Ordinal-Sequence; :: thesis: for b being Ordinal st dom A = n + 1 & ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) holds
Sum^ A in exp (omega,b)
let b be Ordinal; :: thesis: ( dom A = n + 1 & ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) implies Sum^ A in exp (omega,b) )
assume that
A6: dom A = n + 1 and
A7: for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ; :: thesis: Sum^ A in exp (omega,b)
A <> {} by A6;
then consider A0 being XFinSequence, a0 being object such that
A8: A = A0 ^ <%a0%> by AFINSQ_1:40;
consider c being Ordinal such that
A9: rng A c= c by ORDINAL2:def 4;
rng A0 c= rng A by A8, AFINSQ_1:24;
then reconsider A0 = A0 as finite Ordinal-Sequence by A9, XBOOLE_1:1, ORDINAL2:def 4;
rng <%a0%> c= rng A by A8, AFINSQ_1:25;
then {a0} c= rng A by AFINSQ_1:33;
then a0 in rng A by ZFMISC_1:31;
then reconsider a0 = a0 as Ordinal ;
A10: (len A0) + 1 = n + 1 by A6, A8, AFINSQ_1:75;
then A13: Sum^ A0 in exp (omega,b) by A5, A10;
n + 0 < n + 1 by XREAL_1:8;
then A . n in exp (omega,b) by A7, AFINSQ_1:86, A6;
then A14: a0 in exp (omega,b) by A8, A10, AFINSQ_1:36;
Sum^ A = (Sum^ A0) +^ a0 by A8, ORDINAL5:54;
hence Sum^ A in exp (omega,b) by A13, A14, Th40; :: thesis: verum