theorem Th13: :: WAYBEL_5:13

for y being object
for L being non empty RelStr
for F being Function-yielding Function holds
( ( y in rng (\// (F,L)) implies ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being object st
( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being object st
( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) )