let p1, p2, q1, q2 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 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 holds
|((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
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 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 holds
|((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
let t1, t2 be Real; :: thesis: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 implies |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| )
assume A1: ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q1 = (VFunc g1,g2,g3) . t1 & q2 = (VFunc g1,g2,g3) . t2 ) ; :: thesis: |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
A2: p1 = |[(f1 . t1),(f2 . t1),(f3 . t1)]| by A1, Def1;
A3: p1 . 1 = f1 . t1 by A2, FINSEQ_1:62;
A4: p1 . 2 = f2 . t1 by A2, FINSEQ_1:62;
A5: p1 . 3 = f3 . t1 by A2, FINSEQ_1:62;
A6: p2 = |[(f1 . t2),(f2 . t2),(f3 . t2)]| by A1, Def1;
A7: p2 . 1 = f1 . t2 by A6, FINSEQ_1:62;
A8: p2 . 2 = f2 . t2 by A6, FINSEQ_1:62;
A9: p2 . 3 = f3 . t2 by A6, FINSEQ_1:62;
A10: q1 = |[(g1 . t1),(g2 . t1),(g3 . t1)]| by A1, Def1;
A11: q1 . 1 = g1 . t1 by A10, FINSEQ_1:62;
A12: q1 . 2 = g2 . t1 by A10, FINSEQ_1:62;
A13: q1 . 3 = g3 . t1 by A10, FINSEQ_1:62;
A14: q2 = |[(g1 . t2),(g2 . t2),(g3 . t2)]| by A1, Def1;
A15: q2 . 1 = g1 . t2 by A14, FINSEQ_1:62;
A16: q2 . 2 = g2 . t2 by A14, FINSEQ_1:62;
A17: q2 . 3 = g3 . t2 by A14, FINSEQ_1:62;
set q = q1 + q2;
A19: q1 + q2 = |[((g1 . t1) + (g1 . t2)),((g2 . t1) + (g2 . t2)),((g3 . t1) + (g3 . t2))]| by A1, Th44;
set p = p1 + p2;
A21: p1 + p2 = |[((f1 . t1) + (f1 . t2)),((f2 . t1) + (f2 . t2)),((f3 . t1) + (f3 . t2))]| by A1, Th44;
|((p1 + p2),(q1 + q2))| = ((((p1 + p2) . 1) * ((q1 + q2) . 1)) + (((p1 + p2) . 2) * ((q1 + q2) . 2))) + (((p1 + p2) . 3) * ((q1 + q2) . 3)) by Lm8
.= ((((f1 . t1) + (f1 . t2)) * ((q1 + q2) . 1)) + (((p1 + p2) . 2) * ((q1 + q2) . 2))) + (((p1 + p2) . 3) * ((q1 + q2) . 3)) by A21, FINSEQ_1:62
.= ((((f1 . t1) + (f1 . t2)) * ((q1 + q2) . 1)) + (((f2 . t1) + (f2 . t2)) * ((q1 + q2) . 2))) + (((p1 + p2) . 3) * ((q1 + q2) . 3)) by A21, FINSEQ_1:62
.= ((((f1 . t1) + (f1 . t2)) * ((q1 + q2) . 1)) + (((f2 . t1) + (f2 . t2)) * ((q1 + q2) . 2))) + (((f3 . t1) + (f3 . t2)) * ((q1 + q2) . 3)) by A21, FINSEQ_1:62
.= ((((f1 . t1) + (f1 . t2)) * ((g1 . t1) + (g1 . t2))) + (((f2 . t1) + (f2 . t2)) * ((q1 + q2) . 2))) + (((f3 . t1) + (f3 . t2)) * ((q1 + q2) . 3)) by A19, FINSEQ_1:62
.= ((((f1 . t1) + (f1 . t2)) * ((g1 . t1) + (g1 . t2))) + (((f2 . t1) + (f2 . t2)) * ((g2 . t1) + (g2 . t2)))) + (((f3 . t1) + (f3 . t2)) * ((q1 + q2) . 3)) by A19, FINSEQ_1:62
.= ((((((f1 . t1) * (g1 . t1)) + ((f1 . t2) * (g1 . t1))) + ((f1 . t1) * (g1 . t2))) + ((f1 . t2) * (g1 . t2))) + (((((f2 . t1) * (g2 . t1)) + ((f2 . t2) * (g2 . t1))) + ((f2 . t1) * (g2 . t2))) + ((f2 . t2) * (g2 . t2)))) + (((f3 . t1) + (f3 . t2)) * ((g3 . t1) + (g3 . t2))) by A19, FINSEQ_1:62
.= ((((((f1 . t1) * (g1 . t1)) + ((f2 . t1) * (g2 . t1))) + ((f3 . t1) * (g3 . t1))) + ((((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2)))) + ((((f1 . t2) * (g1 . t1)) + ((f2 . t2) * (g2 . t1))) + ((f3 . t2) * (g3 . t1)))) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2)))
.= ((|(p1,q1)| + ((((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2)))) + ((((f1 . t2) * (g1 . t1)) + ((f2 . t2) * (g2 . t1))) + ((f3 . t2) * (g3 . t1)))) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2))) by A3, A4, A5, A11, A12, A13, Lm8
.= ((|(p1,q1)| + |(p1,q2)|) + ((((f1 . t2) * (g1 . t1)) + ((f2 . t2) * (g2 . t1))) + ((f3 . t2) * (g3 . t1)))) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2))) by A3, A4, A5, A15, A16, A17, Lm8
.= ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2))) by A7, A8, A9, A11, A12, A13, Lm8
.= ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by A7, A8, A9, A15, A16, A17, Lm8 ;
hence |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| ; :: thesis: verum