let N be Matrix of 3,REAL; :: thesis: for uf being FinSequence of REAL
for u being Element of (TOP-REAL 3) st N is invertible & u = uf & not u is zero holds
N * uf <> 0. (TOP-REAL 3)
let uf be FinSequence of REAL ; :: thesis: for u being Element of (TOP-REAL 3) st N is invertible & u = uf & not u is zero holds
N * uf <> 0. (TOP-REAL 3)
let u be Element of (TOP-REAL 3); :: thesis: ( N is invertible & u = uf & not u is zero implies N * uf <> 0. (TOP-REAL 3) )
assume A1: ( N is invertible & u = uf & not u is zero ) ; :: thesis: N * uf <> 0. (TOP-REAL 3)
then dom uf = Seg 3 by FINSEQ_1:89;
then A2: len uf = 3 by FINSEQ_1:def 3;
assume A3: N * uf = 0. (TOP-REAL 3) ; :: thesis: contradiction
A4: ( (Inv N) * N = 1_Rmatrix 3 & (Inv N) * N = 1_Rmatrix 3 ) by A1, MATRIXR2:def 6;
( width N = 3 & len N = 3 & width (Inv N) = 3 ) by MATRIX_0:24;
then (Inv N) * (N * uf) = ((Inv N) * N) * uf by A2, MATRIXR2:59
.= uf by A4, A2, MATRIXR2:86 ;
hence contradiction by A3, A1, Th31; :: thesis: verum