let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n st x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n holds
x1 // x2
let x1, x2 be Element of REAL n; :: thesis: ( x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n implies x1 // x2 )
assume A1: ( x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n ) ; :: thesis: x1 // x2
then consider a1, a2 being Real such that
A2: ( (a1 * x1) + (a2 * x2) = 0* n & ( a1 <> 0 or a2 <> 0 ) ) by Def2;

now

per cases ( a1 <> 0 or a2 <> 0 ) by A2;

case A3: a1 <> 0 ; :: thesis: ex t being Element of REAL st x1 // x2

A4: a1 * x1 = (0* n) - (a2 * x2) by A2, Th11
.= - (a2 * x2) by RVSUM_1:54 ;
A5: x1 = 1 * x1 by EUCLID_4:3
.= (a1 / a1) * x1 by A3, XCMPLX_1:60
.= (1 / a1) * (a1 * x1) by Th1
.= (1 / a1) * ((- a2) * x2) by A4, Th8
.= ((- a2) / a1) * x2 by Th1 ;
set t = (- a2) / a1;
take t = (- a2) / a1; :: thesis: x1 // x2
thus x1 // x2 by A1, A5, Def1; :: thesis: verum

end;

case A6: a2 <> 0 ; :: thesis: ex s being Element of REAL st x1 // x2

A7: a2 * x2 = (0* n) - (a1 * x1) by A2, Th11
.= - (a1 * x1) by RVSUM_1:54 ;
A8: x2 = 1 * x2 by EUCLID_4:3
.= (a2 / a2) * x2 by A6, XCMPLX_1:60
.= (1 / a2) * (a2 * x2) by Th1
.= (1 / a2) * ((- a1) * x1) by A7, Th8
.= ((- a1) / a2) * x1 by Th1 ;
set s = (- a1) / a2;
take s = (- a1) / a2; :: thesis: x1 // x2
thus x1 // x2 by A1, A8, Def1; :: thesis: verum

end;

end;

end;

hence x1 // x2 ; :: thesis: verum