set F = { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;
reconsider T = [(Total ({} X)),({} X)] as Element of TOL X by Th35;
A1: id ({} X) in Funcs ((T `2),(T `2)) by FUNCT_2:9;
Funcs ((T `2),(T `2)) in { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;
then reconsider UF = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } as non empty set by A1, TARSKI:def 4;

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

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

end;

hence ( not FuncsT X is empty & FuncsT X is functional ) by FUNCT_1:def 13; :: thesis: verum