let UN be Universe; :: thesis: for V being non empty Element of UN holds Funcs V is Subset of UN
let V be non empty Element of UN; :: thesis: Funcs V is Subset of UN

now :: thesis: for o being object st o in { (Funcs (A,B)) where A, B is Element of V : verum } holds
o in UN

let o be object ; :: thesis: ( o in { (Funcs (A,B)) where A, B is Element of V : verum } implies o in UN )
assume o in { (Funcs (A,B)) where A, B is Element of V : verum } ; :: thesis: o in UN
then consider A, B being Element of V such that
A1: o = Funcs (A,B) ;
A2: UN is axiom_GU1 ;
reconsider A = A, B = B as Element of UN by A2;
Funcs (A,B) in UN ;
hence o in UN by A1; :: thesis: verum

end;

then { (Funcs (A,B)) where A, B is Element of V : verum } c= UN ;
then union { (Funcs (A,B)) where A, B is Element of V : verum } c= union UN by ZFMISC_1:77;
hence Funcs V is Subset of UN by Th81; :: thesis: verum