let p, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
mlt p,q = <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (g2 . t2)),((f3 . t1) * (g3 . t2))*>
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2 being Real st p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 holds
mlt p,q = <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (g2 . t2)),((f3 . t1) * (g3 . t2))*>
let t1, t2 be Real; :: thesis: ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 implies mlt p,q = <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (g2 . t2)),((f3 . t1) * (g3 . t2))*> )
assume A1: ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 ) ; :: thesis: mlt p,q = <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (g2 . t2)),((f3 . t1) * (g3 . t2))*>
A2: ( len p = 3 & len q = 3 ) by A1, Th35;
mlt p,q = <*((p . 1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*> by A2, EUCLID_5:28
.= <*((f1 . t1) * (q . 1)),((p . 2) * (q . 2)),((p . 3) * (q . 3))*> by A1, Th34
.= <*((f1 . t1) * (q . 1)),((f2 . t1) * (q . 2)),((p . 3) * (q . 3))*> by A1, Th34
.= <*((f1 . t1) * (q . 1)),((f2 . t1) * (q . 2)),((f3 . t1) * (q . 3))*> by A1, Th34
.= <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (q . 2)),((f3 . t1) * (q . 3))*> by A1, Th34
.= <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (g2 . t2)),((f3 . t1) * (q . 3))*> by A1, Th34
.= <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (g2 . t2)),((f3 . t1) * (g3 . t2))*> by A1, Th34 ;
hence mlt p,q = <*((f1 . t1) * (g1 . t2)),((f2 . t1) * (g2 . t2)),((f3 . t1) * (g3 . t2))*> ; :: thesis: verum