let p1, p2, q be 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
|((p1 + p2),q)| = |(p1,q)| + |(p2,q)|
let f1, f2, f3, g1, g2, g3 be 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
|((p1 + p2),q)| = |(p1,q)| + |(p2,q)|
let t1, t2 be Real; ( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 implies |((p1 + p2),q)| = |(p1,q)| + |(p2,q)| )
assume B0:
( p1 = (VFunc f1,f2,f3) . t1 & p2 = (VFunc f1,f2,f3) . t2 & q = (VFunc g1,g2,g3) . t2 )
; |((p1 + p2),q)| = |(p1,q)| + |(p2,q)|
A0:
p1 = |[(f1 . t1),(f2 . t1),(f3 . t1)]|
by B0, Def1;
B1:
p1 . 1 = f1 . t1
by A0, FINSEQ_1:62;
B2:
p1 . 2 = f2 . t1
by A0, FINSEQ_1:62;
B3:
p1 . 3 = f3 . t1
by A0, FINSEQ_1:62;
A2:
p2 = |[(f1 . t2),(f2 . t2),(f3 . t2)]|
by B0, Def1;
A3:
p2 . 1 = f1 . t2
by A2, FINSEQ_1:62;
A4:
p2 . 2 = f2 . t2
by A2, FINSEQ_1:62;
A5:
p2 . 3 = f3 . t2
by A2, FINSEQ_1:62;
C0:
q = |[(g1 . t2),(g2 . t2),(g3 . t2)]|
by B0, Def1;
C1:
q . 1 = g1 . t2
by C0, FINSEQ_1:62;
C2:
q . 2 = g2 . t2
by C0, FINSEQ_1:62;
C3:
q . 3 = g3 . t2
by C0, FINSEQ_1:62;
D3:
p1 + p2 = |[((p1 . 1) + (p2 . 1)),((p1 . 2) + (p2 . 2)),((p1 . 3) + (p2 . 3))]|
by Lm4;
set p = p1 + p2;
D5:
(p1 + p2) . 2 = (p1 . 2) + (p2 . 2)
by D3, FINSEQ_1:62;
D6:
(p1 + p2) . 3 = (p1 . 3) + (p2 . 3)
by D3, FINSEQ_1:62;
D7:
|((p1 + p2),q)| = ((((p1 + p2) . 1) * (q . 1)) + (((p1 + p2) . 2) * (q . 2))) + (((p1 + p2) . 3) * (q . 3))
by Lm8;
|((p1 + p2),q)| =
((((f1 . t1) + (f1 . t2)) * (g1 . t2)) + (((f2 . t1) + (f2 . t2)) * (g2 . t2))) + (((f3 . t1) + (f3 . t2)) * (g3 . t2))
by C1, C2, C3, A3, A4, A5, B1, B2, B3, D3, D5, D6, D7, FINSEQ_1:62
.=
((((f1 . t1) * (g1 . t2)) + ((f2 . t1) * (g2 . t2))) + ((f3 . t1) * (g3 . t2))) + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2)))
.=
|(p1,q)| + ((((f1 . t2) * (g1 . t2)) + ((f2 . t2) * (g2 . t2))) + ((f3 . t2) * (g3 . t2)))
by B1, B2, B3, C1, C2, C3, Lm8
.=
|(p1,q)| + |(p2,q)|
by A3, A4, A5, C1, C2, C3, Lm8
;
hence
|((p1 + p2),q)| = |(p1,q)| + |(p2,q)|
; verum