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