let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for F, G being FinSequence of R holds h . (Sum (F ^ G)) = (h . (Sum F)) + (h . (Sum G))
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for F, G being FinSequence of R holds h . (Sum (F ^ G)) = (h . (Sum F)) + (h . (Sum G))
let h be Homomorphism of R,S; :: thesis: for F, G being FinSequence of R holds h . (Sum (F ^ G)) = (h . (Sum F)) + (h . (Sum G))
let F, G be FinSequence of R; :: thesis: h . (Sum (F ^ G)) = (h . (Sum F)) + (h . (Sum G))
thus h . (Sum (F ^ G)) = h . ((Sum F) + (Sum G)) by RLVECT_1:41
.= (h . (Sum F)) + (h . (Sum G)) by VECTSP_1:def 20 ; :: thesis: verum