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

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 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: ( 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 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: 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 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: ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real )

thus ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real ) :: thesis: verum

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

reconsider s = sin r, c = cos r as Element of F_Real by XREAL_0:def 1;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 A2, XXREAL_0:1;

then k >= 1 + 1 by NAT_1:13;

hence k > 2 by A3, XXREAL_0:1; :: thesis: verum

end;assume that

A2: ( k >= 1 & k <> 1 ) and

A3: k <> 2 ; :: thesis: k > 2

k > 1 by A2, XXREAL_0:1;

then k >= 1 + 1 by NAT_1:13;

hence k > 2 by A3, XXREAL_0:1; :: thesis: verum

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 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: ( 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 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: 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 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: ( k <> m & {k,m} <> {i,j} implies ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real )

proof

A50:
P1 . m >= 1
by A43, FINSEQ_1:1;
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 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: verum

end;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 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: verum

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 A21, A38, A42, A51, FUNCT_1:def 4;

end;A51: k <> m and

A52: {k,m} <> {i,j} ; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real

A53: P1 . k <> P1 . m by A21, A38, A42, A51, FUNCT_1:def 4;

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;

end;

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 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: verum

end;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: verum

suppose A60:
( k = i & m <> j )
; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real

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: verum

end;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: verum

suppose A62:
( k = j & m <> i )
; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real

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: verum

end;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: verum

suppose A64:
( m = i & k <> j )
; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real

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: verum

end;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: verum

suppose A66:
( m = j & k <> i )
; :: thesis: ((((B * P1) @) * P1) @) * (k,m) = 0. F_Real

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: verum

end;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: verum