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:66; :: 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:8;
hence x in FuncsC X by A5, TARSKI:def 4; :: thesis: verum