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 object ; :: 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;
dom (.: f) = bool (dom f) by Def1;
then A3: X in bool (dom f) by A2, FUNCT_1:def 7;
then A4: f . x in f .: X by A1, FUNCT_1:def 6;
(.: f) . X in B by A2, FUNCT_1:def 7;
then f .: X in B by A3, Def1;
then f . x in union B by A4, TARSKI:def 4;
hence x in f " (union B) by A1, A3, FUNCT_1:def 7; :: thesis: verum