let b, n be Nat; :: thesis: for f, g being n -element XFinSequence of NAT holds value ((f + g),b) = (value (f,b)) + (value (g,b))
let f, g be n -element XFinSequence of NAT ; :: thesis: value ((f + g),b) = (value (f,b)) + (value (g,b))
consider p being XFinSequence of NAT such that
A1: ( dom p = dom (f + g) & ( for i being Nat st i in dom p holds
p . i = ((f + g) . i) * (b |^ i) ) & value ((f + g),b) = Sum p ) by NUMERAL1:def 1;
consider p1 being XFinSequence of NAT such that
A2: ( dom p1 = dom f & ( for i being Nat st i in dom p1 holds
p1 . i = (f . i) * (b |^ i) ) & value (f,b) = Sum p1 ) by NUMERAL1:def 1;
consider p2 being XFinSequence of NAT such that
A3: ( dom p2 = dom g & ( for i being Nat st i in dom p2 holds
p2 . i = (g . i) * (b |^ i) ) & value (g,b) = Sum p2 ) by NUMERAL1:def 1;
A4: ( dom p = n & dom p1 = n & dom p2 = n & dom f = n & dom g = n & dom (f + g) = n ) by A1, A2, A3, CARD_1:def 7;
reconsider p = p as n -element XFinSequence of NAT by A4, CARD_1:def 7;
reconsider p1 = p1 as n -element XFinSequence of NAT by A4, CARD_1:def 7;
reconsider p2 = p2 as n -element XFinSequence of NAT by A4, CARD_1:def 7;
A5: dom (p1 + p2) = (dom p1) /\ (dom p2) by VALUED_1:def 1;
p = p1 + p2

proof

for k being Nat st k in dom p holds
p . k = (p1 + p2) . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = (p1 + p2) . k )
assume B1: k in dom p ; :: thesis: p . k = (p1 + p2) . k
B3: ( p . k = ((f + g) . k) * (b |^ k) & p1 . k = (f . k) * (b |^ k) & p2 . k = (g . k) * (b |^ k) ) by B1, A1, A2, A3, A4;
p . k = ((f + g) . k) * (b |^ k) by B1, A1
.= ((f . k) + (g . k)) * (b |^ k) by B1, VALUED_1:def 1, A1
.= (p1 . k) + (p2 . k) by B3 ;
hence p . k = (p1 + p2) . k by B1, A4, A5, VALUED_1:def 1; :: thesis: verum

end;

hence p = p1 + p2 by A4, A5; :: thesis: verum

end;

hence value ((f + g),b) = (value (f,b)) + (value (g,b)) by A1, A2, A3, RVSUM_4:49; :: thesis: verum