consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that
A1: ( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) ) by Th18;
thus for b₁ being set st b₁ = l `2 holds
( b₁ is Function-like & b₁ is Relation-like ) by A1; :: thesis: verum