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:9;
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 :: thesis: for f being object st f in UF holds
f is Function

let f be object ; :: 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 13; :: thesis: verum