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