let H, G be Group; :: thesis: for x being set
for g being Homomorphism of G,H holds
( x in Image g iff ex a being Element of G st x = g . a )
let x be set ; :: thesis: for g being Homomorphism of G,H holds
( x in Image g iff ex a being Element of G st x = g . a )
let g be Homomorphism of G,H; :: thesis: ( x in Image g iff ex a being Element of G st x = g . a )
thus ( x in Image g implies ex a being Element of G st x = g . a ) :: thesis: ( ex a being Element of G st x = g . a implies x in Image g )

proof

assume x in Image g ; :: thesis: ex a being Element of G st x = g . a
then x in the carrier of (Image g) by STRUCT_0:def 5;
then x in g .: the carrier of G by Def11;
then consider y being set such that
y in dom g and
A1: y in the carrier of G and
A2: g . y = x by FUNCT_1:def 12;
reconsider y = y as Element of G by A1;
take y ; :: thesis: x = g . y
thus x = g . y by A2; :: thesis: verum

end;

given a being Element of G such that A3: x = g . a ; :: thesis: x in Image g
the carrier of G = dom g by FUNCT_2:def 1;
then x in g .: the carrier of G by A3, FUNCT_1:def 12;
then x in the carrier of (Image g) by Def11;
hence x in Image g by STRUCT_0:def 5; :: thesis: verum