let p1, p2 be Element of REAL 3; :: thesis: p1 + p2 = |[((p1 . 1) + (p2 . 1)),((p1 . 2) + (p2 . 2)),((p1 . 3) + (p2 . 3))]|
A1: (p1 + p2) . 1 = (p1 . 1) + (p2 . 1) by RVSUM_1:11;
A2: (p1 + p2) . 2 = (p1 . 2) + (p2 . 2) by RVSUM_1:11;
(p1 + p2) . 3 = (p1 . 3) + (p2 . 3) by RVSUM_1:11;
hence p1 + p2 = |[((p1 . 1) + (p2 . 1)),((p1 . 2) + (p2 . 2)),((p1 . 3) + (p2 . 3))]| by A1, A2, Th1; :: thesis: verum