for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Rotation (i,j,n,0) = 1. (F_Real,n)