let f, g be Function of G,G; :: thesis: ( ( for x being Element of G holds f . x = a * x ) & ( for x being Element of G holds g . x = a * x ) implies f = g )
assume that
A2: for x being Element of G holds f . x = a * x and
A3: for x being Element of G holds g . x = a * x ; :: thesis: f = g

now

let x be set ; :: thesis: ( x in the carrier of G implies f . x = g . x )
assume x in the carrier of G ; :: thesis: f . x = g . x
then reconsider y = x as Element of G ;
thus f . x = a * y by A2
.= g . x by A3 ; :: thesis: verum

end;

hence f = g by FUNCT_2:12; :: thesis: verum