let G, H be Group; :: thesis: for g being Homomorphism of G,H
for x being object holds
( x in Image g iff ex a being Element of G st x = g . a )
let g be Homomorphism of G,H; :: thesis: for x being object holds
( x in Image g iff ex a being Element of G st x = g . a )
let x be object ; :: 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) ;
then x in g .: the carrier of G by Def10;
then consider y being object such that
y in dom g and
A1: y in the carrier of G and
A2: g . y = x by FUNCT_1:def 6;
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 6;
then x in the carrier of (Image g) by Def10;
hence x in Image g ; :: thesis: verum