let G1, G2 be Group; :: thesis:
let H1 be Subgroup of G1; :: thesis:
let K be Subgroup of H1; :: thesis:
let H2 be Subgroup of G2; :: thesis:
let f be Homomorphism of G1,G2; :: thesis:
let g be Homomorphism of H1,H2; :: thesis:
assume A1: for k being Element of G1 st k in K holds
f . k = g . k ; :: thesis:
A2: ( Image (f | K) is strict Subgroup of G2 & Image (g | K) is strict Subgroup of G2 ) by GROUP_2:56;
for y being object holds
( y in the carrier of (Image (f | K)) iff y in the carrier of (Image (g | K)) )

let y be object ; :: thesis:
thus ( y in the carrier of (Image (f | K)) implies y in the carrier of (Image (g | K)) ) :: thesis:

assume y in the carrier of (Image (f | K)) ; :: thesis:
then consider h being Element of K such that
B1: (f | K) . h = y by STRUCT_0:def 5, GROUP_6:45;
B2: ( h is Element of G1 & h is Element of H1 & h in K ) by GROUP_2:42;
f . h = g . h by A1, B2
.= (g | K) . h by B2, Th1 ;
then (g | K) . h = (f | K) . h by B2, Th1
.= y by B1 ;
hence y in the carrier of (Image (g | K)) by STRUCT_0:def 5, GROUP_6:45; :: thesis:

end;

thus ( y in the carrier of (Image (g | K)) implies y in the carrier of (Image (f | K)) ) :: thesis:

assume y in the carrier of (Image (g | K)) ; :: thesis:
then consider h being Element of K such that
C1: (g | K) . h = y by STRUCT_0:def 5, GROUP_6:45;
C2: ( h is Element of H1 & h is Element of G1 & h in K ) by GROUP_2:42;
g . h = f . h by A1, C2
.= (f | K) . h by C2, Th1 ;
then (f | K) . h = (g | K) . h by C2, Th1
.= y by C1 ;
hence y in the carrier of (Image (f | K)) by STRUCT_0:def 5, GROUP_6:45; :: thesis:

end;