let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (f + c) or not y in dom (f + c) or not (f + c) . x = (f + c) . y or x = y )
assume that
A1: ( x in dom (f + c) & y in dom (f + c) ) and
A2: (f + c) . x = (f + c) . y ; :: thesis: x = y
A3: dom (f + c) = dom f by VALUED_1:def 2;
( (f + c) . x = (f . x) + c & (f + c) . y = (f . y) + c ) by A1, VALUED_1:def 2;
hence x = y by A1, A3, A2, FUNCT_1:def 4; :: thesis: verum