let r be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds
ex A being Matrix of n,F_Real st
( Det A = 1. F_Real & A * (i,i) = cos r & A * (j,j) = cos r & A * (i,j) = sin r & A * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices A holds
( ( k = m & k <> i & k <> j implies A * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies A * (k,m) = 0. F_Real ) ) ) )

let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies ex A being Matrix of n,F_Real st
( Det A = 1. F_Real & A * (i,i) = cos r & A * (j,j) = cos r & A * (i,j) = sin r & A * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices A holds
( ( k = m & k <> i & k <> j implies A * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies A * (k,m) = 0. F_Real ) ) ) ) )

A1: now :: thesis: for k being Nat st k >= 1 & k <> 1 & k <> 2 holds
k > 2
let k be Nat; :: thesis: ( k >= 1 & k <> 1 & k <> 2 implies k > 2 )
assume that
A2: ( k >= 1 & k <> 1 ) and
A3: k <> 2 ; :: thesis: k > 2
k > 1 by ;
then k >= 1 + 1 by NAT_1:13;
hence k > 2 by ; :: thesis: verum
end;
reconsider s = sin r, c = cos r as Element of F_Real by XREAL_0:def 1;
set S = Seg n;
assume that
A4: 1 <= i and
A5: i < j and
A6: j <= n ; :: thesis: ex A being Matrix of n,F_Real st
( Det A = 1. F_Real & A * (i,i) = cos r & A * (j,j) = cos r & A * (i,j) = sin r & A * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices A holds
( ( k = m & k <> i & k <> j implies A * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies A * (k,m) = 0. F_Real ) ) ) )

A7: 1 < j by ;
then A8: 1 + 1 <= j by NAT_1:13;
then reconsider n2 = n - 2 as Nat by ;
consider P being Permutation of (Seg n) such that
A9: P . 1 = i and
A10: P . 2 = j and
for k being Nat st k in Seg n & k > 2 holds
( ( k <= i + 1 implies P . k = k - 2 ) & ( i + 1 < k & k <= j implies P . k = k - 1 ) & ( k > j implies P . k = k ) ) by A4, A5, A6, Lm2;
reconsider p = P as one-to-one Function ;
dom P = Seg n by FUNCT_2:52;
then A11: rng (p ") = Seg n by FUNCT_1:33;
rng P = Seg n by FUNCT_2:def 3;
then dom (p ") = Seg n by FUNCT_1:33;
then reconsider P1 = p " as one-to-one Function of (Seg n),(Seg n) by ;
P1 is onto by ;
then reconsider P1 = P1 as Permutation of (Seg n) ;
A12: dom P = Seg n by FUNCT_2:52;
1 <= n by ;
then A13: 1 in Seg n ;
then A14: P1 . (P . 1) = 1 by ;
set A = (c,s) ][ ((- s),c);
set ONE = 1. (F_Real,n2);
set ao = <*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>;
set B = block_diagonal (<*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>,());
A15: len ((c,s) ][ ((- s),c)) = 2 by MATRIX_0:25;
then Len <*((c,s) ][ ((- s),c))*> = <*2*> by MATRIXJ1:15;
then A16: Sum (Len <*((c,s) ][ ((- s),c))*>) = 2 by RVSUM_1:73;
len (1. (F_Real,n2)) = n2 by MATRIX_0:25;
then A17: Sum (Len <*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>) = 2 + n2 by ;
then reconsider B = block_diagonal (<*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>,()) as Matrix of n,F_Real ;
A18: Indices B = [:(Seg n),(Seg n):] by MATRIX_0:24;
2 <= n by ;
then A19: 2 in Seg n ;
then A20: P1 . (P . 2) = 2 by ;
set pBp = (((B * P1) @) * P1) @ ;
A21: dom P1 = Seg n by FUNCT_2:52;
i < n by ;
then A22: i in Seg n by A4;
then [i,i] in Indices B by ;
then A23: ((((B * P1) @) * P1) @) * (i,i) = B * (1,1) by A9, A14, Th1;
take (((B * P1) @) * P1) @ ; :: thesis: ( Det ((((B * P1) @) * P1) @) = 1. F_Real & ((((B * P1) @) * P1) @) * (i,i) = cos r & ((((B * P1) @) * P1) @) * (j,j) = cos r & ((((B * P1) @) * P1) @) * (i,j) = sin r & ((((B * P1) @) * P1) @) * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices ((((B * P1) @) * P1) @) holds
( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) ) ) )

