let f, g be XFinSequence of NAT ; :: thesis: for i being Integer st dom f = dom g & ( for n being object st n in dom f holds
f . n = i * (g . n) ) holds
Sum f = i * (Sum g)
let i be Integer; :: thesis: ( dom f = dom g & ( for n being object st n in dom f holds
f . n = i * (g . n) ) implies Sum f = i * (Sum g) )
assume ( dom f = dom g & ( for n being object st n in dom f holds
f . n = i * (g . n) ) ) ; :: thesis: Sum f = i * (Sum g)
then f = i (#) g by VALUED_1:def 5;
hence Sum f = i * (Sum g) by AFINSQ_2:64; :: thesis: verum