defpred S₁[ Nat] means for A, B being finite Ordinal-Sequence st dom B = $1 holds
Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B);
A1: S₁[ 0 ]

proof

let A, B be finite Ordinal-Sequence; :: thesis: ( dom B = 0 implies Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B) )
assume dom B = 0 ; :: thesis: Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)
then B = {} ;
hence Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B) by ORDINAL2:27, ORDINAL5:52; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let A, B be finite Ordinal-Sequence; :: thesis: ( dom B = n + 1 implies Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B) )
assume A4: dom B = n + 1 ; :: thesis: 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 ; :: thesis: verum

end;

A8: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let A, B be finite Ordinal-Sequence; :: thesis: Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)
dom B is Nat ;
hence Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B) by A8; :: thesis: verum