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

( (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