theorem LM01: :: PETRI_3:1

for I being set
for F, D, R being ManySortedSet of I st ( for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = D . i & rng f = R . i ) ) & ( for i, j being object
for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds
dom f misses dom g ) holds
ex G being Function st
( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )