let I1, I2 be invertible Matrix of n,F_Real; :: thesis: ( I1 * (i,i) = cos r & I1 * (j,j) = cos r & I1 * (i,j) = sin r & I1 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices I1 holds

( ( k = m & k <> i & k <> j implies I1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I1 * (k,m) = 0. F_Real ) ) ) & I2 * (i,i) = cos r & I2 * (j,j) = cos r & I2 * (i,j) = sin r & I2 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices I2 holds

( ( k = m & k <> i & k <> j implies I2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I2 * (k,m) = 0. F_Real ) ) ) implies I1 = I2 )

assume that

A4: ( I1 * (i,i) = cos r & I1 * (j,j) = cos r & I1 * (i,j) = sin r & I1 * (j,i) = - (sin r) ) and

A5: for k, m being Nat st [k,m] in Indices I1 holds

( ( k = m & k <> i & k <> j implies I1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I1 * (k,m) = 0. F_Real ) ) and

A6: ( I2 * (i,i) = cos r & I2 * (j,j) = cos r & I2 * (i,j) = sin r & I2 * (j,i) = - (sin r) ) and

A7: for k, m being Nat st [k,m] in Indices I2 holds

( ( k = m & k <> i & k <> j implies I2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I2 * (k,m) = 0. F_Real ) ) ; :: thesis: I1 = I2

for k, m being Nat st [k,m] in Indices I1 holds

I1 * (k,m) = I2 * (k,m)

( ( k = m & k <> i & k <> j implies I1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I1 * (k,m) = 0. F_Real ) ) ) & I2 * (i,i) = cos r & I2 * (j,j) = cos r & I2 * (i,j) = sin r & I2 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices I2 holds

( ( k = m & k <> i & k <> j implies I2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I2 * (k,m) = 0. F_Real ) ) ) implies I1 = I2 )

assume that

A4: ( I1 * (i,i) = cos r & I1 * (j,j) = cos r & I1 * (i,j) = sin r & I1 * (j,i) = - (sin r) ) and

A5: for k, m being Nat st [k,m] in Indices I1 holds

( ( k = m & k <> i & k <> j implies I1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I1 * (k,m) = 0. F_Real ) ) and

A6: ( I2 * (i,i) = cos r & I2 * (j,j) = cos r & I2 * (i,j) = sin r & I2 * (j,i) = - (sin r) ) and

A7: for k, m being Nat st [k,m] in Indices I2 holds

( ( k = m & k <> i & k <> j implies I2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies I2 * (k,m) = 0. F_Real ) ) ; :: thesis: I1 = I2

for k, m being Nat st [k,m] in Indices I1 holds

I1 * (k,m) = I2 * (k,m)

proof

hence
I1 = I2
by MATRIX_0:27; :: thesis: verum
let k, m be Nat; :: thesis: ( [k,m] in Indices I1 implies I1 * (k,m) = I2 * (k,m) )

assume A8: [k,m] in Indices I1 ; :: thesis: I1 * (k,m) = I2 * (k,m)

then A9: [k,m] in Indices I2 by MATRIX_0:26;

end;assume A8: [k,m] in Indices I1 ; :: thesis: I1 * (k,m) = I2 * (k,m)

then A9: [k,m] in Indices I2 by MATRIX_0:26;

per cases
( ( k = m & ( k = i or k = j ) ) or ( k <> m & ( ( k = i & m = j ) or ( k = j & m = i ) ) ) or ( k = m & k <> i & k <> j ) or ( k <> m & ( ( 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 ) ) ) )
;

end;

suppose
( ( k = m & ( k = i or k = j ) ) or ( k <> m & ( ( k = i & m = j ) or ( k = j & m = i ) ) ) )
; :: thesis: I1 * (k,m) = I2 * (k,m)

end;

end;

suppose A10:
( k = m & k <> i & k <> j )
; :: thesis: I1 * (k,m) = I2 * (k,m)

then
I1 * (k,m) = 1. F_Real
by A5, A8;

hence I1 * (k,m) = I2 * (k,m) by A7, A9, A10; :: thesis: verum

end;hence I1 * (k,m) = I2 * (k,m) by A7, A9, A10; :: thesis: verum

suppose A11:
( k <> m & ( ( 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 ) ) )
; :: thesis: I1 * (k,m) = I2 * (k,m)

then A12:
{k,m} <> {i,j}
by ZFMISC_1:6;

then I1 * (k,m) = 0. F_Real by A5, A8, A11;

hence I1 * (k,m) = I2 * (k,m) by A7, A9, A11, A12; :: thesis: verum

end;then I1 * (k,m) = 0. F_Real by A5, A8, A11;

hence I1 * (k,m) = I2 * (k,m) by A7, A9, A11, A12; :: thesis: verum