let r be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r))
let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) )
assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r))
then A2: (Rotation (i,j,n,r)) * (Rotation (i,j,n,(- r))) = Rotation (i,j,n,(r + (- r))) by Th17
.= 1. (F_Real,n) by A1, Th18 ;
(Rotation (i,j,n,(- r))) * (Rotation (i,j,n,r)) = Rotation (i,j,n,((- r) + r)) by A1, Th17
.= 1. (F_Real,n) by A1, Th18 ;
then Rotation (i,j,n,r) is_reverse_of Rotation (i,j,n,(- r)) by A2, MATRIX_6:def 2;
hence (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) by MATRIX_6:def 4; :: thesis: verum