let a be Ordinal; :: thesis: for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)
defpred S₁[ 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: S₁[ {} ] by Th52, ORDINAL2:27;
A2: for f being finite Sequence
for x being object st S₁[f] holds
S₁[f ^ <%x%>]

proof

let f be finite Sequence; :: thesis: for x being object st S₁[f] holds
S₁[f ^ <%x%>]
let x be object ; :: thesis: ( S₁[f] implies S₁[f ^ <%x%>] )
assume A3: S₁[f] ; :: thesis: S₁[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 S₁[f] from AFINSQ_1:sch 3(A1, A2);
hence for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A) ; :: thesis: verum