defpred S₁[ Nat] means for A being finite Ordinal-Sequence
for b being Ordinal st dom A = $1 & ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) holds
Sum^ A in exp (omega,b);
A1: S₁[ 0 ]

proof

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;

per cases ( 0 in b or not 0 in b ) ;

suppose 0 in b ; :: thesis: Sum^ A in exp (omega,b)

then exp (omega,0) in exp (omega,b) by ORDINAL4:24;
hence Sum^ A in exp (omega,b) by A3, ORDINAL1:10; :: thesis: verum

end;

suppose not 0 in b ; :: thesis: Sum^ A in exp (omega,b)

hence Sum^ A in exp (omega,b) by A3, ORDINAL1:16, XBOOLE_1:3; :: thesis: verum

end;

end;

end;

A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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;

now :: thesis: for a being Ordinal st a in dom A0 holds
A0 . a in exp (omega,b)

let a be Ordinal; :: thesis: ( a in dom A0 implies A0 . a in exp (omega,b) )
assume A11: a in dom A0 ; :: thesis: A0 . a in exp (omega,b)
then A12: A0 . a = A . a by A8, AFINSQ_1:def 3;
dom A0 c= dom A by A8, AFINSQ_1:21;
hence A0 . a in exp (omega,b) by A7, A11, A12; :: thesis: verum

end;

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

end;

A15: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A4);
let A be finite Ordinal-Sequence; :: thesis: for b being Ordinal st ( 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: ( ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) implies Sum^ A in exp (omega,b) )
thus ( ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) implies Sum^ A in exp (omega,b) ) by A15; :: thesis: verum