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 9;
A2: ( @ ((nat_hom F1) . a) = (nat_hom F1) . a & @ ((nat_hom F1) . b) = (nat_hom F1) . b ) by GROUP_6:def 6;
thus (a * b) * F1 = (nat_hom F1) . (a * b) by GROUP_6:def 9
.= ((nat_hom F1) . a) * ((nat_hom F1) . b) by GROUP_6:def 7
.= (a * F1) * (b * F1) by A1, A2, GROUP_6:24 ; :: thesis: verum