let i be Nat; 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); 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; 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; 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; ( 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
; 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))*>
; verum