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

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:23;
hence {(((l2 `2 ) * (l1 `2 )) . x),(((l2 `2 ) * (l1 `2 )) . y)} in cod l2 by A8, FUNCT_1:23; :: 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:19;
hence [[(dom l1),(cod l2)],((l2 `2 ) * (l1 `2 ))] is Element of MapsC X by A1, A3, A2, A5, Th19; :: thesis: verum