let B be set ; :: thesis: for f being Function st f is one-to-one holds
(" f) .: B = (.: f) " B
let f be Function; :: thesis: ( f is one-to-one implies (" f) .: B = (.: f) " B )
assume A1: f is one-to-one ; :: thesis: (" f) .: B = (.: f) " B
A2: (" f) .: B c= (.: f) " B by Th33;
(.: f) " B c= (" f) .: B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (.: f) " B or x in (" f) .: B )
assume x in (.: f) " B ; :: thesis: x in (" f) .: B
then A3: ( x in dom (.: f) & (.: f) . x in B ) by FUNCT_1:def 13;
then x in bool (dom f) by Def1;
then ( x c= f " (f .: x) & f " (f .: x) c= x & f .: x c= rng f ) by A1, FUNCT_1:146, FUNCT_1:152, RELAT_1:144;
then ( x = f " (f .: x) & f .: x in bool (rng f) ) by XBOOLE_0:def 10;
then ( x = (" f) . (f .: x) & f .: x in dom (" f) & f .: x in B ) by A3, Def2, Th8;
hence x in (" f) .: B by FUNCT_1:def 12; :: thesis: verum

end;

hence (" f) .: B = (.: f) " B by A2, XBOOLE_0:def 10; :: thesis: verum