let p1, p2, p3 be Element of REAL 3; :: thesis: ( (((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>) = ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) iff (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) )
F2: for r1, r2 being Element of REAL
for R being Element of 3 -tuples_on REAL holds (r1 * R) - (r2 * R) = (r1 - r2) * R

proof

let r1, r2 be Element of REAL ; :: thesis: for R being Element of 3 -tuples_on REAL holds (r1 * R) - (r2 * R) = (r1 - r2) * R
let R be Element of 3 -tuples_on REAL; :: thesis: (r1 * R) - (r2 * R) = (r1 - r2) * R
(r1 * R) - (r2 * R) = (r1 * R) + (((- 1) * r2) * R) by RVSUM_1:71
.= (r1 + (- r2)) * R by RVSUM_1:72 ;
hence (r1 * R) - (r2 * R) = (r1 - r2) * R ; :: thesis: verum

end;

A1: ( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) by FINSEQ_1:62;
A2: ( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) by FINSEQ_1:62;
A3: ( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) by FINSEQ_1:62;
thus ( (((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>) = ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) implies (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) ) :: thesis: ( (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) implies (((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>) = ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) )

proof

assume (((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>) = ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) ; :: thesis: (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>)
then (((((p1 . 1) * <e1>) + (((p1 . 2) * <e2>) + ((p1 . 3) * <e3>))) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then (((((p1 . 1) * <e1>) - ((p3 . 1) * <e1>)) + (((p1 . 2) * <e2>) + ((p1 . 3) * <e3>))) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then (((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) * <e2>) + ((p1 . 3) * <e3>))) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by F2;
then ((((((p1 . 1) - (p3 . 1)) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((((p1 . 1) - (p3 . 1)) * <e1>) + ((p1 . 2) * <e2>)) - ((p3 . 2) * <e2>)) + ((p1 . 3) * <e3>)) - ((p3 . 3) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then (((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) * <e2>) + (- ((p3 . 2) * <e2>)))) + ((p1 . 3) * <e3>)) + (- ((p3 . 3) * <e3>)) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) * <e2>) - ((p3 . 2) * <e2>))) + (((p1 . 3) * <e3>) - ((p3 . 3) * <e3>)) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) * <e3>) - ((p3 . 3) * <e3>)) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by F2;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 1) * <e1>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by F2;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) - ((p3 . 1) * <e1>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) - ((p3 . 1) * <e1>)) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((((p2 . 1) + (p3 . 1)) * <e1>) - ((p3 . 1) * <e1>)) + (((p2 . 2) + (p3 . 2)) * <e2>)) - ((p3 . 2) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((((p2 . 1) * <e1>) + ((p3 . 1) * <e1>)) + (- ((p3 . 1) * <e1>))) + (((p2 . 2) + (p3 . 2)) * <e2>)) - ((p3 . 2) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by RVSUM_1:72;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = ((((((p2 . 1) * <e1>) + (((p3 . 1) * <e1>) - ((p3 . 1) * <e1>))) + (((p2 . 2) + (p3 . 2)) * <e2>)) - ((p3 . 2) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = ((((((p2 . 1) * <e1>) + (0.REAL 3)) + (((p2 . 2) + (p3 . 2)) * <e2>)) - ((p3 . 2) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by EUCLIDLP:7;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((p2 . 1) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) - ((p3 . 2) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by EUCLID_4:1;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((p2 . 1) * <e1>) + (((p2 . 2) * <e2>) + ((p3 . 2) * <e2>))) - ((p3 . 2) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by RVSUM_1:72;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = ((((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p3 . 2) * <e2>)) + (- ((p3 . 2) * <e2>))) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + (((p3 . 2) * <e2>) + (- ((p3 . 2) * <e2>)))) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + (0.REAL 3)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by EUCLIDLP:7;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = ((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>)) - ((p3 . 3) * <e3>) by EUCLID_4:1;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = ((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + (((p2 . 3) * <e3>) + ((p3 . 3) * <e3>))) - ((p3 . 3) * <e3>) by RVSUM_1:72;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = (((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + ((p3 . 3) * <e3>)) - ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = ((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + (((p3 . 3) * <e3>) + (- ((p3 . 3) * <e3>))) by RVSUM_1:32;
then ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) = ((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + (0.REAL 3) by EUCLIDLP:7;
hence (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) by EUCLID_4:1; :: thesis: verum

end;

now

assume C1: (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) ; :: thesis: ( (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) implies (((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>) = ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) )
((((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) = ((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + ((((p3 . 1) * <e1>) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>))

proof

D1: ((p2 . 1) * <e1>) . 1 = (p2 . 1) * 1 by A1, RVSUM_1:66
.= p2 . 1 ;
D2: ((p2 . 1) * <e1>) . 2 = (p2 . 1) * 0 by A1, RVSUM_1:66
.= 0 ;
D3: ((p2 . 1) * <e1>) . 3 = (p2 . 1) * 0 by A1, RVSUM_1:66
.= 0 ;
D4: ((p2 . 2) * <e2>) . 1 = (p2 . 2) * (<e2> . 1) by RVSUM_1:66
.= 0 by A2 ;
D5: ((p2 . 2) * <e2>) . 2 = (p2 . 2) * 1 by A2, RVSUM_1:66
.= p2 . 2 ;
D6: ((p2 . 2) * <e2>) . 3 = (p2 . 2) * 0 by A2, RVSUM_1:66
.= 0 ;
D7: ((p2 . 3) * <e3>) . 1 = (p2 . 3) * 0 by A3, RVSUM_1:66
.= 0 ;
D8: ((p2 . 3) * <e3>) . 2 = (p2 . 3) * 0 by A3, RVSUM_1:66
.= 0 ;
D9: ((p2 . 3) * <e3>) . 3 = (p2 . 3) * 1 by A3, RVSUM_1:66
.= p2 . 3 ;
D10: ((p3 . 1) * <e1>) . 1 = (p3 . 1) * 1 by A1, RVSUM_1:66
.= p3 . 1 ;
D11: ((p3 . 1) * <e1>) . 2 = (p3 . 1) * 0 by A1, RVSUM_1:66
.= 0 ;
D12: ((p3 . 1) * <e1>) . 3 = (p3 . 1) * 0 by A1, RVSUM_1:66
.= 0 ;
D13: ((p3 . 2) * <e2>) . 1 = (p3 . 2) * (<e2> . 1) by RVSUM_1:66
.= 0 by A2 ;
D14: ((p3 . 2) * <e2>) . 2 = (p3 . 2) * 1 by A2, RVSUM_1:66
.= p3 . 2 ;
D15: ((p3 . 2) * <e2>) . 3 = (p3 . 2) * 0 by A2, RVSUM_1:66
.= 0 ;
D16: ((p3 . 3) * <e3>) . 1 = (p3 . 3) * 0 by A3, RVSUM_1:66
.= 0 ;
D17: ((p3 . 3) * <e3>) . 2 = (p3 . 3) * 0 by A3, RVSUM_1:66
.= 0 ;
D18: ((p3 . 3) * <e3>) . 3 = (p3 . 3) * 1 by A3, RVSUM_1:66
.= p3 . 3 ;
D19: (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((p2 . 1) * <e1>) + (((p2 . 2) * <e2>) + ((p2 . 3) * <e3>)) by RVSUM_1:32
.= ((p2 . 1) * <e1>) + |[(0 + 0),((p2 . 2) + 0),(0 + (p2 . 3))]| by D4, D5, D6, D7, D8, D9, Lm4
.= |[(p2 . 1),0,0]| + |[0,(p2 . 2),(p2 . 3)]| by D1, D2, D3, Lm1
.= |[((p2 . 1) + 0),(0 + (p2 . 2)),(0 + (p2 . 3))]| by LmA31
.= |[(p2 . 1),(p2 . 2),(p2 . 3)]| ;
D20: (((p3 . 1) * <e1>) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) = ((p3 . 1) * <e1>) + (((p3 . 2) * <e2>) + ((p3 . 3) * <e3>)) by RVSUM_1:32
.= ((p3 . 1) * <e1>) + |[(0 + 0),((p3 . 2) + 0),(0 + (p3 . 3))]| by D13, D14, D15, D16, D17, D18, Lm4
.= |[(p3 . 1),0,0]| + |[0,(p3 . 2),(p3 . 3)]| by D10, D11, D12, Lm1
.= |[((p3 . 1) + 0),(0 + (p3 . 2)),(0 + (p3 . 3))]| by LmA31
.= |[(p3 . 1),(p3 . 2),(p3 . 3)]| ;
((((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) = (((((p2 . 1) * <e1>) + (((p2 . 2) * <e2>) + ((p2 . 3) * <e3>))) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by RVSUM_1:32
.= (((((p2 . 1) * <e1>) + |[(0 + 0),((p2 . 2) + 0),(0 + (p2 . 3))]|) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by D4, D5, D6, D7, D8, D9, Lm4
.= (((|[(p2 . 1),0,0]| + |[0,(p2 . 2),(p2 . 3)]|) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by D1, D2, D3, Lm1
.= ((|[((p2 . 1) + 0),(0 + (p2 . 2)),(0 + (p2 . 3))]| + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by LmA31
.= ((|[(p2 . 1),(p2 . 2),(p2 . 3)]| + |[(p3 . 1),0,0]|) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by D10, D11, D12, Lm1
.= (|[((p2 . 1) + (p3 . 1)),((p2 . 2) + 0),((p2 . 3) + 0)]| + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by LmA31
.= (|[((p2 . 1) + (p3 . 1)),(p2 . 2),(p2 . 3)]| + |[0,(p3 . 2),0]|) + ((p3 . 3) * <e3>) by D13, D14, D15, Lm1
.= |[(((p2 . 1) + (p3 . 1)) + 0),((p2 . 2) + (p3 . 2)),((p2 . 3) + 0)]| + ((p3 . 3) * <e3>) by LmA31
.= |[((p2 . 1) + (p3 . 1)),((p2 . 2) + (p3 . 2)),(p2 . 3)]| + |[0,0,(p3 . 3)]| by D16, D17, D18, Lm1
.= |[(((p2 . 1) + (p3 . 1)) + 0),(((p2 . 2) + (p3 . 2)) + 0),((p2 . 3) + (p3 . 3))]| by LmA31 ;
hence ((((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) = ((((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>)) + ((((p3 . 1) * <e1>) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>)) by D19, D20, LmA31; :: thesis: verum

end;

then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>)) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by EUCLIDLP:29, C1;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((((p1 . 1) - (p3 . 1)) * <e1>) + ((((p1 . 2) - (p3 . 2)) * <e2>) + (((p1 . 3) - (p3 . 3)) * <e3>))) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((((p1 . 1) * <e1>) - ((p3 . 1) * <e1>)) + ((((p1 . 2) - (p3 . 2)) * <e2>) + (((p1 . 3) - (p3 . 3)) * <e3>))) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by F2;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((((p1 . 1) * <e1>) + ((((p1 . 2) - (p3 . 2)) * <e2>) + (((p1 . 3) - (p3 . 3)) * <e3>))) - ((p3 . 1) * <e1>)) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + ((((p1 . 2) - (p3 . 2)) * <e2>) + (((p1 . 3) - (p3 . 3)) * <e3>))) + (((p3 . 1) * <e1>) - ((p3 . 1) * <e1>))) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + ((((p1 . 2) - (p3 . 2)) * <e2>) + (((p1 . 3) - (p3 . 3)) * <e3>))) + (0.REAL 3)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by RVSUM_1:58;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((p1 . 1) * <e1>) + ((((p1 . 2) - (p3 . 2)) * <e2>) + (((p1 . 3) - (p3 . 3)) * <e3>))) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by EUCLID_4:1;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) * <e3>) - ((p3 . 3) * <e3>))) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by F2;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + ((p1 . 3) * <e3>)) - ((p3 . 3) * <e3>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + ((p1 . 3) * <e3>)) + ((p3 . 2) * <e2>)) - ((p3 . 3) * <e3>)) + ((p3 . 3) * <e3>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + ((p1 . 3) * <e3>)) + ((p3 . 2) * <e2>)) + (((p3 . 3) * <e3>) - ((p3 . 3) * <e3>)) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + ((p1 . 3) * <e3>)) + ((p3 . 2) * <e2>)) + (0.REAL 3) by RVSUM_1:58;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + ((p1 . 3) * <e3>)) + ((p3 . 2) * <e2>) by EUCLID_4:1;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((p1 . 1) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) * <e3>) + ((p3 . 2) * <e2>)) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((p1 . 1) * <e1>) + (((p1 . 2) * <e2>) - ((p3 . 2) * <e2>))) + (((p1 . 3) * <e3>) + ((p3 . 2) * <e2>)) by F2;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + (- ((p3 . 2) * <e2>))) + (((p1 . 3) * <e3>) + ((p3 . 2) * <e2>)) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) - ((p3 . 2) * <e2>)) + ((p1 . 3) * <e3>)) + ((p3 . 2) * <e2>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = (((((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>)) - ((p3 . 2) * <e2>)) + ((p3 . 2) * <e2>) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>)) + (((p3 . 2) * <e2>) - ((p3 . 2) * <e2>)) by RVSUM_1:32;
then ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) = ((((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>)) + (0.REAL 3) by RVSUM_1:58;
hence ( (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) implies (((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>) = ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) ) by EUCLID_4:1; :: thesis: verum

end;

hence ( (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((((p1 . 1) - (p3 . 1)) * <e1>) + (((p1 . 2) - (p3 . 2)) * <e2>)) + (((p1 . 3) - (p3 . 3)) * <e3>) implies (((p1 . 1) * <e1>) + ((p1 . 2) * <e2>)) + ((p1 . 3) * <e3>) = ((((p2 . 1) + (p3 . 1)) * <e1>) + (((p2 . 2) + (p3 . 2)) * <e2>)) + (((p2 . 3) + (p3 . 3)) * <e3>) ) ; :: thesis: verum