let A be partial non-empty UAStr ; :: thesis: for R being Relation of the carrier of A holds
( R |^ (A,0) = R & R |^ (A,1) = R |^ A )
let R be Relation of the carrier of A; :: thesis: ( R |^ (A,0) = R & R |^ (A,1) = R |^ A )
consider F being ManySortedSet of NAT such that
R |^ (A,0) = F . 0 and
A1: F . 0 = R and
A2: 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 . (0 + 1) = R |^ A by A1, A2;
hence ( R |^ (A,0) = R & R |^ (A,1) = R |^ A ) by A1, A2, Def6; :: thesis: verum