for v, w being Element of M holds (nat_hom R) . (v * w) = ((nat_hom R) . v) * ((nat_hom R) . w)

proof

let v, w be Element of M; :: thesis: (nat_hom R) . (v * w) = ((nat_hom R) . v) * ((nat_hom R) . w)
( (nat_hom R) . v = Class R,v & (nat_hom R) . w = Class R,w ) by Def7;
then (ClassOp R) . ((nat_hom R) . v),((nat_hom R) . w) = Class R,(v * w) by Def5;
hence (nat_hom R) . (v * w) = ((nat_hom R) . v) * ((nat_hom R) . w) by Def7; :: thesis: verum

end;

hence nat_hom R is multiplicative by GROUP_6:def 7; :: thesis: verum