defpred S1[ 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:
S1[ 0 ]
A4:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A5:
S1[
n]
;
S1[n + 1]
let A be
finite Ordinal-Sequence;
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;
( 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)
;
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;
verum
end;
A15:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A4);
let A be finite Ordinal-Sequence; 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; ( ( 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; verum