let p1, p2, q be Element of REAL 3; |((p1 + p2),q)| = |(p1,q)| + |(p2,q)|
A1:
|(p1,q)| = (((p1 . 1) * (q . 1)) + ((p1 . 2) * (q . 2))) + ((p1 . 3) * (q . 3))
by Lm5;
A2:
|(p2,q)| = (((p2 . 1) * (q . 1)) + ((p2 . 2) * (q . 2))) + ((p2 . 3) * (q . 3))
by Lm5;
A3:
p1 + p2 = |[((p1 . 1) + (p2 . 1)),((p1 . 2) + (p2 . 2)),((p1 . 3) + (p2 . 3))]|
by Th55;
set p = p1 + p2;
A4:
(p1 + p2) . 2 = (p1 . 2) + (p2 . 2)
by A3, FINSEQ_1:45;
A5:
(p1 + p2) . 3 = (p1 . 3) + (p2 . 3)
by A3, FINSEQ_1:45;
|((p1 + p2),q)| = ((((p1 + p2) . 1) * (q . 1)) + (((p1 + p2) . 2) * (q . 2))) + (((p1 + p2) . 3) * (q . 3))
by Lm5;
then
|((p1 + p2),q)| = ((((p1 . 1) + (p2 . 1)) * (q . 1)) + (((p1 . 2) + (p2 . 2)) * (q . 2))) + (((p1 . 3) + (p2 . 3)) * (q . 3))
by A3, A4, A5, FINSEQ_1:45;
hence
|((p1 + p2),q)| = |(p1,q)| + |(p2,q)|
by A1, A2; verum