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;
hence
( not FuncsT X is empty & FuncsT X is functional )
by FUNCT_1:def 13; verum