let B be set ; :: thesis: for f being Function holds (" f) .: B c= (.: f) " B
let f be Function; :: thesis: (" f) .: B c= (.: f) " B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (" f) .: B or x in (.: f) " B )
assume x in (" f) .: B ; :: thesis: x in (.: f) " B
then consider Y being set such that
A1: Y in dom (" f) and
A2: Y in B and
A3: x = (" f) . Y by FUNCT_1:def 6;
A4: (" f) . Y = f " Y by A1, Th24;
then A5: x c= dom f by A3, RELAT_1:132;
then x in bool (dom f) ;
then A6: x in dom (.: f) by Def1;
Y in bool (rng f) by A1, Def2;
then f .: x in B by A2, A3, A4, FUNCT_1:77;
then (.: f) . x in B by A5, Def1;
hence x in (.: f) " B by A6, FUNCT_1:def 7; :: thesis: verum