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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (.: f) " B or x in (" f) .: B )
reconsider xx = x as set by TARSKI:1;
A3: f .: xx c= rng f by RELAT_1:111;
then f .: xx in bool (rng f) ;
then A4: f .: xx in dom (" f) by Def2;
assume A5: x in (.: f) " B ; :: thesis: x in (" f) .: B
then A6: x in dom (.: f) by FUNCT_1:def 7;
then x in bool (dom f) by Def1;
then A7: xx c= f " (f .: xx) by FUNCT_1:76;
f " (f .: xx) c= xx by A1, FUNCT_1:82;
then x = f " (f .: xx) by A7, XBOOLE_0:def 10;
then A8: x = (" f) . (f .: xx) by A3, Def2;
(.: f) . x in B by A5, FUNCT_1:def 7;
then f .: xx in B by A6, Th7;
hence x in (" f) .: B by A8, A4, FUNCT_1:def 6; :: thesis: verum

end;

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