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

for p1 being FinSequence of 1 -tuples_on REAL

for uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let u be Element of (TOP-REAL 3); :: thesis: for p1 being FinSequence of 1 -tuples_on REAL

for uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let p1 be FinSequence of 1 -tuples_on REAL; :: thesis: for uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let uf be FinSequence of F_Real; :: thesis: for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & u = uf & p1 = N * uf implies p1 . i = <*((N * (<*uf*> @)) * (i,1))*> )

assume that

A1: i in Seg 3 and

A2: u = uf and

A3: p1 = N * uf ; :: thesis: p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

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

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A5: 3 = len uf by A2, EUCLID_8:50;

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

p1 = N * (<*uf*> @) by A3, LAPLACE:def 9;

then p1 . i = Line ((N * (<*uf*> @)),i) by A1, A4, MATRIX_0:52

.= <*((N * (<*uf*> @)) * (i,1))*> by A6, A5, ANPROJ_8:92 ;

hence p1 . i = <*((N * (<*uf*> @)) * (i,1))*> ; :: thesis: verum

for p1 being FinSequence of 1 -tuples_on REAL

for uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let u be Element of (TOP-REAL 3); :: thesis: for p1 being FinSequence of 1 -tuples_on REAL

for uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let p1 be FinSequence of 1 -tuples_on REAL; :: thesis: for uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let uf be FinSequence of F_Real; :: thesis: for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & p1 = N * uf holds

p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & u = uf & p1 = N * uf implies p1 . i = <*((N * (<*uf*> @)) * (i,1))*> )

assume that

A1: i in Seg 3 and

A2: u = uf and

A3: p1 = N * uf ; :: thesis: p1 . i = <*((N * (<*uf*> @)) * (i,1))*>

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

u in TOP-REAL 3 ;

then u in REAL 3 by EUCLID:22;

then A5: 3 = len uf by A2, EUCLID_8:50;

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

p1 = N * (<*uf*> @) by A3, LAPLACE:def 9;

then p1 . i = Line ((N * (<*uf*> @)),i) by A1, A4, MATRIX_0:52

.= <*((N * (<*uf*> @)) * (i,1))*> by A6, A5, ANPROJ_8:92 ;

hence p1 . i = <*((N * (<*uf*> @)) * (i,1))*> ; :: thesis: verum