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

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