let p1, p2, p3 be Element of REAL 3; :: thesis: p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3)
A1: p2 + p3 = |[((p2 . 1) + (p3 . 1)),((p2 . 2) + (p3 . 2)),((p2 . 3) + (p3 . 3))]| by Lm2;
then A2: (p2 + p3) . 1 = (p2 . 1) + (p3 . 1) ;
A3: (p2 + p3) . 2 = (p2 . 2) + (p3 . 2) by A1;
A4: (p2 + p3) . 3 = (p2 . 3) + (p3 . 3) by 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 Lm8
.= |[(((((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)))]| ;
hence p1 <X> (p2 + p3) = (p1 <X> p2) + (p1 <X> p3) by A2, A3, A4; :: thesis: verum