let x, X be set ; :: thesis: ( x in FuncsC X iff ex C1, C2 being Element of CSp X st
( ( union C2 = {} implies union C1 = {} ) & x is Function of union C1, union C2 ) )
set F = { (Funcs (union xx),(union y)) where xx, y is Element of CSp X : verum } ;
thus ( x in FuncsC X implies ex C1, C2 being Element of CSp X st
( ( union C2 = {} implies union C1 = {} ) & x is Function of union C1, union C2 ) ) :: thesis: ( ex C1, C2 being Element of CSp X st
( ( union C2 = {} implies union C1 = {} ) & x is Function of union C1, union C2 ) implies x in FuncsC X )

proof

assume x in FuncsC X ; :: thesis: ex C1, C2 being Element of CSp X st
( ( union C2 = {} implies union C1 = {} ) & x is Function of union C1, union C2 )
then consider C being set such that
A1: x in C and
A2: C in { (Funcs (union xx),(union y)) where xx, y is Element of CSp X : verum } by TARSKI:def 4;
consider A, B being Element of CSp X such that
A3: C = Funcs (union A),(union B) by A2;
take A ; :: thesis: ex C2 being Element of CSp X st
( ( union C2 = {} implies union A = {} ) & x is Function of union A, union C2 )
take B ; :: thesis: ( ( union B = {} implies union A = {} ) & x is Function of union A, union B )
thus ( ( union B = {} implies union A = {} ) & x is Function of union A, union B ) by A1, A3, FUNCT_2:121; :: thesis: verum

end;

given A, B being Element of CSp X such that A4: ( ( union B = {} implies union A = {} ) & x is Function of union A, union B ) ; :: thesis: x in FuncsC X
A5: Funcs (union A),(union B) in { (Funcs (union xx),(union y)) where xx, y is Element of CSp X : verum } ;
x in Funcs (union A),(union B) by A4, FUNCT_2:11;
hence x in FuncsC X by A5, TARSKI:def 4; :: thesis: verum