let X be set ; :: thesis: for l being Element of MapsC X holds l = [[(dom l),(cod l)],(l `2)]
let l be Element of MapsC X; :: thesis: l = [[(dom l),(cod l)],(l `2)]
consider g being Element of FuncsC X, C1, C2 being Element of CSp X such that
A1: 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;
[C1,C2] = l `1 by A1, MCART_1:def 1;
then l `1 = [(dom l),(cod l)] by MCART_1:8;
hence l = [[(dom l),(cod l)],(l `2)] by A1, MCART_1:8; :: thesis: verum