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:75;
then A1: (f | X) ~ c= (f | Y) ~ by SYSREL:11;
f | X is one-to-one by FUNCT_1:52;
then A2: (f | X) ~ = (f | X) " by FUNCT_1:def 5;
f | Y is one-to-one by FUNCT_1:52;
then A3: (f | Y) ~ = (f | Y) " by FUNCT_1:def 5;
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:2; :: thesis: verum