let G1, G2 be Group; :: thesis: for H being Subgroup of G1
for a being Element of G1
for f being Homomorphism of G1,G2 holds f .: (H * a) = (f .: H) * (f . a)
let H be Subgroup of G1; :: thesis: for a being Element of G1
for f being Homomorphism of G1,G2 holds f .: (H * a) = (f .: H) * (f . a)
let a be Element of G1; :: thesis: for f being Homomorphism of G1,G2 holds f .: (H * a) = (f .: H) * (f . a)
let f be Homomorphism of G1,G2; :: thesis: f .: (H * a) = (f .: H) * (f . a)
A1: dom f = the carrier of G1 by FUNCT_2:def 1;
for y being object st y in f .: (H * a) holds
y in (f .: H) * (f . a)

proof

let y be object ; :: thesis: ( y in f .: (H * a) implies y in (f .: H) * (f . a) )
assume y in f .: (H * a) ; :: thesis: y in (f .: H) * (f . a)
then consider x being object such that
B1: ( x in the carrier of G1 & x in H * a ) and
B2: y = f . x by A1, FUNCT_1:def 6;
consider h being Element of G1 such that
B3: ( x = h * a & h in H ) by B1, GROUP_2:104;
( dom f = the carrier of G1 & h in H & h in G1 ) by FUNCT_2:def 1, B3;
then f . h in f .: the carrier of H by FUNCT_1:def 6;
then f . h in f .: H by GRSOLV_1:8;
then (f . h) * (f . a) in (f .: H) * (f . a) by GROUP_2:104;
hence y in (f .: H) * (f . a) by B2, B3, GROUP_6:def 6; :: thesis: verum

end;

then A2: f .: (H * a) c= (f .: H) * (f . a) ;
for y being object st y in (f .: H) * (f . a) holds
y in f .: (H * a)

proof

let y be object ; :: thesis: ( y in (f .: H) * (f . a) implies y in f .: (H * a) )
assume y in (f .: H) * (f . a) ; :: thesis: y in f .: (H * a)
then consider g being Element of G2 such that
B1: y = g * (f . a) and
B2: g in f .: H by GROUP_2:104;
g in Image (f | H) by B2, GRSOLV_1:def 3;
then consider x being Element of H such that
B3: g = (f | H) . x by GROUP_6:45;
B4: ( x in H & x is Element of G1 ) by GROUP_2:42;
reconsider x = x as Element of G1 by GROUP_2:42;
B5: y = g * (f . a) by B1
.= (f . x) * (f . a) by B3, B4, Th1
.= f . (x * a) by GROUP_6:def 6 ;
( x * a in the carrier of G1 & dom f = the carrier of G1 ) by FUNCT_2:def 1;
then ( x * a in dom f & x * a in H * a & y = f . (x * a) ) by B4, B5, GROUP_2:104;
hence y in f .: (H * a) by FUNCT_1:def 6; :: thesis: verum

end;

then (f .: H) * (f . a) c= f .: (H * a) ;
hence f .: (H * a) = (f .: H) * (f . a) by A2, XBOOLE_0:def 10; :: thesis: verum