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