let i, n be Nat; :: thesis: ( i in Seg n implies Det (AxialSymmetry (i,n)) = - (1. F_Real) )
assume A1: i in Seg n ; :: thesis: Det (AxialSymmetry (i,n)) = - (1. F_Real)
then consider M being Matrix of n,F_Real such that
A2: Det M = - (1. F_Real) and
A3: ( M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds
( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) ) by Lm1;
Det M <> 0. F_Real by A2;
then M is invertible by LAPLACE:34;
hence Det (AxialSymmetry (i,n)) = - (1. F_Real) by A1, A2, A3, Def2; :: thesis: verum