A24: Indices ((((B * P1) @) * P1) @) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A25: Det B = 1. F_Real by ;
A26: block_diagonal (<*((c,s) ][ ((- s),c))*>,()) = (c,s) ][ ((- s),c) by MATRIXJ1:34;
width ((c,s) ][ ((- s),c)) = 2 by MATRIX_0:24;
then Width <*((c,s) ][ ((- s),c))*> = <*2*> by MATRIXJ1:19;
then A27: Sum (Width <*((c,s) ][ ((- s),c))*>) = 2 by RVSUM_1:73;
1 < j by ;
then A28: j in Seg n by A6;
then [j,j] in Indices B by ;
then A29: ((((B * P1) @) * P1) @) * (j,j) = B * (2,2) by ;
A30: block_diagonal (<*(1. (F_Real,n2))*>,()) = 1. (F_Real,n2) by MATRIXJ1:34;
[1,1] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A31: B * (1,1) = ((c,s) ][ ((- s),c)) * (1,1) by ;
[2,1] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A32: B * (2,1) = ((c,s) ][ ((- s),c)) * (2,1) by ;
[1,2] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A33: B * (1,2) = ((c,s) ][ ((- s),c)) * (1,2) by ;
[2,2] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A34: B * (2,2) = ((c,s) ][ ((- s),c)) * (2,2) by ;
A35: <*((c,s) ][ ((- s),c))*> ^ <*(1. (F_Real,n2))*> = <*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*> ;
[i,j] in Indices B by ;
then A36: ((((B * P1) @) * P1) @) * (i,j) = B * (1,2) by A9, A10, A14, A20, Th1;
[j,i] in Indices B by ;
then ((((B * P1) @) * P1) @) * (j,i) = B * (2,1) by A9, A10, A14, A20, Th1;
hence ( Det ((((B * P1) @) * P1) @) = 1. F_Real & ((((B * P1) @) * P1) @) * (i,i) = cos r & ((((B * P1) @) * P1) @) * (j,j) = cos r & ((((B * P1) @) * P1) @) * (i,j) = sin r & ((((B * P1) @) * P1) @) * (j,i) = - (sin r) ) by ; :: thesis: for k, m being Nat st [k,m] in Indices ((((B * P1) @) * P1) @) holds
( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) )

let k, m be Nat; :: thesis: ( [k,m] in Indices ((((B * P1) @) * P1) @) implies ( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) ) )
assume A37: [k,m] in Indices ((((B * P1) @) * P1) @) ; :: thesis: ( ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) )
A38: k in Seg n by ;
set Pk = P1 . k;
set Pm = P1 . m;
A39: rng P1 = Seg n by FUNCT_2:def 3;
then A40: P1 . k in Seg n by ;
then A41: P1 . k >= 1 by FINSEQ_1:1;
A42: m in Seg n by ;
then A43: P1 . m in Seg n by ;
then A44: [(P1 . k),(P1 . m)] in [:(Seg n),(Seg n):] by ;
A45: ((((B * P1) @) * P1) @) * (k,m) = B * ((P1 . k),(P1 . m)) by A18, A24, A37, Th1;
thus ( k = m & k <> i & k <> j implies ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real ) :: thesis: ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real )
proof
assume that
A46: k = m and
A47: ( k <> i & k <> j ) ; :: thesis: ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real
( P1 . k <> 1 & P1 . k <> 2 ) by ;
then A48: P1 . k > 2 by ;
then reconsider Pk2 = (P1 . k) - 2 as Nat by NAT_1:21;
( P1 . k = Pk2 + 2 & Pk2 > 2 - 2 ) by ;
then A49: [Pk2,Pk2] in Indices (1. (F_Real,n2)) by ;
then (1. (F_Real,n2)) * (Pk2,Pk2) = B * ((Pk2 + 2),(Pk2 + 2)) by ;
hence ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real by ; :: thesis: verum
end;
A50: P1 . m >= 1 by ;
thus ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) :: thesis: verum
proof
assume that
A51: k <> m and
A52: {k,m} <> {i,j} ; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real
A53: P1 . k <> P1 . m by ;
per cases ( ( k <> i & k <> j & m <> i & m <> j ) or ( k = i & m <> j ) or ( k = j & m <> i ) or ( m = i & k <> j ) or ( m = j & k <> i ) ) by A52;
suppose A54: ( k <> i & k <> j & m <> i & m <> j ) ; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real
then ( P1 . k <> 1 & P1 . k <> 2 ) by ;
then A55: P1 . k > 2 by ;
( P1 . m <> 1 & P1 . m <> 2 ) by ;
then A56: P1 . m > 2 by ;
then reconsider Pk2 = (P1 . k) - 2, Pm2 = (P1 . m) - 2 as Nat by ;
A57: Pk2 > 2 - 2 by ;
A58: ( P1 . k = Pk2 + 2 & P1 . m = Pm2 + 2 ) ;
Pm2 > 2 - 2 by ;
then A59: [Pk2,Pm2] in Indices (1. (F_Real,n2)) by ;
then (1. (F_Real,n2)) * (Pk2,Pm2) = B * ((Pk2 + 2),(Pm2 + 2)) by ;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by ; :: thesis: verum
end;
suppose A60: ( k = i & m <> j ) ; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real
then P1 . m <> 2 by ;
then A61: P1 . m > 2 by A1, A9, A14, A50, A53, A60;
P1 . k = 1 by ;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by ; :: thesis: verum
end;
suppose A62: ( k = j & m <> i ) ; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real
then P1 . m <> 1 by ;
then A63: P1 . m > 2 by A1, A10, A20, A50, A53, A62;
P1 . k = 2 by ;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by ; :: thesis: verum
end;
suppose A64: ( m = i & k <> j ) ; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real
then P1 . k <> 2 by ;
then A65: P1 . k > 2 by A1, A9, A14, A41, A53, A64;
P1 . m = 1 by ;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by ; :: thesis: verum
end;
suppose A66: ( m = j & k <> i ) ; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real
then P1 . k <> 1 by ;
then A67: P1 . k > 2 by A1, A10, A20, A41, A53, A66;
P1 . m = 2 by ;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by ; :: thesis: verum
end;
end;
end;