let f be Function; :: thesis: for A being set st f is one-to-one & A c= dom f holds
(f " ) .: (f .: A) = A
let A be set ; :: thesis: ( f is one-to-one & A c= dom f implies (f " ) .: (f .: A) = A )
set B = f .: A;
assume that
A1: f is one-to-one and
A2: A c= dom f ; :: thesis: (f " ) .: (f .: A) = A
A3: (f " ) .: (f .: A) c= A

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (f " ) .: (f .: A) or y in A )
assume y in (f " ) .: (f .: A) ; :: thesis: y in A
then consider x being set such that
x in dom (f " ) and
A4: x in f .: A and
A5: y = (f " ) . x by FUNCT_1:def 12;
ex y2 being set st
( y2 in dom f & y2 in A & x = f . y2 ) by A4, FUNCT_1:def 12;
hence y in A by A1, A5, FUNCT_1:54; :: thesis: verum

end;

A c= (f " ) .: (f .: A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (f " ) .: (f .: A) )
assume A6: x in A ; :: thesis: x in (f " ) .: (f .: A)
set y0 = f . x;
A7: (f " ) . (f . x) = x by A1, A2, A6, FUNCT_1:56;
f . x in rng f by A2, A6, FUNCT_1:12;
then A8: f . x in dom (f " ) by A1, FUNCT_1:55;
f . x in f .: A by A2, A6, FUNCT_1:def 12;
hence x in (f " ) .: (f .: A) by A7, A8, FUNCT_1:def 12; :: thesis: verum

end;

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