let X, Y be set ; :: thesis: Union (X --> Y) c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (X --> Y) or x in Y )
assume x in Union (X --> Y) ; :: thesis: x in Y
then consider Z being set such that
A1: ( x in Z & Z in rng (X --> Y) ) by TARSKI:def 4;
A2: ex z being set st
( z in dom (X --> Y) & Z = (X --> Y) . z ) by A1, FUNCT_1:def 5;
thus x in Y by A1, A2, FUNCOP_1:13; :: thesis: verum