let x, X be set ; :: thesis: ( x in FuncsT X iff ex T1, T2 being Element of TOL X st
( ( T2 `2 = {} implies T1 `2 = {} ) & x is Function of (T1 `2),(T2 `2) ) )
set F = { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;
thus ( x in FuncsT X implies ex A, B being Element of TOL X st
( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) ) :: thesis: ( ex T1, T2 being Element of TOL X st
( ( T2 `2 = {} implies T1 `2 = {} ) & x is Function of (T1 `2),(T2 `2) ) implies x in FuncsT X )

proof

assume x in FuncsT X ; :: thesis: ex A, B being Element of TOL X st
( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) )
then consider C being set such that
A1: x in C and
A2: C in { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } by TARSKI:def 4;
consider A, B being Element of TOL X such that
A3: C = Funcs ((A `2),(B `2)) by A2;
take A ; :: thesis: ex B being Element of TOL X st
( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) )
take B ; :: thesis: ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) )
thus ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) by A1, A3, FUNCT_2:66; :: thesis: verum

end;

given A, B being Element of TOL X such that A4: ( ( B `2 = {} implies A `2 = {} ) & x is Function of (A `2),(B `2) ) ; :: thesis: x in FuncsT X
A5: Funcs ((A `2),(B `2)) in { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;
x in Funcs ((A `2),(B `2)) by A4, FUNCT_2:8;
hence x in FuncsT X by A5, TARSKI:def 4; :: thesis: verum