let g1, g2 be Function of R,(R / I); :: thesis: ( ( for a being Element of R holds g1 . a = Class ((EqRel (R,I)),a) ) & ( for a being Element of R holds g2 . a = Class ((EqRel (R,I)),a) ) implies g1 = g2 )
assume that
A1: for a being Element of R holds g1 . a = Class ((EqRel (R,I)),a) and
A2: for a being Element of R holds g2 . a = Class ((EqRel (R,I)),a) ; :: thesis: g1 = g2
let x be Element of R; :: according to FUNCT_2:def 8 :: thesis: g1 . x = g2 . x
thus g1 . x = Class ((EqRel (R,I)),x) by A1
.= g2 . x by A2 ; :: thesis: verum