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)) )

set O1 = Rotation (i,j,n,r);

set O2 = Rotation (i,j,n,(- r));

set S = Seg n;

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: (Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r))

A2: Indices (Rotation (i,j,n,(- r))) = [:(Seg n),(Seg n):] by MATRIX_0:24;

A3: Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):] by MATRIX_0:24;

A4: Indices ((Rotation (i,j,n,r)) @) = [:(Seg n),(Seg n):] by MATRIX_0:24;

for k, m being Nat st [k,m] in [:(Seg n),(Seg n):] holds

((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

(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)) )

set O1 = Rotation (i,j,n,r);

set O2 = Rotation (i,j,n,(- r));

set S = Seg n;

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: (Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r))

A2: Indices (Rotation (i,j,n,(- r))) = [:(Seg n),(Seg n):] by MATRIX_0:24;

A3: Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):] by MATRIX_0:24;

A4: Indices ((Rotation (i,j,n,r)) @) = [:(Seg n),(Seg n):] by MATRIX_0:24;

for k, m being Nat st [k,m] in [:(Seg n),(Seg n):] holds

((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

proof

hence
(Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r))
by A4, MATRIX_0:27; :: thesis: verum
A5:
cos r = cos (- r)
by SIN_COS:31;

let k, m be Nat; :: thesis: ( [k,m] in [:(Seg n),(Seg n):] implies ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) )

A6: - (sin r) = sin (- r) by SIN_COS:31;

assume A7: [k,m] in [:(Seg n),(Seg n):] ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then A8: [m,k] in [:(Seg n),(Seg n):] by A3, A4, MATRIX_0:def 6;

then A9: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,r)) * (m,k) by A3, MATRIX_0:def 6;

end;let k, m be Nat; :: thesis: ( [k,m] in [:(Seg n),(Seg n):] implies ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) )

A6: - (sin r) = sin (- r) by SIN_COS:31;

assume A7: [k,m] in [:(Seg n),(Seg n):] ; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then A8: [m,k] in [:(Seg n),(Seg n):] by A3, A4, MATRIX_0:def 6;

then A9: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,r)) * (m,k) by A3, MATRIX_0:def 6;

per cases
( ( k = m & k = i ) or ( k = m & k = j ) or ( k = m & k <> i & k <> j ) or ( k <> m & k = i & m = j ) or ( k <> m & k = i & m <> j ) or ( k <> m & k = j & m = i ) or ( k <> m & k = j & m <> i ) or ( k <> m & k <> j & k <> i ) or ( k <> m & m <> j & m <> i ) )
;

end;

suppose A10:
( k = m & k = i )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
(Rotation (i,j,n,r)) * (m,k) = cos r
by A1, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A5, A9, A10, Def3; :: thesis: verum

end;hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A5, A9, A10, Def3; :: thesis: verum

suppose A11:
( k = m & k = j )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
(Rotation (i,j,n,r)) * (m,k) = cos r
by A1, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A5, A9, A11, Def3; :: thesis: verum

end;hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A5, A9, A11, Def3; :: thesis: verum

suppose A12:
( k = m & k <> i & k <> j )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
(Rotation (i,j,n,r)) * (m,k) = 1. F_Real
by A1, A3, A7, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A12, Def3; :: thesis: verum

end;hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A12, Def3; :: thesis: verum

suppose A13:
( k <> m & k = i & m = j )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
(Rotation (i,j,n,r)) * (m,k) = - (sin r)
by A1, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A6, A9, A13, Def3; :: thesis: verum

end;hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A6, A9, A13, Def3; :: thesis: verum

suppose A14:
( k <> m & k = i & m <> j )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
not m in {i,j}
by TARSKI:def 2;

then A15: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A14, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A14, A15, Def3; :: thesis: verum

end;then A15: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A14, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A14, A15, Def3; :: thesis: verum

suppose A16:
( k <> m & k = j & m = i )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
(Rotation (i,j,n,(- r))) * (k,m) = - (sin (- r))
by A1, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A6, A9, A16, Def3; :: thesis: verum

end;hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A6, A9, A16, Def3; :: thesis: verum

suppose A17:
( k <> m & k = j & m <> i )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
not m in {i,j}
by TARSKI:def 2;

then A18: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A17, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A17, A18, Def3; :: thesis: verum

end;then A18: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A17, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A17, A18, Def3; :: thesis: verum

suppose A19:
( k <> m & k <> j & k <> i )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
not k in {i,j}
by TARSKI:def 2;

then A20: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A19, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A19, A20, Def3; :: thesis: verum

end;then A20: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A19, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A19, A20, Def3; :: thesis: verum

suppose A21:
( k <> m & m <> j & m <> i )
; :: thesis: ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m)

then
not m in {i,j}
by TARSKI:def 2;

then A22: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A21, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A21, A22, Def3; :: thesis: verum

end;then A22: {m,k} <> {i,j} by TARSKI:def 2;

then (Rotation (i,j,n,r)) * (m,k) = 0. F_Real by A1, A3, A8, A21, Def3;

hence ((Rotation (i,j,n,r)) @) * (k,m) = (Rotation (i,j,n,(- r))) * (k,m) by A1, A2, A7, A9, A21, A22, Def3; :: thesis: verum