let B be set ; :: thesis: for f being Function holds union ((" f) .: B) c= f " (union B)
let f be Function; :: thesis: union ((" f) .: B) c= f " (union B)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union ((" f) .: B) or x in f " (union B) )
assume x in union ((" f) .: B) ; :: thesis: x in f " (union B)
then consider X being set such that
A1: x in X and
A2: X in (" f) .: B by TARSKI:def 4;
consider Y being set such that
A3: Y in dom (" f) and
A4: Y in B and
A5: X = (" f) . Y by A2, FUNCT_1:def 12;
A6: (" f) . Y = f " Y by A3, Th24;
Y in bool (rng f) by A3, Def2;
then A7: f .: X in B by A4, A5, A6, FUNCT_1:147;
A8: f " Y c= dom f by RELAT_1:167;
then f . x in f .: X by A1, A5, A6, FUNCT_1:def 12;
then f . x in union B by A7, TARSKI:def 4;
hence x in f " (union B) by A1, A5, A6, A8, FUNCT_1:def 13; :: thesis: verum