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
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
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 p + q = |[((f1 . t1) + (g1 . t2)),((f2 . t1) + (g2 . t2)),((f3 . t1) + (g3 . t2))]| )
assume ( p = (VFunc f1,f2,f3) . t1 & q = (VFunc g1,g2,g3) . t2 ) ; :: thesis: p + q = |[((f1 . t1) + (g1 . t2)),((f2 . t1) + (g2 . t2)),((f3 . t1) + (g3 . t2))]|
then A1: ( p = |[(f1 . t1),(f2 . t1),(f3 . t1)]| & q = |[(g1 . t2),(g2 . t2),(g3 . t2)]| ) by Def1;
A2: ( p . 1 = f1 . t1 & p . 2 = f2 . t1 & p . 3 = f3 . t1 ) by A1, FINSEQ_1:62;
( q . 1 = g1 . t2 & q . 2 = g2 . t2 & q . 3 = g3 . t2 ) by A1, FINSEQ_1:62;
hence p + q = |[((f1 . t1) + (g1 . t2)),((f2 . t1) + (g2 . t2)),((f3 . t1) + (g3 . t2))]| by A2, Lm4; :: thesis: verum