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 :: 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 = a + y by A2
.= g . x by A3 ; :: thesis: verum

end;

hence f = g ; :: thesis: verum