let f be Function; for A being set st f is one-to-one holds
(.: f) .: A c= (" f) " A
let A be set ; ( f is one-to-one implies (.: f) .: A c= (" f) " A )
assume A1:
f is one-to-one
; (.: f) .: A c= (" f) " A
let y be object ; TARSKI:def 3 ( not y in (.: f) .: A or y in (" f) " A )
reconsider yy = y as set by TARSKI:1;
assume
y in (.: f) .: A
; y in (" f) " A
then consider x being object such that
A2:
x in dom (.: f)
and
A3:
x in A
and
A4:
y = (.: f) . x
by FUNCT_1:def 6;
reconsider x = x as set by TARSKI:1;
A5:
x in bool (dom f)
by A2, Def1;
then A6:
y = f .: x
by A4, Def1;
then A7:
x c= f " yy
by A5, FUNCT_1:76;
A8:
yy c= rng f
by A6, RELAT_1:111;
then
y in bool (rng f)
;
then A9:
y in dom (" f)
by Def2;
f " yy c= x
by A1, A6, FUNCT_1:82;
then
f " yy in A
by A3, A7, XBOOLE_0:def 10;
then
(" f) . y in A
by A8, Def2;
hence
y in (" f) " A
by A9, FUNCT_1:def 7; verum