let X, Y be set ; :: thesis: Union (X --> Y) c= Y
let x be object ; :: 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 and
A2: Z in rng (X --> Y) by TARSKI:def 4;
ex z being object st
( z in dom (X --> Y) & Z = (X --> Y) . z ) by A2, FUNCT_1:def 3;
hence x in Y by A1, FUNCOP_1:7; :: thesis: verum