let p1, p2 be Element of REAL 3; :: thesis: ( p1,p2 are_ldependent2 implies p1 <X> p2 = 0.REAL 3 )
assume p1,p2 are_ldependent2 ; :: thesis: p1 <X> p2 = 0.REAL 3
then A1: ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & ( a1 <> 0 or a2 <> 0 ) ) by EUCLIDLP:def 2;

now

per cases ( ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a1 <> 0 ) or ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a2 <> 0 ) ) by A1;

case ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a1 <> 0 ) ; :: thesis: p1 <X> p2 = 0.REAL 3

then consider a1, a2 being Real such that
A3: ( a1 <> 0 & (a1 * p1) + (a2 * p2) = 0.REAL 3 ) ;
A5: (1 / a1) * (a1 * p1) = (1 / a1) * (- (a2 * p2)) by A3, RVSUM_1:41
.= (1 / a1) * (((- 1) * a2) * p2) by RVSUM_1:71
.= (1 / a1) * ((- a2) * p2) ;
A6: (1 / a1) * (a1 * p1) = (a1 * (1 / a1)) * p1 by EUCLID_4:4
.= 1 * p1 by A3, XCMPLX_1:107 ;
A7: 1 * p1 = |[(1 * (p1 . 1)),(1 * (p1 . 2)),(1 * (p1 . 3))]| by Lm3
.= p1 by Lm1 ;
A8: 0.REAL 3 = |[0,0,0]| by FINSEQ_2:76;
p1 <X> p2 = (((- a2) * (1 / a1)) * p2) <X> p2 by A5, A6, A7, EUCLID_4:4
.= (((- a2) / a1) * p2) <X> p2 by XCMPLX_1:100 ;
then p1 <X> p2 = ((- a2) / a1) * (p2 <X> p2) by Lm12;
then p1 <X> p2 = ((- a2) / a1) * (0.REAL 3) by FINSEQ_2:76
.= |[(((- a2) / a1) * ((0.REAL 3) . 1)),(((- a2) / a1) * ((0.REAL 3) . 2)),(((- a2) / a1) * ((0.REAL 3) . 3))]| by Lm3
.= |[(((- a2) / a1) * 0),(((- a2) / a1) * ((0.REAL 3) . 2)),(((- a2) / a1) * ((0.REAL 3) . 3))]| by A8, FINSEQ_1:62
.= |[0,(((- a2) / a1) * 0),(((- a2) / a1) * ((0.REAL 3) . 3))]| by A8, FINSEQ_1:62
.= 0.REAL 3 by A8, FINSEQ_1:62 ;
hence p1 <X> p2 = 0.REAL 3 ; :: thesis: verum

end;

case ex a1, a2 being Real st
( (a1 * p1) + (a2 * p2) = 0.REAL 3 & a2 <> 0 ) ; :: thesis: p1 <X> p2 = 0.REAL 3

then consider a1, a2 being Real such that
A10: ( a2 <> 0 & (a1 * p1) + (a2 * p2) = 0.REAL 3 ) ;
A12: (1 / a2) * (a2 * p2) = (1 / a2) * (- (a1 * p1)) by A10, RVSUM_1:41
.= (1 / a2) * (((- 1) * a1) * p1) by RVSUM_1:71
.= (1 / a2) * ((- a1) * p1) ;
A13: (1 / a2) * (a2 * p2) = (a2 * (1 / a2)) * p2 by EUCLID_4:4
.= 1 * p2 by A10, XCMPLX_1:107 ;
A14: 1 * p2 = |[(1 * (p2 . 1)),(1 * (p2 . 2)),(1 * (p2 . 3))]| by Lm3
.= p2 by Lm1 ;
A15: 0.REAL 3 = |[0,0,0]| by FINSEQ_2:76;
p1 <X> p2 = p1 <X> (((- a1) * (1 / a2)) * p1) by A12, A13, A14, EUCLID_4:4
.= p1 <X> (((- a1) / a2) * p1) by XCMPLX_1:100
.= (((- a1) / a2) * p1) <X> p1 by Lm12
.= ((- a1) / a2) * (p1 <X> p1) by Lm12
.= ((- a1) / a2) * (0.REAL 3) by FINSEQ_2:76
.= |[(((- a1) / a2) * ((0.REAL 3) . 1)),(((- a1) / a2) * ((0.REAL 3) . 2)),(((- a1) / a2) * ((0.REAL 3) . 3))]| by Lm3
.= |[(((- a1) / a2) * 0),(((- a1) / a2) * ((0.REAL 3) . 2)),(((- a1) / a2) * ((0.REAL 3) . 3))]| by A15, FINSEQ_1:62
.= |[0,(((- a1) / a2) * 0),(((- a1) / a2) * ((0.REAL 3) . 3))]| by A15, FINSEQ_1:62
.= 0.REAL 3 by A15, FINSEQ_1:62 ;
hence p1 <X> p2 = 0.REAL 3 ; :: thesis: verum

end;

end;

end;

hence p1 <X> p2 = 0.REAL 3 ; :: thesis: verum