let g1, g2 be Function of (AbGr M),(AbGr N); :: thesis: ( ( for x being object st x in the carrier of (AbGr M) holds
g1 . x = f . x ) & ( for x being object st x in the carrier of (AbGr M) holds
g2 . x = f . x ) implies g1 = g2 )
assume that
A5: for x being object st x in the carrier of (AbGr M) holds
g1 . x = f . x and
A6: for x being object st x in the carrier of (AbGr M) holds
g2 . x = f . x ; :: thesis: g1 = g2
A7: dom g1 = the carrier of (AbGr M) by FUNCT_2:def 1;

now :: thesis: for x being object st x in dom g1 holds
g1 . x = g2 . x

let x be object ; :: thesis: ( x in dom g1 implies g1 . x = g2 . x )
assume A9: x in dom g1 ; :: thesis: g1 . x = g2 . x
hence g1 . x = f . x by A5
.= g2 . x by A6, A9 ;
:: thesis: verum

end;

hence g1 = g2 by A7; :: thesis: verum