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

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