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

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

hence
it1 = it2
by A4, A5; :: thesis: verum
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;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