theorem Th42: :: COH_SP:43

for X being set
for m being Element of MapsT X holds
( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )