let i be Nat; :: thesis: for v being Element of ()
for pf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & pf = v holds
(Line (N,i)) "*" pf = ((N * pf) . i) . 1

let v be Element of (); :: thesis: for pf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & pf = v holds
(Line (N,i)) "*" pf = ((N * pf) . i) . 1

let pf be FinSequence of F_Real; :: thesis: for N being Matrix of 3,F_Real st i in Seg 3 & pf = v holds
(Line (N,i)) "*" pf = ((N * pf) . i) . 1

let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & pf = v implies (Line (N,i)) "*" pf = ((N * pf) . i) . 1 )
assume that
A1: i in Seg 3 and
A2: pf = v ; :: thesis: (Line (N,i)) "*" pf = ((N * pf) . i) . 1
A3: N * (<*pf*> @) is Matrix of 3,1,F_Real by ;
v in TOP-REAL 3 ;
then v in REAL 3 by EUCLID:22;
then A4: 3 = len pf by ;
v in TOP-REAL 3 ;
then A5: v in REAL 3 by EUCLID:22;
A6: width <*pf*> = len pf by ANPROJ_8:75
.= 3 by ;
A7: width N = 3 by MATRIX_0:24
.= len (<*pf*> @) by ;
N * (<*pf*> @) is Matrix of 3,1,F_Real by ;
then A8: ( [1,1] in Indices (N * (<*pf*> @)) & [2,1] in Indices (N * (<*pf*> @)) & [3,1] in Indices (N * (<*pf*> @)) ) by ;
A9: not not i = 1 & ... & not i = 3 by ;
(N * pf) . i = (N * (<*pf*> @)) . i by LAPLACE:def 9
.= Line ((N * (<*pf*> @)),i) by
.= <*((N * (<*pf*> @)) * (i,1))*> by ;
then ((N * pf) . i) . 1 = (N * (<*pf*> @)) * (i,1) by FINSEQ_1:40
.= (Line (N,i)) "*" (Col ((<*pf*> @),1)) by ;
hence (Line (N,i)) "*" pf = ((N * pf) . i) . 1 by ANPROJ_8:93; :: thesis: verum