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 & dom it2 = the carrier of G ) by FUNCT_2:def 1;
for x being set st x in dom it1 holds
it1 . x = it2 . x

proof

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

end;

hence it1 = it2 by A4, FUNCT_1:9; :: thesis: verum