theorem :: PUA2MSS1:18

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