consider A being Matrix of n,F_Real such that
A2: Det A = 1. F_Real and
A3: ( 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 ) ) ) ) by A1, Lm3;
Det A <> 0. F_Real by A2;
then A is invertible by LAPLACE:34;
hence ex b₁ being invertible Matrix of n,F_Real st
( b₁ * (i,i) = cos r & b₁ * (j,j) = cos r & b₁ * (i,j) = sin r & b₁ * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b₁ holds
( ( k = m & k <> i & k <> j implies b₁ * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b₁ * (k,m) = 0. F_Real ) ) ) ) by A3; :: thesis: verum