let it1, it2 be Function of the carrier of G,(con_class a); :: thesis: ( ( for x being Element of G holds it1 . x = a |^ x ) & ( for x being Element of G holds it2 . x = a |^ x ) implies it1 = it2 )
assume that
A2: for x being Element of G holds it1 . x = a |^ x and
A3: for x being Element of G holds it2 . x = a |^ x ; :: thesis: it1 = it2
A4: dom it1 = the carrier of G by FUNCT_2:def 1;
A5: dom it2 = the carrier of G by FUNCT_2:def 1;
for x being object st x in dom it1 holds
it1 . x = it2 . x

proof

let x be object ; :: thesis: ( x in dom it1 implies it1 . x = it2 . x )
assume x in dom it1 ; :: thesis: it1 . x = it2 . x
then reconsider y = x as Element of G ;
it1 . y = a |^ y by A2;
hence it1 . x = it2 . x by A3; :: thesis: verum

end;

hence it1 = it2 by A4, A5; :: thesis: verum