let r be Real; :: thesis:
let i, j, n be Nat; :: thesis:

A1: now :: thesis:

let k be Nat; :: thesis:
assume that
A2: ( k >= 1 & k <> 1 ) and
A3: k <> 2 ; :: thesis:
k > 1 by A2, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
hence k > 2 by A3, XXREAL_0:1; :: thesis:

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:
A7: 1 < j by A4, A5, XXREAL_0:2;
then A8: 1 + 1 <= j by NAT_1:13;
then reconsider n2 = n - 2 as Nat by A6, NAT_1:21, XXREAL_0:2;
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 A11, FUNCT_2:1;
P1 is onto by A11, FUNCT_2:def 3;
then reconsider P1 = P1 as Permutation of (Seg n) ;
A12: dom P = Seg n by FUNCT_2:52;
1 <= n by A6, A7, XXREAL_0:2;
then A13: 1 in Seg n ;
then A14: P1 . (P . 1) = 1 by A12, FUNCT_1:34;
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))*>,(0. F_Real));
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 A15, MATRIXJ1:16;
then reconsider B = block_diagonal (<*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*>,(0. F_Real)) as Matrix of n,F_Real ;
A18: Indices B = [:(Seg n),(Seg n):] by MATRIX_0:24;
2 <= n by A6, A8, XXREAL_0:2;
then A19: 2 in Seg n ;
then A20: P1 . (P . 2) = 2 by A12, FUNCT_1:34;
set pBp = (((B * P1) @) * P1) @ ;
A21: dom P1 = Seg n by FUNCT_2:52;
i < n by A5, A6, XXREAL_0:2;
then A22: i in Seg n by A4;
then [i,i] in Indices B by A18, ZFMISC_1:87;
then A23: ((((B * P1) @) * P1) @) * (i,i) = B * (1,1) by A9, A14, Th1;
take (((B * P1) @) * P1) @ ; :: thesis:
A24: Indices ((((B * P1) @) * P1) @) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A25: Det B = 1. F_Real by A17, Th12;
A26: block_diagonal (<*((c,s) ][ ((- s),c))*>,(0. F_Real)) = (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 A4, A5, XXREAL_0:2;
then A28: j in Seg n by A6;
then [j,j] in Indices B by A18, ZFMISC_1:87;
then A29: ((((B * P1) @) * P1) @) * (j,j) = B * (2,2) by A10, A20, Th1;
A30: block_diagonal (<*(1. (F_Real,n2))*>,(0. F_Real)) = 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 A26, A30, MATRIXJ1:26;
[2,1] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A32: B * (2,1) = ((c,s) ][ ((- s),c)) * (2,1) by A26, A30, MATRIXJ1:26;
[1,2] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A33: B * (1,2) = ((c,s) ][ ((- s),c)) * (1,2) by A26, A30, MATRIXJ1:26;
[2,2] in Indices ((c,s) ][ ((- s),c)) by MATRIX_0:48;
then A34: B * (2,2) = ((c,s) ][ ((- s),c)) * (2,2) by A26, A30, MATRIXJ1:26;
A35: <*((c,s) ][ ((- s),c))*> ^ <*(1. (F_Real,n2))*> = <*((c,s) ][ ((- s),c)),(1. (F_Real,n2))*> ;
[i,j] in Indices B by A18, A22, A28, ZFMISC_1:87;
then A36: ((((B * P1) @) * P1) @) * (i,j) = B * (1,2) by A9, A10, A14, A20, Th1;
[j,i] in Indices B by A18, A22, A28, ZFMISC_1:87;
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 A23, A25, A29, A34, A33, A32, A31, A36, Th1, MATRIX_0:50; :: thesis:
let k, m be Nat; :: thesis:
assume A37: [k,m] in Indices ((((B * P1) @) * P1) @) ; :: thesis:
A38: k in Seg n by A24, A37, ZFMISC_1:87;
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 A21, A38, FUNCT_1:def 3;
then A41: P1 . k >= 1 by FINSEQ_1:1;
A42: m in Seg n by A24, A37, ZFMISC_1:87;
then A43: P1 . m in Seg n by A21, A39, FUNCT_1:def 3;
then A44: [(P1 . k),(P1 . m)] in [:(Seg n),(Seg n):] by A40, ZFMISC_1:87;
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:

proof

assume that
A46: k = m and
A47: ( k <> i & k <> j ) ; :: thesis:
( P1 . k <> 1 & P1 . k <> 2 ) by A9, A10, A14, A20, A21, A22, A28, A38, A47, FUNCT_1:def 4;
then A48: P1 . k > 2 by A1, A41;
then reconsider Pk2 = (P1 . k) - 2 as Nat by NAT_1:21;
( P1 . k = Pk2 + 2 & Pk2 > 2 - 2 ) by A48, XREAL_1:8;
then A49: [Pk2,Pk2] in Indices (1. (F_Real,n2)) by A16, A18, A27, A30, A44, A46, MATRIXJ1:27;
then (1. (F_Real,n2)) * (Pk2,Pk2) = B * ((Pk2 + 2),(Pk2 + 2)) by A16, A27, A30, MATRIXJ1:28;
hence ((((B * P1) @) * P1) @) * (k,k) = 1. F_Real by A45, A46, A49, MATRIX_1:def 3; :: thesis:

end;

A50: P1 . m >= 1 by A43, FINSEQ_1:1;
thus ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) :: thesis:

