let A be partial non-empty UAStr ; :: thesis: for i being Element of NAT
for R being Relation of the carrier of A holds R |^ A,(i + 1) = (R |^ A,i) |^ A
let i be Element of 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 Element of NAT
for R being Relation of the carrier of A st R = F . i holds
F . (i + 1) = R |^ A by Def7;
F . (i + 1) = (R |^ A,i) |^ A by A1, A3;
hence R |^ A,(i + 1) = (R |^ A,i) |^ A by A2, A3, Def7; :: thesis: verum