theorem Th17: :: COH_SP:17

for x, X being set holds
( 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) ) )