let a be Ordinal; :: 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 Def8;
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 Def8;
dom <%a%> = 1 by AFINSQ_1:def 4;
then A3: ( dom (A ^ <%a%>) = (dom A) +^ 1 & (dom A) +^ 1 = succ (dom A) ) by ORDINAL2:31, ORDINAL4:def 1;
reconsider dA = dom A as Element of NAT by ORDINAL1:def 12;
A4: dom A in succ (dom A) by ORDINAL1:6;
defpred S₁[ Nat] means ( $1 in succ (dom A) implies f . $1 = g . $1 );
A5: S₁[ 0 ] by A1, A2;
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A7: S₁[n] and
A8: n + 1 in succ (dom A) ; :: thesis: f . (n + 1) = g . (n + 1)
Segm (n + 1) = succ (Segm n) by NAT_1:38;
then A9: n in dom A by A8, ORDINAL3:3;
then n in succ (dom A) by A4, ORDINAL1:10;
then ( g . (n + 1) = (g . n) +^ (A . n) & f . (n + 1) = (f . n) +^ ((A ^ <%a%>) . n) ) by A1, A2, A3, A9;
hence f . (n + 1) = g . (n + 1) by A7, A9, A4, ORDINAL1:10, ORDINAL4:def 1; :: thesis: verum

end;

A10: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
thus Sum^ (A ^ <%a%>) = f . ((dom A) +^ 1) by A1, A3, ORDINAL2:6
.= f . (dA + 1) by CARD_2:36
.= (f . (dom A)) +^ ((A ^ <%a%>) . (len A)) by A1, A3, ORDINAL1:6
.= (f . (dom A)) +^ a by AFINSQ_1:36
.= (g . (dom A)) +^ a by A10, ORDINAL1:6
.= (Sum^ A) +^ a by A2, ORDINAL2:6 ; :: thesis: verum