let G1, G2, G3 be Group; :: thesis: for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for A being Subgroup of G1 holds multMagma(# the carrier of (f2 .: (f1 .: A)), the multF of (f2 .: (f1 .: A)) #) = multMagma(# the carrier of ((f2 * f1) .: A), the multF of ((f2 * f1) .: A) #)
let f1 be Homomorphism of G1,G2; :: thesis: for f2 being Homomorphism of G2,G3
for A being Subgroup of G1 holds multMagma(# the carrier of (f2 .: (f1 .: A)), the multF of (f2 .: (f1 .: A)) #) = multMagma(# the carrier of ((f2 * f1) .: A), the multF of ((f2 * f1) .: A) #)
let f2 be Homomorphism of G2,G3; :: thesis: for A being Subgroup of G1 holds multMagma(# the carrier of (f2 .: (f1 .: A)), the multF of (f2 .: (f1 .: A)) #) = multMagma(# the carrier of ((f2 * f1) .: A), the multF of ((f2 * f1) .: A) #)
let A be Subgroup of G1; :: thesis: multMagma(# the carrier of (f2 .: (f1 .: A)), the multF of (f2 .: (f1 .: A)) #) = multMagma(# the carrier of ((f2 * f1) .: A), the multF of ((f2 * f1) .: A) #)
for z being Element of G3 holds
( z in f2 .: (f1 .: A) iff z in (f2 * f1) .: A )

proof

let z be Element of G3; :: thesis: ( z in f2 .: (f1 .: A) iff z in (f2 * f1) .: A )
thus ( z in f2 .: (f1 .: A) implies z in (f2 * f1) .: A ) :: thesis: ( z in (f2 * f1) .: A implies z in f2 .: (f1 .: A) )

proof

assume z in f2 .: (f1 .: A) ; :: thesis: z in (f2 * f1) .: A
then z in f2 .: the carrier of (f1 .: A) by GRSOLV_1:8;
then consider y being object such that
A2: y in dom f2 and
A3: y in the carrier of (f1 .: A) and
A4: z = f2 . y by FUNCT_1:def 6;
y in f1 .: the carrier of A by A3, GRSOLV_1:8;
then consider x being object such that
A5: ( x in dom f1 & x in the carrier of A & y = f1 . x ) by FUNCT_1:def 6;
A6: x in dom (f2 * f1) by A2, A5, FUNCT_1:11;
then ( x in the carrier of A & z = (f2 * f1) . x ) by A4, A5, FUNCT_1:12;
then z in (f2 * f1) .: the carrier of A by A6, FUNCT_1:def 6;
hence z in (f2 * f1) .: A by GRSOLV_1:8; :: thesis: verum

end;

thus ( z in (f2 * f1) .: A implies z in f2 .: (f1 .: A) ) :: thesis: verum

proof

assume z in (f2 * f1) .: A ; :: thesis: z in f2 .: (f1 .: A)
then z in (f2 * f1) .: the carrier of A by GRSOLV_1:8;
then consider x being object such that
A2: ( x in dom (f2 * f1) & x in the carrier of A & z = (f2 * f1) . x ) by FUNCT_1:def 6;
A3: ( x in dom f1 & f1 . x in dom f2 ) by A2, FUNCT_1:11;
set y = f1 . x;
( x in dom f1 & x in the carrier of A & f1 . x = f1 . x ) by A2, FUNCT_1:11;
then A5: f1 . x in f1 .: the carrier of A by FUNCT_1:def 6;
z = (f2 * f1) . x by A2
.= f2 . (f1 . x) by A2, FUNCT_1:12
.= f2 . (f1 . x) ;
then z in f2 .: (f1 .: the carrier of A) by A3, A5, FUNCT_1:def 6;
then z in f2 .: the carrier of (f1 .: A) by GRSOLV_1:8;
hence z in f2 .: (f1 .: A) by GRSOLV_1:8; :: thesis: verum

end;

end;

hence multMagma(# the carrier of (f2 .: (f1 .: A)), the multF of (f2 .: (f1 .: A)) #) = multMagma(# the carrier of ((f2 * f1) .: A), the multF of ((f2 * f1) .: A) #) by GROUP_2:60; :: thesis: verum