theorem Th21: :: COH_SP:21

for X being set
for l being Element of MapsC X holds
( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l ) )