let b, k, n be Nat; :: thesis: for f being k -element XFinSequence of NAT holds value ((f ^ <%n%>),b) = (value (f,b)) + (n * (b |^ k))
let f be k -element XFinSequence of NAT ; :: thesis: value ((f ^ <%n%>),b) = (value (f,b)) + (n * (b |^ k))
reconsider g = f ^ <%n%> as k + 1 -element XFinSequence of NAT ;
consider g1 being XFinSequence of NAT such that
A1: ( dom g1 = dom g & ( for i being Nat st i in dom g1 holds
g1 . i = (g . i) * (b |^ i) ) & value (g,b) = Sum g1 ) by NUMERAL1:def 1;
consider f1 being XFinSequence of NAT such that
A2: ( dom f1 = dom f & ( for i being Nat st i in dom f1 holds
f1 . i = (f . i) * (b |^ i) ) & value (f,b) = Sum f1 ) by NUMERAL1:def 1;
A3: ( dom g1 = k + 1 & dom f1 = k ) by A1, A2, CARD_1:def 7;
A5: k + 0 < k + 1 by XREAL_1:6;
then A6: ( dom (g1 | k) = k & k = dom f1 ) by A3, AFINSQ_1:54;
A7: g1 | k = f1

proof

for i being Nat st i in dom f1 holds
f1 . i = (g1 | k) . i

proof

let i be Nat; :: thesis: ( i in dom f1 implies f1 . i = (g1 | k) . i )
assume C1: i in dom f1 ; :: thesis: f1 . i = (g1 | k) . i
k + 0 < k + 1 by XREAL_1:6;
then i < len g by C1, AFINSQ_1:86, A1, A3, XXREAL_0:2;
then g1 . i = (g . i) * (b |^ i) by A1, AFINSQ_1:86
.= (f . i) * (b |^ i) by AFINSQ_1:def 3, C1, A2
.= f1 . i by A2, C1 ;
hence f1 . i = (g1 | k) . i by C1, A3, FUNCT_1:49; :: thesis: verum

end;

hence g1 | k = f1 by A6; :: thesis: verum

end;

g1 . k = (g . k) * (b |^ k) by A1, A3, A5, AFINSQ_1:86
.= n * (b |^ k) ;
then g1 = f1 ^ <%(n * (b |^ k))%> by A7, A1, CARD_1:def 7, AFINSQ_1:56;
then value (g,b) = (Sum f1) + (Sum <%(n * (b |^ k))%>) by A1, AFINSQ_2:55
.= (value (f,b)) + (n * (b |^ k)) by A2 ;
hence value ((f ^ <%n%>),b) = (value (f,b)) + (n * (b |^ k)) ; :: thesis: verum