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₁[ Nat] means R |^ (A,(i + $1)) = (R |^ (A,i)) |^ (A,$1);
A1: S₁[ 0 ] by Th15;

A2: now :: thesis: for j being Nat st S₁[j] holds
S₁[j + 1]

let j be 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 Th16
.= (R |^ (A,i)) |^ (A,(j + 1)) by A3, Th16 ;
hence S₁[j + 1] ; :: thesis: verum

end;

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