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 object ; :: 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 object such that
x in dom (f ") and
A4: x in f .: A and
A5: y = (f ") . x by Def6;
ex y2 being object st
( y2 in dom f & y2 in A & x = f . y2 ) by A4, Def6;
hence y in A by A1, A5, Th31; :: thesis: verum

end;

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

proof

let x be object ; :: 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, Th33;
f . x in rng f by A2, A6, Def3;
then A8: f . x in dom (f ") by A1, Th32;
f . x in f .: A by A2, A6, Def6;
hence x in (f ") .: (f .: A) by A7, A8, Def6; :: thesis: verum

end;

hence (f ") .: (f .: A) = A by A3; :: thesis: verum