let A be partial non-empty UAStr ; :: thesis: 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
let i, j be Element of NAT ; :: thesis: for R being Relation of the carrier of A holds R |^ A,(i + j) = (R |^ A,i) |^ A,j
let R be Relation of the carrier of A; :: thesis: R |^ A,(i + j) = (R |^ A,i) |^ A,j
defpred S₁[ Element of NAT ] means R |^ A,(i + $1) = (R |^ A,i) |^ A,$1;
A1: S₁[ 0 ] by Th17;

A2: now

let j be Element of NAT ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A3: S₁[j] ; :: thesis: S₁[j + 1]
R |^ A,(i + (j + 1)) = R |^ A,((i + j) + 1)
.= (R |^ A,(i + j)) |^ A by Th18
.= (R |^ A,i) |^ A,(j + 1) by A3, Th18 ;
hence S₁[j + 1] ; :: thesis: verum

end;

for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A1, A2);
hence R |^ A,(i + j) = (R |^ A,i) |^ A,j ; :: thesis: verum