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