set f = nat_hom N;
let a be Element of G; :: according to GROUP_6:def 6 :: thesis: for b being Element of G holds (nat_hom N) . (a * b) = ((nat_hom N) . a) * ((nat_hom N) . b)
let b be Element of G; :: thesis: (nat_hom N) . (a * b) = ((nat_hom N) . a) * ((nat_hom N) . b)
A1: (nat_hom N) . a = a * N by Def8;
A2: (nat_hom N) . b = b * N by Def8;
A3: (nat_hom N) . (a * b) = (a * b) * N by Def8;
thus ((nat_hom N) . a) * ((nat_hom N) . b) = (@ ((nat_hom N) . a)) * (@ ((nat_hom N) . b)) by Def3
.= ((a * N) * b) * N by A1, A2, GROUP_3:9
.= (a * (N * b)) * N by GROUP_2:106
.= (a * (b * N)) * N by GROUP_3:117
.= a * ((b * N) * N) by GROUP_2:96
.= a * (b * N) by Th5
.= (nat_hom N) . (a * b) by A3, GROUP_2:105 ; :: thesis: verum