let X, Y be non empty set ; :: thesis: for y being Element of Y holds [:X,{y}:] c= union (Funcs (X,Y))
let y be Element of Y; :: thesis: [:X,{y}:] c= union (Funcs (X,Y))
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in [:X,{y}:] or o in union (Funcs (X,Y)) )
assume o in [:X,{y}:] ; :: thesis: o in union (Funcs (X,Y))
then ( o in X --> y & X --> y in Funcs (X,Y) ) by FUNCT_2:8;
hence o in union (Funcs (X,Y)) by TARSKI:def 4; :: thesis: verum