reconsider A = bool X as Subset-Family of X ;
A is Coherence_Space by Th2;
then A in { x where x is Subset-Family of X : x is Coherence_Space } ;
then reconsider A = A as Element of CSp X ;
set F = { (Funcs (union T),(union TT)) where T, TT is Element of CSp X : verum } ;
( id (union A) in Funcs (union A),(union A) & Funcs (union A),(union A) in { (Funcs (union T),(union TT)) where T, TT is Element of CSp X : verum } ) by FUNCT_2:12;
then reconsider UF = union { (Funcs (union T),(union TT)) where T, TT is Element of CSp X : verum } as non empty set by 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
A1: f in C and
A2: C in { (Funcs (union T),(union TT)) where T, TT is Element of CSp X : verum } by TARSKI:def 4;
ex A, B being Element of CSp X st C = Funcs (union A),(union B) by A2;
hence f is Function by A1; :: thesis: verum

end;

hence ( not FuncsC X is empty & FuncsC X is functional ) by FUNCT_1:def 19; :: thesis: verum