A2: ( union (cod l2) <> {} or union (dom l2) = {} ) by Th21;
A3: ( union (cod l1) <> {} or union (dom l1) = {} ) by Th21;
A4: l1 `2 is Function of (union (dom l1)),(union (cod l1)) by Th21;

A5: now :: thesis: for x, y being set st {x,y} in dom l1 holds
{(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2

let x, y be set ; :: thesis: ( {x,y} in dom l1 implies {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2 )
assume A6: {x,y} in dom l1 ; :: thesis: {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2
then x in union (dom l1) by Th16;
then A7: x in dom (l1 `2) by A3, A4, FUNCT_2:def 1;
y in union (dom l1) by A6, Th16;
then A8: y in dom (l1 `2) by A3, A4, FUNCT_2:def 1;
{((l1 `2) . x),((l1 `2) . y)} in cod l1 by A6, Th21;
then {((l2 `2) . ((l1 `2) . x)),((l2 `2) . ((l1 `2) . y))} in cod l2 by A1, Th21;
then {(((l2 `2) * (l1 `2)) . x),((l2 `2) . ((l1 `2) . y))} in cod l2 by A7, FUNCT_1:13;
hence {(((l2 `2) * (l1 `2)) . x),(((l2 `2) * (l1 `2)) . y)} in cod l2 by A8, FUNCT_1:13; :: thesis: verum

end;

l2 `2 is Function of (union (dom l2)),(union (cod l2)) by Th21;
then (l2 `2) * (l1 `2) is Function of (union (dom l1)),(union (cod l2)) by A1, A3, A4, FUNCT_2:13;
hence [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X by A1, A3, A2, A5, Th19; :: thesis: verum