set F = { (Funcs A,B) where A, B is Element of V : verum } ;
consider A being Element of V;
( id A in Funcs A,A & Funcs A,A in { (Funcs A,B) where A, B is Element of V : verum } ) by FUNCT_2:12;
then reconsider UF = union { (Funcs A,B) where A, B is Element of V : verum } as non empty set by TARSKI:def 4;

now

let f be set ; :: thesis: ( f in UF implies f is Function )
assume f in UF ; :: thesis: f is Function
then consider C being set such that
A1: f in C and
A2: C in { (Funcs A,B) where A, B is Element of V : verum } by TARSKI:def 4;
ex A, B being Element of V st C = Funcs A,B by A2;
hence f is Function by A1; :: thesis: verum

end;

hence ( Funcs V is functional & not Funcs V is empty ) by FUNCT_1:def 19; :: thesis: verum