proof

assume that
A51: k <> m and
A52: {k,m} <> {i,j} ; :: thesis:
A53: P1 . k <> P1 . m by A21, A38, A42, A51, FUNCT_1:def 4;

per cases by A52;

suppose A54: ( k <> i & k <> j & m <> i & m <> j ) ; :: thesis:

then ( P1 . k <> 1 & P1 . k <> 2 ) by A9, A10, A14, A20, A21, A22, A28, A38, FUNCT_1:def 4;
then A55: P1 . k > 2 by A1, A41;
( P1 . m <> 1 & P1 . m <> 2 ) by A9, A10, A14, A20, A21, A22, A28, A42, A54, FUNCT_1:def 4;
then A56: P1 . m > 2 by A1, A50;
then reconsider Pk2 = (P1 . k) - 2, Pm2 = (P1 . m) - 2 as Nat by A55, NAT_1:21;
A57: Pk2 > 2 - 2 by A55, XREAL_1:8;
A58: ( P1 . k = Pk2 + 2 & P1 . m = Pm2 + 2 ) ;
Pm2 > 2 - 2 by A56, XREAL_1:8;
then A59: [Pk2,Pm2] in Indices (1. (F_Real,n2)) by A16, A18, A27, A30, A44, A58, A57, MATRIXJ1:27;
then (1. (F_Real,n2)) * (Pk2,Pm2) = B * ((Pk2 + 2),(Pm2 + 2)) by A16, A27, A30, MATRIXJ1:28;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by A45, A53, A59, MATRIX_1:def 3; :: thesis:

end;

suppose A60: ( k = i & m <> j ) ; :: thesis:

then P1 . m <> 2 by A10, A20, A21, A28, A42, FUNCT_1:def 4;
then A61: P1 . m > 2 by A1, A9, A14, A50, A53, A60;
P1 . k = 1 by A9, A12, A13, A60, FUNCT_1:34;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by A16, A18, A27, A35, A44, A45, A61, MATRIXJ1:29; :: thesis:

end;

suppose A62: ( k = j & m <> i ) ; :: thesis:

then P1 . m <> 1 by A9, A14, A21, A22, A42, FUNCT_1:def 4;
then A63: P1 . m > 2 by A1, A10, A20, A50, A53, A62;
P1 . k = 2 by A10, A12, A19, A62, FUNCT_1:34;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by A16, A18, A27, A35, A44, A45, A63, MATRIXJ1:29; :: thesis:

end;

suppose A64: ( m = i & k <> j ) ; :: thesis:

then P1 . k <> 2 by A10, A20, A21, A28, A38, FUNCT_1:def 4;
then A65: P1 . k > 2 by A1, A9, A14, A41, A53, A64;
P1 . m = 1 by A9, A12, A13, A64, FUNCT_1:34;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by A16, A18, A27, A35, A44, A45, A65, MATRIXJ1:29; :: thesis:

end;

suppose A66: ( m = j & k <> i ) ; :: thesis:

then P1 . k <> 1 by A9, A14, A21, A22, A38, FUNCT_1:def 4;
then A67: P1 . k > 2 by A1, A10, A20, A41, A53, A66;
P1 . m = 2 by A10, A12, A19, A66, FUNCT_1:34;
hence ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real by A16, A18, A27, A35, A44, A45, A67, MATRIXJ1:29; :: thesis:

end;