let r1, r2 be Element of REAL ; :: thesis: for p1, p2, q being Element of REAL 3
for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2 being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 holds
|(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|)
let p1, p2, q be Element of REAL 3; :: thesis: for f1, f2, f3, g1, g2, g3 being PartFunc of ,
for t1, t2 being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 holds
|(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|)
let f1, f2, f3, g1, g2, g3 be PartFunc of ,; :: thesis: for t1, t2 being Real st p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 holds
|(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|)
let t1, t2 be Real; :: thesis: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 implies |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|) )
assume A1: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 ) ; :: thesis: |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|)
A10: q = |[(g1 . t2),(g2 . t2),(g3 . t2)]| by A1, Def1;
A11: q . 1 = g1 . t2 by A10, FINSEQ_1:62;
A12: q . 2 = g2 . t2 by A10, FINSEQ_1:62;
A13: q . 3 = g3 . t2 by A10, FINSEQ_1:62;
A14: r1 * |(p1,q)| = r1 * ((((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2))) by A1, Th51;
A15: r2 * |(p2,q)| = r2 * ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2))) by A1, Th51;
A16: (r1 * p1) + (r2 * p2) = |[(r1 * (f1 . t1)),(r1 * (f2 . t1)),(r1 * (f3 . t1))]| + (r2 * p2) by A1, Th38
.= |[(r1 * (f1 . t1)),(r1 * (f2 . t1)),(r1 * (f3 . t1))]| + |[(r2 * (f1 . t2)),(r2 * (f2 . t2)),(r2 * (f3 . t2))]| by A1, Th38
.= |[((r1 * (f1 . t1)) + (r2 * (f1 . t2))),((r1 * (f2 . t1)) + (r2 * (f2 . t2))),((r1 * (f3 . t1)) + (r2 * (f3 . t2)))]| by LmA31 ;
set p = (r1 * p1) + (r2 * p2);
|(((r1 * p1) + (r2 * p2)),q)| = (((((r1 * p1) + (r2 * p2)) . 1) * (q . 1)) + ((((r1 * p1) + (r2 * p2)) . 2) * (q . 2))) + ((((r1 * p1) + (r2 * p2)) . 3) * (q . 3)) by Lm8
.= ((((r1 * (f1 . t1)) + (r2 * (f1 . t2))) * (q . 1)) + ((((r1 * p1) + (r2 * p2)) . 2) * (q . 2))) + ((((r1 * p1) + (r2 * p2)) . 3) * (q . 3)) by A16, FINSEQ_1:62
.= ((((r1 * (f1 . t1)) + (r2 * (f1 . t2))) * (q . 1)) + (((r1 * (f2 . t1)) + (r2 * (f2 . t2))) * (q . 2))) + ((((r1 * p1) + (r2 * p2)) . 3) * (q . 3)) by A16, FINSEQ_1:62
.= ((((r1 * (f1 . t1)) * (g1 . t2)) + (((r1 * (f2 . t1)) + (r2 * (f2 . t2))) * (g2 . t2))) + ((r2 * (f1 . t2)) * (g1 . t2))) + (((r1 * (f3 . t1)) + (r2 * (f3 . t2))) * (g3 . t2)) by A11, A12, A13, A16, FINSEQ_1:62
.= (r1 * |(p1,q)|) + (r2 * |(p2,q)|) by A14, A15 ;
hence |(((r1 * p1) + (r2 * p2)),q)| = (r1 * |(p1,q)|) + (r2 * |(p2,q)|) ; :: thesis: verum