defpred S1[ Nat] means for A, B being finite Ordinal-Sequence st dom B = $1 holds
Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B);
A1:
S1[ 0 ]
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
let A,
B be
finite Ordinal-Sequence;
( dom B = n + 1 implies Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B) )
assume A4:
dom B = n + 1
;
Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)
then
B <> {}
;
then consider C being
XFinSequence,
a being
object such that A5:
B = C ^ <%a%>
by AFINSQ_1:40;
consider b being
Ordinal such that A6:
rng B c= b
by ORDINAL2:def 4;
rng C c= rng B
by A5, AFINSQ_1:24;
then reconsider C =
C as
finite Ordinal-Sequence by A6, XBOOLE_1:1, ORDINAL2:def 4;
rng <%a%> c= rng B
by A5, AFINSQ_1:25;
then
{a} c= rng B
by AFINSQ_1:33;
then
a in rng B
by ZFMISC_1:31;
then reconsider a =
a as
Ordinal ;
A7:
(dom C) + 1 =
(len C) + (len <%a%>)
by AFINSQ_1:34
.=
n + 1
by A4, A5, AFINSQ_1:17
;
thus Sum^ (A ^ B) =
Sum^ ((A ^ C) ^ <%a%>)
by A5, AFINSQ_1:27
.=
(Sum^ (A ^ C)) +^ a
by ORDINAL5:54
.=
((Sum^ A) +^ (Sum^ C)) +^ a
by A3, A7
.=
(Sum^ A) +^ ((Sum^ C) +^ a)
by ORDINAL3:30
.=
(Sum^ A) +^ (Sum^ B)
by A5, ORDINAL5:54
;
verum
end;
A8:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
let A, B be finite Ordinal-Sequence; Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)
dom B is Nat
;
hence
Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)
by A8; verum