let x, y be object ; :: according to FUNCT_1:def 10 :: thesis: ( not x in proj1 (f | X) or not y in proj1 (f | X) or (f | X) . x = (f | X) . y )
A1: dom (f | X) c= dom f by RELAT_1:60;
assume that
A2: x in dom (f | X) and
A3: y in dom (f | X) ; :: thesis: (f | X) . x = (f | X) . y
thus (f | X) . x = f . x by A2, FUNCT_1:47
.= f . y by A1, A2, A3, FUNCT_1:def 10
.= (f | X) . y by A3, FUNCT_1:47 ; :: thesis: verum