let f be one-to-one Function; :: thesis: for X, Y being set st X c= Y holds
for x being set st x in dom ((f | X) " ) holds
((f | X) " ) . x = ((f | Y) " ) . x
let X, Y be set ; :: thesis: ( X c= Y implies for x being set st x in dom ((f | X) " ) holds
((f | X) " ) . x = ((f | Y) " ) . x )
assume X c= Y ; :: thesis: for x being set st x in dom ((f | X) " ) holds
((f | X) " ) . x = ((f | Y) " ) . x
then f | X c= f | Y by RELAT_1:104;
then A1: (f | X) ~ c= (f | Y) ~ by SYSREL:27;
f | X is one-to-one by FUNCT_1:84;
then A2: (f | X) ~ = (f | X) " by FUNCT_1:def 9;
f | Y is one-to-one by FUNCT_1:84;
then A3: (f | Y) ~ = (f | Y) " by FUNCT_1:def 9;
let x be set ; :: thesis: ( x in dom ((f | X) " ) implies ((f | X) " ) . x = ((f | Y) " ) . x )
assume x in dom ((f | X) " ) ; :: thesis: ((f | X) " ) . x = ((f | Y) " ) . x
hence ((f | X) " ) . x = ((f | Y) " ) . x by A1, A2, A3, GRFUNC_1:8; :: thesis: verum