let a be ordinal number ; :: thesis: for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)
defpred S₁[ finite T-Sequence] means for f being finite Ordinal-Sequence st f = $1 holds
Sum^ (<%a%> ^ f) = a +^ (Sum^ f);
<%a%> ^ {} = <%a%> by AFINSQ_1:32;
then Sum^ (<%a%> ^ {} ) = a by Th51;
then A0: S₁[ {} ] by Th50, ORDINAL2:44;
A1: for f being finite T-Sequence
for x being set st S₁[f] holds
S₁[f ^ <%x%>]

proof

let f be finite T-Sequence; :: thesis: for x being set st S₁[f] holds
S₁[f ^ <%x%>]
let x be set ; :: thesis: ( S₁[f] implies S₁[f ^ <%x%>] )
assume A2: 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 number such that
A3: rng g c= b by ORDINAL2:def 8;
assume A4: g = f ^ <%x%> ; :: thesis: Sum^ (<%a%> ^ g) = a +^ (Sum^ g)
then rng g = (rng f) \/ (rng <%x%>) by AFINSQ_1:29;
then A5: ( rng f c= b & rng <%x%> c= b ) by A3, XBOOLE_1:11;
then reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 8;
rng <%x%> = {x} by AFINSQ_1:36;
then x in b by A5, ZFMISC_1:37;
then reconsider x = x as Ordinal ;
thus Sum^ (<%a%> ^ g) = Sum^ ((<%a%> ^ f9) ^ <%x%>) by A4, AFINSQ_1:30
.= (Sum^ (<%a%> ^ f9)) +^ x by Th59
.= (a +^ (Sum^ f9)) +^ x by A2
.= a +^ ((Sum^ f9) +^ x) by ORDINAL3:33
.= a +^ (Sum^ g) by A4, Th59 ; :: thesis: verum

end;

for f being finite T-Sequence holds S₁[f] from AFINSQ_1:sch 3(A0, A1);
hence for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A) ; :: thesis: verum