let f be one-to-one Function; :: thesis: for X being set holds
( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X )
let X be set ; :: thesis: ( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X )
( f | X is one-to-one & X |` f is one-to-one ) by FUNCT_1:52, FUNCT_1:58;
then ( f " = f ~ & (f | X) " = (f | X) ~ & (X |` f) " = (X |` f) ~ ) by FUNCT_1:def 5;
hence ( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X ) by Th2; :: thesis: verum