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>) )
A1: for r1, r2 being Real
for R being Element of 3 -tuples_on REAL holds (r1 * R) - (r2 * R) = (r1 - r2) * R

proof

let r1, r2 be 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:49
.= (r1 + (- r2)) * R by RVSUM_1:50 ;
hence (r1 * R) - (r2 * R) = (r1 - r2) * R ; :: thesis: verum

end;

A2: ( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) ;
A3: ( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) ;
A4: ( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) ;
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:15;
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:15;
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 A1;
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:15;
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:15;
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:15;
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:15;
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 A1;
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 A1;
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:15;
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:15;
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:15;
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:50;
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:15;
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:2;
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:50;
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:15;
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:15;
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:2;
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:50;
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:15;
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:15;
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:2;
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 :: 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>) & (((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>) )

assume A5: (((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

A6: ((p2 . 1) * <e1>) . 1 = (p2 . 1) * 1 by A2, RVSUM_1:44
.= p2 . 1 ;
A7: ((p2 . 1) * <e1>) . 2 = (p2 . 1) * 0 by A2, RVSUM_1:44
.= 0 ;
A8: ((p2 . 1) * <e1>) . 3 = (p2 . 1) * 0 by A2, RVSUM_1:44
.= 0 ;
A9: ((p2 . 2) * <e2>) . 1 = (p2 . 2) * (<e2> . 1) by RVSUM_1:44
.= 0 ;
A10: ((p2 . 2) * <e2>) . 2 = (p2 . 2) * 1 by A3, RVSUM_1:44
.= p2 . 2 ;
A11: ((p2 . 2) * <e2>) . 3 = (p2 . 2) * 0 by A3, RVSUM_1:44
.= 0 ;
A12: ((p2 . 3) * <e3>) . 1 = (p2 . 3) * 0 by A4, RVSUM_1:44
.= 0 ;
A13: ((p2 . 3) * <e3>) . 2 = (p2 . 3) * 0 by A4, RVSUM_1:44
.= 0 ;
A14: ((p2 . 3) * <e3>) . 3 = (p2 . 3) * 1 by A4, RVSUM_1:44
.= p2 . 3 ;
A15: ((p3 . 1) * <e1>) . 1 = (p3 . 1) * 1 by A2, RVSUM_1:44
.= p3 . 1 ;
A16: ((p3 . 1) * <e1>) . 2 = (p3 . 1) * 0 by A2, RVSUM_1:44
.= 0 ;
A17: ((p3 . 1) * <e1>) . 3 = (p3 . 1) * 0 by A2, RVSUM_1:44
.= 0 ;
A18: ((p3 . 2) * <e2>) . 1 = (p3 . 2) * (<e2> . 1) by RVSUM_1:44
.= 0 ;
A19: ((p3 . 2) * <e2>) . 2 = (p3 . 2) * 1 by A3, RVSUM_1:44
.= p3 . 2 ;
A20: ((p3 . 2) * <e2>) . 3 = (p3 . 2) * 0 by A3, RVSUM_1:44
.= 0 ;
A21: ((p3 . 3) * <e3>) . 1 = (p3 . 3) * 0 by A4, RVSUM_1:44
.= 0 ;
A22: ((p3 . 3) * <e3>) . 2 = (p3 . 3) * 0 by A4, RVSUM_1:44
.= 0 ;
A23: ((p3 . 3) * <e3>) . 3 = (p3 . 3) * 1 by A4, RVSUM_1:44
.= p3 . 3 ;
A24: (((p2 . 1) * <e1>) + ((p2 . 2) * <e2>)) + ((p2 . 3) * <e3>) = ((p2 . 1) * <e1>) + (((p2 . 2) * <e2>) + ((p2 . 3) * <e3>)) by RVSUM_1:15
.= ((p2 . 1) * <e1>) + |[(0 + 0),((p2 . 2) + 0),(0 + (p2 . 3))]| by A9, A10, A11, A12, A13, A14, Lm2
.= |[(p2 . 1),0,0]| + |[0,(p2 . 2),(p2 . 3)]| by A6, A7, A8, Th1
.= |[((p2 . 1) + 0),(0 + (p2 . 2)),(0 + (p2 . 3))]| by Lm8
.= |[(p2 . 1),(p2 . 2),(p2 . 3)]| ;
A25: (((p3 . 1) * <e1>) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) = ((p3 . 1) * <e1>) + (((p3 . 2) * <e2>) + ((p3 . 3) * <e3>)) by RVSUM_1:15
.= ((p3 . 1) * <e1>) + |[(0 + 0),((p3 . 2) + 0),(0 + (p3 . 3))]| by A18, A19, A20, A21, A22, A23, Lm2
.= |[(p3 . 1),0,0]| + |[0,(p3 . 2),(p3 . 3)]| by A15, A16, A17, Th1
.= |[((p3 . 1) + 0),(0 + (p3 . 2)),(0 + (p3 . 3))]| by Lm8
.= |[(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:15
.= (((((p2 . 1) * <e1>) + |[(0 + 0),((p2 . 2) + 0),(0 + (p2 . 3))]|) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by A9, A10, A11, A12, A13, A14, Lm2
.= (((|[(p2 . 1),0,0]| + |[0,(p2 . 2),(p2 . 3)]|) + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by A6, A7, A8, Th1
.= ((|[((p2 . 1) + 0),(0 + (p2 . 2)),(0 + (p2 . 3))]| + ((p3 . 1) * <e1>)) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by Lm8
.= ((|[(p2 . 1),(p2 . 2),(p2 . 3)]| + |[(p3 . 1),0,0]|) + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by A15, A16, A17, Th1
.= (|[((p2 . 1) + (p3 . 1)),((p2 . 2) + 0),((p2 . 3) + 0)]| + ((p3 . 2) * <e2>)) + ((p3 . 3) * <e3>) by Lm8
.= (|[((p2 . 1) + (p3 . 1)),(p2 . 2),(p2 . 3)]| + |[0,(p3 . 2),0]|) + ((p3 . 3) * <e3>) by A18, A19, A20, Th1
.= |[(((p2 . 1) + (p3 . 1)) + 0),((p2 . 2) + (p3 . 2)),((p2 . 3) + 0)]| + ((p3 . 3) * <e3>) by Lm8
.= |[((p2 . 1) + (p3 . 1)),((p2 . 2) + (p3 . 2)),(p2 . 3)]| + |[0,0,(p3 . 3)]| by A21, A22, A23, Th1
.= |[(((p2 . 1) + (p3 . 1)) + 0),(((p2 . 2) + (p3 . 2)) + 0),((p2 . 3) + (p3 . 3))]| by Lm8 ;
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 A24, A25, Lm8; :: 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 A5, EUCLIDLP:24;
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:15;
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 A1;
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:15;
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:15;
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:37;
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:15;
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 A1;
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:15;
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:15;
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:15;
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:37;
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:15;
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 A1;
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:15;
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:15;
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:15;
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:15;
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:37;
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