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