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

now :: thesis: for f being set st f in UF holds
f is Function

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 ) ; :: thesis: verum