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

now :: thesis: for x being object st x in the carrier of G holds
f . x = g . x

let x be object ; :: 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 = y * a by A5
.= g . x by A6 ; :: thesis: verum

end;

hence f = g ; :: thesis: verum