let i be Nat; :: thesis: for v being Element of (TOP-REAL 3)

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 (TOP-REAL 3); :: 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 A2, FINSEQ_3:153, ANPROJ_8:91;

v in TOP-REAL 3 ;

then v in REAL 3 by EUCLID:22;

then A4: 3 = len pf by A2, EUCLID_8:50;

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 A2, A5, EUCLID_8:50 ;

A7: width N = 3 by MATRIX_0:24

.= len (<*pf*> @) by MATRIX_0:def 6, A6 ;

N * (<*pf*> @) is Matrix of 3,1,F_Real by A2, FINSEQ_3:153, ANPROJ_8:91;

then A8: ( [1,1] in Indices (N * (<*pf*> @)) & [2,1] in Indices (N * (<*pf*> @)) & [3,1] in Indices (N * (<*pf*> @)) ) by MATRIX_0:23, ANPROJ_8:2;

A9: not not i = 1 & ... & not i = 3 by A1, FINSEQ_1:91;

(N * pf) . i = (N * (<*pf*> @)) . i by LAPLACE:def 9

.= Line ((N * (<*pf*> @)),i) by A1, A3, MATRIX_0:52

.= <*((N * (<*pf*> @)) * (i,1))*> by A9, A4, ANPROJ_8:92 ;

then ((N * pf) . i) . 1 = (N * (<*pf*> @)) * (i,1) by FINSEQ_1:40

.= (Line (N,i)) "*" (Col ((<*pf*> @),1)) by A9, A7, A8, MATRIX_3:def 4 ;

hence (Line (N,i)) "*" pf = ((N * pf) . i) . 1 by ANPROJ_8:93; :: thesis: verum

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 (TOP-REAL 3); :: 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 A2, FINSEQ_3:153, ANPROJ_8:91;

v in TOP-REAL 3 ;

then v in REAL 3 by EUCLID:22;

then A4: 3 = len pf by A2, EUCLID_8:50;

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 A2, A5, EUCLID_8:50 ;

A7: width N = 3 by MATRIX_0:24

.= len (<*pf*> @) by MATRIX_0:def 6, A6 ;

N * (<*pf*> @) is Matrix of 3,1,F_Real by A2, FINSEQ_3:153, ANPROJ_8:91;

then A8: ( [1,1] in Indices (N * (<*pf*> @)) & [2,1] in Indices (N * (<*pf*> @)) & [3,1] in Indices (N * (<*pf*> @)) ) by MATRIX_0:23, ANPROJ_8:2;

A9: not not i = 1 & ... & not i = 3 by A1, FINSEQ_1:91;

(N * pf) . i = (N * (<*pf*> @)) . i by LAPLACE:def 9

.= Line ((N * (<*pf*> @)),i) by A1, A3, MATRIX_0:52

.= <*((N * (<*pf*> @)) * (i,1))*> by A9, A4, ANPROJ_8:92 ;

then ((N * pf) . i) . 1 = (N * (<*pf*> @)) * (i,1) by FINSEQ_1:40

.= (Line (N,i)) "*" (Col ((<*pf*> @),1)) by A9, A7, A8, MATRIX_3:def 4 ;

hence (Line (N,i)) "*" pf = ((N * pf) . i) . 1 by ANPROJ_8:93; :: thesis: verum