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:45;
( (p2 + p3) `1 = (p2 `1) + (p3 `1) & (p2 + p3) `2 = (p2 `2) + (p3 `2) ) by A2, FINSEQ_1:45;
hence p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3) by A3, A1; :: thesis: verum