let f be Function; for A being set st A c= bool (dom f) holds
(" f) " A c= (.: f) .: A
let A be set ; ( A c= bool (dom f) implies (" f) " A c= (.: f) .: A )
assume A1:
A c= bool (dom f)
; (" 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 A2:
y in (" f) " A
; y in (.: f) .: A
then A3:
(" f) . y in A
by FUNCT_1:def 7;
y in dom (" f)
by A2, FUNCT_1:def 7;
then A4:
y in bool (rng f)
by Def2;
then A5:
f " yy in A
by A3, Def2;
then
f " yy in bool (dom f)
by A1;
then A6:
f " yy in dom (.: f)
by Def1;
f .: (f " yy) = y
by A4, FUNCT_1:77;
then A7:
(.: f) . (f " yy) = y
by A1, A5, Def1;
f " yy in A
by A3, A4, Def2;
hence
y in (.: f) .: A
by A7, A6, FUNCT_1:def 6; verum