let A be partial non-empty UAStr ; :: thesis: for i being Nat
for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
let i be Nat; :: thesis: for R being Relation of the carrier of A holds R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
let R be Relation of the carrier of A; :: thesis: R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A
consider F being ManySortedSet of NAT such that
A1: R |^ (A,i) = F . i and
A2: F . 0 = R and
A3: for i being Nat
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A by Def6;
F . (i + 1) = (R |^ (A,i)) |^ A by A1, A3;
hence R |^ (A,(i + 1)) = (R |^ (A,i)) |^ A by A2, A3, Def6; :: thesis: verum