consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that
A2:
l = [[C1,C2],g]
and
( union C2 = {} implies union C1 = {} )
and
g is Function of (union C1),(union C2)
and
for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2
by Th18;
thus
(l `1) `2 is Element of CSp X
by A2; verum