let T, S be 1-sorted ; :: thesis: for f being Function of T,S
for P1 being Subset of S st rng f = [#] S & f is one-to-one holds
f " P1 = (f ") .: P1
let f be Function of T,S; :: thesis: for P1 being Subset of S st rng f = [#] S & f is one-to-one holds
f " P1 = (f ") .: P1
let P1 be Subset of S; :: thesis: ( rng f = [#] S & f is one-to-one implies f " P1 = (f ") .: P1 )
assume rng f = [#] S ; :: thesis: ( not f is one-to-one or f " P1 = (f ") .: P1 )
then A1: f is onto by FUNCT_2:def 3;
assume A2: f is one-to-one ; :: thesis: f " P1 = (f ") .: P1
f " P1 = (f ") .: P1 by A2, FUNCT_1:85;
hence f " P1 = (f ") .: P1 by A1, A2, Def4; :: thesis: verum