let b be Nat; for f, g being XFinSequence of NAT holds value ((f ^ g),b) = (value (f,b)) + ((value (g,b)) * (b |^ (len f)))
let f, g be XFinSequence of NAT ; value ((f ^ g),b) = (value (f,b)) + ((value (g,b)) * (b |^ (len f)))
consider fx being XFinSequence of NAT such that
A1:
dom fx = dom f
and
A2:
for i being Nat st i in dom fx holds
fx . i = (f . i) * (b |^ i)
and
A3:
value (f,b) = Sum fx
by NUMERAL1:def 1;
consider gx being XFinSequence of NAT such that
A4:
dom gx = dom g
and
A5:
for i being Nat st i in dom gx holds
gx . i = (g . i) * (b |^ i)
and
A6:
value (g,b) = Sum gx
by NUMERAL1:def 1;
consider fgx being XFinSequence of NAT such that
A7:
dom fgx = dom (f ^ g)
and
A8:
for i being Nat st i in dom fgx holds
fgx . i = ((f ^ g) . i) * (b |^ i)
and
A9:
value ((f ^ g),b) = Sum fgx
by NUMERAL1:def 1;
dom (f ^ g) = (len f) + (len g)
by AFINSQ_1:def 3;
then consider Fx, Gx being XFinSequence such that
A10:
( len Fx = len f & len Gx = len g & fgx = Fx ^ Gx )
by A7, AFINSQ_1:61;
( rng Fx c= rng fgx & rng Gx c= rng fgx & rng fgx c= NAT )
by A10, AFINSQ_1:24, AFINSQ_1:25;
then reconsider Fx = Fx, Gx = Gx as XFinSequence of NAT by XBOOLE_1:1, RELAT_1:def 19;
for k being Nat st k in dom fx holds
fx . k = Fx . k
proof
let k be
Nat;
( k in dom fx implies fx . k = Fx . k )
assume A11:
k in dom fx
;
fx . k = Fx . k
A12:
fx . k = (f . k) * (b |^ k)
by A2, A11;
A13:
Fx . k = fgx . k
by A1, A11, A10, AFINSQ_1:def 3;
dom f c= dom (f ^ g)
by AFINSQ_1:21;
then
fgx . k = ((f ^ g) . k) * (b |^ k)
by A1, A11, A7, A8;
hence
fx . k = Fx . k
by A13, A12, A1, A11, AFINSQ_1:def 3;
verum
end;
then A14:
fx = Fx
by A10, A1, AFINSQ_1:8;
set B = b |^ (len f);
A15:
dom ((b |^ (len f)) (#) gx) = dom gx
by VALUED_1:def 5;
for k being Nat st k in dom gx holds
((b |^ (len f)) (#) gx) . k = Gx . k
proof
let k be
Nat;
( k in dom gx implies ((b |^ (len f)) (#) gx) . k = Gx . k )
assume A16:
k in dom gx
;
((b |^ (len f)) (#) gx) . k = Gx . k
A17:
gx . k = (g . k) * (b |^ k)
by A5, A16;
A18:
fgx . (k + (len Fx)) = ((f ^ g) . (k + (len Fx))) * (b |^ (k + (len Fx)))
by AFINSQ_1:23, A4, A16, A10, A8;
A19:
(f ^ g) . (k + (len Fx)) = g . k
by A4, A16, A10, AFINSQ_1:def 3;
A20:
b |^ (k + (len Fx)) = (b |^ k) * (b |^ (len f))
by A10, NEWTON:8;
((b |^ (len f)) (#) gx) . k = (b |^ (len f)) * (gx . k)
by VALUED_1:6;
hence
((b |^ (len f)) (#) gx) . k = Gx . k
by A4, A16, A10, AFINSQ_1:def 3, A17, A18, A19, A20;
verum
end;
then
Gx = (b |^ (len f)) (#) gx
by A15, A4, A10, AFINSQ_1:8;
hence value ((f ^ g),b) =
(Sum Fx) + (Sum ((b |^ (len f)) (#) gx))
by A9, A10, AFINSQ_2:55
.=
(value (f,b)) + ((value (g,b)) * (b |^ (len f)))
by A3, A6, A14, AFINSQ_2:64
;
verum