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

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