set B = (dom f) /\ A;
consider p being Function such that
A1: rng p = (dom f) /\ A and
A2: dom p in omega by Def1;
take f * p ; :: according to FINSET_1:def 1 :: thesis: ( rng (f * p) = f .: A & dom (f * p) in omega )
rng (f * p) = f .: ((dom f) /\ A) by A1, RELAT_1:127;
hence rng (f * p) = f .: A by RELAT_1:112; :: thesis: dom (f * p) in omega
thus dom (f * p) in omega by A1, A2, RELAT_1:27, XBOOLE_1:17; :: thesis: verum