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 A1: X c= Y ; :: thesis: for x being set st x in dom ((f | X) " ) holds
((f | X) " ) . x = ((f | Y) " ) . x
let x be set ; :: thesis: ( x in dom ((f | X) " ) implies ((f | X) " ) . x = ((f | Y) " ) . x )
assume B1: x in dom ((f | X) " ) ; :: thesis: ((f | X) " ) . x = ((f | Y) " ) . x
C1: f | X c= f | Y by A1, RELAT_1:104;
D1: (f | X) ~ c= (f | Y) ~ by C1, SYSREL:27;
E1a: f | X is one-to-one by FUNCT_1:84;
E1: (f | X) ~ = (f | X) " by E1a, FUNCT_1:def 9;
F1a: f | Y is one-to-one by FUNCT_1:84;
F1: (f | Y) ~ = (f | Y) " by F1a, FUNCT_1:def 9;
thus ((f | X) " ) . x = ((f | Y) " ) . x by B1, D1, E1, F1, GRFUNC_1:8; :: thesis: verum