theorem Th16: :: PUA2MSS1:17

for A being partial non-empty UAStr
for i being Nat
for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A