:: deftheorem Def2 defines AxialSymmetry MATRTOP3:def 2 :
for n, i being Nat st i in Seg n holds
for b₃ being invertible Matrix of n,F_Real holds
( b₃ = AxialSymmetry (i,n) iff ( b₃ * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b₃ holds
( ( k = m & k <> i implies b₃ * (k,k) = 1. F_Real ) & ( k <> m implies b₃ * (k,m) = 0. F_Real ) ) ) ) );