let g1, g2 be Function of (R / (ker f)),(Image f); :: thesis: ( ( for a being Element of R holds g1 . (Class ((EqRel (R,(ker f))),a)) = f . a ) & ( for a being Element of R holds g2 . (Class ((EqRel (R,(ker f))),a)) = f . a ) implies g1 = g2 )
assume that
A1: for a being Element of R holds g1 . (Class ((EqRel (R,(ker f))),a)) = f . a and
A2: for a being Element of R holds g2 . (Class ((EqRel (R,(ker f))),a)) = f . a ; :: thesis: g1 = g2
A: dom g1 = the carrier of (R / (ker f)) by FUNCT_2:def 1
.= dom g2 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 x in dom g1 ; :: thesis: g1 . x = g2 . x
then reconsider x1 = x as Element of (R / (ker f)) ;
consider b being Element of R such that
B1: x1 = Class ((EqRel (R,(ker f))),b) by RING_1:11;
thus g1 . x = f . b by B1, A1
.= g2 . x by B1, A2 ; :: thesis: verum
end;
hence g1 = g2 by A; :: thesis: verum