let A be partial non-empty UAStr ; 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 ; 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; R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j)
defpred S1[ Nat] means R |^ (A,(i + $1)) = (R |^ (A,i)) |^ (A,$1);
A1:
S1[ 0 ]
by Th15;
A2:
now for j being Nat st S1[j] holds
S1[j + 1]let j be
Nat;
( S1[j] implies S1[j + 1] )assume A3:
S1[
j]
;
S1[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
S1[
j + 1]
;
verum end;
for j being Nat holds S1[j]
from NAT_1:sch 2(A1, A2);
hence
R |^ (A,(i + j)) = (R |^ (A,i)) |^ (A,j)
; verum