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:121; :: 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:11;
hence x in FuncsT X by A5, TARSKI:def 4; :: thesis: verum