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 set ; TARSKI:def 3 ( not y in (.: f) .: A or y in (" f) " A )
assume
y in (.: f) .: A
; y in (" f) " A
then consider x being set such that
A2:
x in dom (.: f)
and
A3:
x in A
and
A4:
y = (.: f) . x
by FUNCT_1:def 12;
A5:
x in bool (dom f)
by A2, Def1;
then A6:
y = f .: x
by A4, Def1;
then A7:
x c= f " y
by A5, FUNCT_1:146;
A8:
y c= rng f
by A6, RELAT_1:144;
then
y in bool (rng f)
;
then A9:
y in dom (" f)
by Def2;
f " y c= x
by A1, A6, FUNCT_1:152;
then
f " y 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 13; verum