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
A3: ( I1 * (i,i) = cos r & I1 * (j,j) = cos r & I1 * (i,j) = sin r & I1 * (j,i) = - (sin r) ) and
A4: 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
A5: ( I2 * (i,i) = cos r & I2 * (j,j) = cos r & I2 * (i,j) = sin r & I2 * (j,i) = - (sin r) ) and
A6: 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

let k, m be Nat; :: thesis: ( [k,m] in Indices I1 implies I1 * (k,m) = I2 * (k,m) )
assume A7: [k,m] in Indices I1 ; :: thesis: I1 * (k,m) = I2 * (k,m)
then A8: [k,m] in Indices I2 by MATRIX_1: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 ) ) ) ) ;

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)

hence I1 * (k,m) = I2 * (k,m) by A3, A5; :: thesis: verum

end;

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

then I1 * (k,m) = 1. F_Real by A4, A7;
hence I1 * (k,m) = I2 * (k,m) by A6, A8, A9; :: thesis: verum

end;

suppose A10: ( 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 A11: {k,m} <> {i,j} by ZFMISC_1:6;
then I1 * (k,m) = 0. F_Real by A4, A7, A10;
hence I1 * (k,m) = I2 * (k,m) by A6, A8, A10, A11; :: thesis: verum

end;

end;

end;

hence I1 = I2 by MATRIX_1:27; :: thesis: verum