theorem :: YELLOW_1:27

for Y being RelStr holds Y |^ {} = RelStr(# {{}},(id {{}}) #) by Th26;