let G be strict Group; :: thesis: for F2 being strict Subgroup of G
for F1 being strict normal Subgroup of F2
for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
let F2 be strict Subgroup of G; :: thesis: for F1 being strict normal Subgroup of F2
for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
let F1 be strict normal Subgroup of F2; :: thesis: for a, b being Element of F2 holds (a * F1) * (b * F1) = (a * b) * F1
let a, b be Element of F2; :: thesis: (a * F1) * (b * F1) = (a * b) * F1
A1: ( (nat_hom F1) . a = a * F1 & (nat_hom F1) . b = b * F1 ) by GROUP_6:def 8;
A2: ( @ ((nat_hom F1) . a) = (nat_hom F1) . a & @ ((nat_hom F1) . b) = (nat_hom F1) . b ) by GROUP_6:def 5;
thus (a * b) * F1 = (nat_hom F1) . (a * b) by GROUP_6:def 8
.= ((nat_hom F1) . a) * ((nat_hom F1) . b) by GROUP_6:def 6
.= (a * F1) * (b * F1) by A1, A2, GROUP_6:19 ; :: thesis: verum