let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies Rotation (i,j,n,0) = 1. (F_Real,n) )
set O = Rotation (i,j,n,0);
assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Rotation (i,j,n,0) = 1. (F_Real,n)
A2: for k, m being Nat st [k,m] in Indices (Rotation (i,j,n,0)) & k <> m holds
(Rotation (i,j,n,0)) * (k,m) = 0. F_Real

proof

let k, m be Nat; :: thesis: ( [k,m] in Indices (Rotation (i,j,n,0)) & k <> m implies (Rotation (i,j,n,0)) * (k,m) = 0. F_Real )
assume that
A3: [k,m] in Indices (Rotation (i,j,n,0)) and
A4: k <> m ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

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

suppose ( ( k = i & m = j ) or ( k = j & m = i ) ) ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then ( (Rotation (i,j,n,0)) * (k,m) = sin 0 or (Rotation (i,j,n,0)) * (k,m) = - (sin 0) ) by A1, Def3;
hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by SIN_COS:31; :: thesis: verum

end;

suppose ( k = i & m <> j ) ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then not m in {i,j} by A4, TARSKI:def 2;
then {k,m} <> {i,j} by TARSKI:def 2;
hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;

suppose ( k = j & m <> i ) ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then not m in {i,j} by A4, TARSKI:def 2;
then {k,m} <> {i,j} by TARSKI:def 2;
hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;

suppose ( m = i & k <> j ) ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then not k in {i,j} by A4, TARSKI:def 2;
then {k,m} <> {i,j} by TARSKI:def 2;
hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;

suppose ( m = j & k <> i ) ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then not k in {i,j} by A4, TARSKI:def 2;
then {k,m} <> {i,j} by TARSKI:def 2;
hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;

suppose ( k <> i & k <> j & m <> i & m <> j ) ; :: thesis: (Rotation (i,j,n,0)) * (k,m) = 0. F_Real

then not m in {i,j} by TARSKI:def 2;
then {k,m} <> {i,j} by TARSKI:def 2;
hence (Rotation (i,j,n,0)) * (k,m) = 0. F_Real by A1, A3, A4, Def3; :: thesis: verum

end;

end;

end;

for k being Nat st [k,k] in Indices (Rotation (i,j,n,0)) holds
(Rotation (i,j,n,0)) * (k,k) = 1. F_Real

proof

let k be Nat; :: thesis: ( [k,k] in Indices (Rotation (i,j,n,0)) implies (Rotation (i,j,n,0)) * (k,k) = 1. F_Real )
assume A5: [k,k] in Indices (Rotation (i,j,n,0)) ; :: thesis: (Rotation (i,j,n,0)) * (k,k) = 1. F_Real
( k = i or k = j or ( k <> i & k <> j ) ) ;
hence (Rotation (i,j,n,0)) * (k,k) = 1. F_Real by A1, A5, Def3, SIN_COS:31; :: thesis: verum

end;

hence Rotation (i,j,n,0) = 1. (F_Real,n) by A2, MATRIX_1:def 3; :: thesis: verum