let p1, p2, p3 be Point of (TOP-REAL 3); :: thesis: p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3)
A1: (p1 <X> p2) + (p1 <X> p3) = |[((((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 ))) + (((p1 `2 ) * (p3 `3 )) - ((p1 `3 ) * (p3 `2 )))),((((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))) + (((p1 `3 ) * (p3 `1 )) - ((p1 `1 ) * (p3 `3 )))),((((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 ))) + (((p1 `1 ) * (p3 `2 )) - ((p1 `2 ) * (p3 `1 ))))]| by Th6
.= |[(((((p1 `2 ) * (p2 `3 )) - ((p1 `3 ) * (p2 `2 ))) + ((p1 `2 ) * (p3 `3 ))) - ((p1 `3 ) * (p3 `2 ))),(((((p1 `3 ) * (p2 `1 )) - ((p1 `1 ) * (p2 `3 ))) + ((p1 `3 ) * (p3 `1 ))) - ((p1 `1 ) * (p3 `3 ))),(((((p1 `1 ) * (p2 `2 )) - ((p1 `2 ) * (p2 `1 ))) + ((p1 `1 ) * (p3 `2 ))) - ((p1 `2 ) * (p3 `1 )))]| ;
A2: p2 + p3 = |[((p2 `1 ) + (p3 `1 )),((p2 `2 ) + (p3 `2 )),((p2 `3 ) + (p3 `3 ))]| by Th5;
then A3: (p2 + p3) `3 = (p2 `3 ) + (p3 `3 ) by FINSEQ_1:62;
( (p2 + p3) `1 = (p2 `1 ) + (p3 `1 ) & (p2 + p3) `2 = (p2 `2 ) + (p3 `2 ) ) by A2, FINSEQ_1:62;
hence p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3) by A3, A1; :: thesis: verum