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;

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

hence
( Funcs V is functional & not Funcs V is empty )
; :: thesis: verumf 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;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