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 . (Product (F ^ <*a*>)) = (h . (Product F)) * (h . a)
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 . (Product (F ^ <*a*>)) = (h . (Product F)) * (h . a)
let h be Homomorphism of R,S; :: thesis: for F being FinSequence of R
for a being Element of R holds h . (Product (F ^ <*a*>)) = (h . (Product F)) * (h . a)
let F be FinSequence of R; :: thesis: for a being Element of R holds h . (Product (F ^ <*a*>)) = (h . (Product F)) * (h . a)
let a be Element of R; :: thesis: h . (Product (F ^ <*a*>)) = (h . (Product F)) * (h . a)
thus h . (Product (F ^ <*a*>)) = h . ((Product F) * (Product <*a*>)) by GROUP_4:5
.= (h . (Product F)) * (h . (Product <*a*>)) by GROUP_6:def 6
.= (h . (Product F)) * (h . a) by GROUP_4:9 ; :: thesis: verum