:: deftheorem Def6 defines |^ PUA2MSS1:def 6 :
for A being partial non-empty UAStr
for R being Relation of the carrier of A
for i being Nat
for b₄ being Relation of the carrier of A holds
( b₄ = R |^ (A,i) iff ex F being ManySortedSet of NAT st
( b₄ = F . i & F . 0 = R & ( for i being Nat
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A ) ) );