theorem Th23: :: WAYBEL_2:23

for L being non empty RelStr
for x being Element of L
for F being non empty NetStr over L holds rng the mapping of (x "/\" F) = {x} "/\" (rng the mapping of F)