theorem Th4: :: MSUALG_3:4

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds (id B) ** F = F