let B be set ; :: thesis: for f being Function st B c= bool (rng f) holds
union ((" f) .: B) = f " (union B)
let f be Function; :: thesis: ( B c= bool (rng f) implies union ((" f) .: B) = f " (union B) )
assume A1: B c= bool (rng f) ; :: thesis: union ((" f) .: B) = f " (union B)
A2: f " (union B) c= union ((" f) .: B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f " (union B) or x in union ((" f) .: B) )
assume A3: x in f " (union B) ; :: thesis: x in union ((" f) .: B)
then f . x in union B by FUNCT_1:def 7;
then consider Y being set such that
A4: f . x in Y and
A5: Y in B by TARSKI:def 4;
x in dom f by A3, FUNCT_1:def 7;
then A6: x in f " Y by A4, FUNCT_1:def 7;
Y in bool (rng f) by A1, A5;
then A7: Y in dom (" f) by Def2;
(" f) . Y = f " Y by A1, A5, Def2;
then f " Y in (" f) .: B by A5, A7, FUNCT_1:def 6;
hence x in union ((" f) .: B) by A6, TARSKI:def 4; :: thesis: verum

end;

union ((" f) .: B) c= f " (union B) by Th25;
hence union ((" f) .: B) = f " (union B) by A2, XBOOLE_0:def 10; :: thesis: verum