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 Th37;
T `2 = {} X by MCART_1:def 2;
then A1: id ({} X) in Funcs (T `2 ),(T `2 ) by FUNCT_2:12;
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

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