let T, S be 1-sorted ; :: thesis: for f being Function of T,S
for P being Subset of T st rng f = [#] S & f is one-to-one holds
f .: P = (f " ) " P
let f be Function of T,S; :: thesis: for P being Subset of T st rng f = [#] S & f is one-to-one holds
f .: P = (f " ) " P
let P be Subset of T; :: thesis: ( rng f = [#] S & f is one-to-one implies f .: P = (f " ) " P )
assume A1: ( rng f = [#] S & f is one-to-one ) ; :: thesis: f .: P = (f " ) " P
then f .: P = (f " ) " P by FUNCT_1:154;
hence f .: P = (f " ) " P by A1, Def4; :: thesis: verum