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

(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