let a be Ordinal; :: thesis: for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)
defpred S1[ finite Sequence] means for f being finite Ordinal-Sequence st f = $1 holds
Sum^ (<%a%> ^ f) = a +^ (Sum^ f);
Sum^ (<%a%> ^ {}) = a by Th53;
then A1: S1[ {} ] by Th52, ORDINAL2:27;
A2: for f being finite Sequence
for x being object st S1[f] holds
S1[f ^ <%x%>]
proof
let f be finite Sequence; :: thesis: for x being object st S1[f] holds
S1[f ^ <%x%>]
let x be object ; :: thesis: ( S1[f] implies S1[f ^ <%x%>] )
assume A3: S1[f] ; :: thesis: S1[f ^ <%x%>]
let g be finite Ordinal-Sequence; :: thesis: ( g = f ^ <%x%> implies Sum^ (<%a%> ^ g) = a +^ (Sum^ g) )
consider b being Ordinal such that
A4: rng g c= b by ORDINAL2:def 4;
assume A5: g = f ^ <%x%> ; :: thesis: Sum^ (<%a%> ^ g) = a +^ (Sum^ g)
then rng g = (rng f) \/ (rng <%x%>) by AFINSQ_1:26;
then A6: ( rng f c= b & rng <%x%> c= b ) by A4, XBOOLE_1:11;
then reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 4;
rng <%x%> = {x} by AFINSQ_1:33;
then x in b by A6, ZFMISC_1:31;
then reconsider x = x as Ordinal ;
thus Sum^ (<%a%> ^ g) = Sum^ ((<%a%> ^ f9) ^ <%x%>) by A5, AFINSQ_1:27
.= (Sum^ (<%a%> ^ f9)) +^ x by Th54
.= (a +^ (Sum^ f9)) +^ x by A3
.= a +^ ((Sum^ f9) +^ x) by ORDINAL3:30
.= a +^ (Sum^ g) by A5, Th54 ; :: thesis: verum
end;
for f being finite Sequence holds S1[f] from AFINSQ_1:sch 3(A1, A2);
 hence for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A) ; :: thesis: verum