let x, y be set ; :: according to FUNCT_1:def 16 :: thesis: ( not x in dom (f | X) or not y in dom (f | X) or (f | X) . x = (f | X) . y )
F: dom (f | X) c= dom f by RELAT_1:89;
assume Z: ( x in dom (f | X) & y in dom (f | X) ) ; :: thesis: (f | X) . x = (f | X) . y
hence (f | X) . x = f . x by FUNCT_1:70
.= f . y by Z, F, FUNCT_1:def 16
.= (f | X) . y by Z, FUNCT_1:70 ;
:: thesis: verum