let a be ordinal number ; :: thesis: for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a
let A be finite Ordinal-Sequence; :: thesis: Sum^ (A ^ <%a%>) = (Sum^ A) +^ a
consider f being Ordinal-Sequence such that
A1: ( Sum^ (A ^ <%a%>) = last f & dom f = succ (dom (A ^ <%a%>)) & f . 0 = 0 & ( for n being Nat st n in dom (A ^ <%a%>) holds
f . (n + 1) = (f . n) +^ ((A ^ <%a%>) . n) ) ) by SUM;
consider g being Ordinal-Sequence such that
A2: ( Sum^ A = last g & dom g = succ (dom A) & g . 0 = 0 & ( for n being Nat st n in dom A holds
g . (n + 1) = (g . n) +^ (A . n) ) ) by SUM;
dom <%a%> = 1 by AFINSQ_1:def 5;
then A5: ( dom (A ^ <%a%>) = (dom A) +^ 1 & (dom A) +^ 1 = succ (dom A) ) by ORDINAL2:48, ORDINAL4:def 1;
reconsider dA = dom A as Element of NAT by ORDINAL1:def 13;
A6: dom A in succ (dom A) by ORDINAL1:10;
defpred S₁[ Nat] means ( $1 in succ (dom A) implies f . $1 = g . $1 );
A3: S₁[ 0 ] by A1, A2;
A4: for n being natural number st S₁[n] holds
S₁[n + 1]

proof

let n be natural number ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
B1: S₁[n] and
B2: n + 1 in succ (dom A) ; :: thesis: f . (n + 1) = g . (n + 1)
n + 1 = succ n by NAT_1:39;
then B3: n in dom A by B2, ORDINAL3:5;
then B4: n in succ (dom A) by A6, ORDINAL1:19;
then ( g . (n + 1) = (g . n) +^ (A . n) & f . (n + 1) = (f . n) +^ ((A ^ <%a%>) . n) ) by A1, A2, A5, B3;
hence f . (n + 1) = g . (n + 1) by B1, B3, B4, ORDINAL4:def 1; :: thesis: verum

end;

AA: for n being natural number holds S₁[n] from NAT_1:sch 2(A3, A4);
thus Sum^ (A ^ <%a%>) = f . ((dom A) +^ 1) by A1, A5, ORDINAL2:7
.= f . (dA + 1) by CARD_2:49
.= (f . (dom A)) +^ ((A ^ <%a%>) . (len A)) by A1, A5, A6
.= (f . (dom A)) +^ a by AFINSQ_1:40
.= (g . (dom A)) +^ a by A6, AA
.= (Sum^ A) +^ a by A2, ORDINAL2:7 ; :: thesis: verum