let i be Nat; :: thesis: for r being Real

for u, v being Element of (TOP-REAL 3)

for p1 being FinSequence of 1 -tuples_on REAL

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

let r be Real; :: thesis: for u, v being Element of (TOP-REAL 3)

for p1 being FinSequence of 1 -tuples_on REAL

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

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

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

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

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

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

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u implies (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf) )

assume that

A1: i in Seg 3 and

A2: u = uf and

A3: pf = v and

A4: p1 = N * uf and

A5: r <> 0 and

A6: v = r * u ; :: thesis: (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

set b = 1 / r;

A7: ( p1 . 1 = <*((N * (<*uf*> @)) * (1,1))*> & p1 . 2 = <*((N * (<*uf*> @)) * (2,1))*> & p1 . 3 = <*((N * (<*uf*> @)) * (3,1))*> ) by A2, A4, FINSEQ_1:1, Lem02;

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

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

.= (1 / r) * ((Line (N,i)) "*" pf) by A1, A2, A3, A5, A6, Lem03 ;

hence (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf) ; :: thesis: verum

for u, v being Element of (TOP-REAL 3)

for p1 being FinSequence of 1 -tuples_on REAL

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

let r be Real; :: thesis: for u, v being Element of (TOP-REAL 3)

for p1 being FinSequence of 1 -tuples_on REAL

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

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

for pf, uf being FinSequence of F_Real

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

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

for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

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

(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u implies (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf) )

assume that

A1: i in Seg 3 and

A2: u = uf and

A3: pf = v and

A4: p1 = N * uf and

A5: r <> 0 and

A6: v = r * u ; :: thesis: (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)

set b = 1 / r;

A7: ( p1 . 1 = <*((N * (<*uf*> @)) * (1,1))*> & p1 . 2 = <*((N * (<*uf*> @)) * (2,1))*> & p1 . 3 = <*((N * (<*uf*> @)) * (3,1))*> ) by A2, A4, FINSEQ_1:1, Lem02;

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

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

.= (1 / r) * ((Line (N,i)) "*" pf) by A1, A2, A3, A5, A6, Lem03 ;

hence (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf) ; :: thesis: verum