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 Def6;
then (ClassOp R) . (((nat_hom R) . v),((nat_hom R) . w)) = Class (R,(v * w)) by Def4;
hence (nat_hom R) . (v * w) = ((nat_hom R) . v) * ((nat_hom R) . w) by Def6; :: thesis: verum

end;

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