theorem Th26: :: YELLOW_1:26

for J being RelStr-yielding ManySortedSet of {} holds product J = RelStr(# {{}},(id {{}}) #)