let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 <> 0* n
let x1, x2 be Element of REAL n; :: thesis: ( x1,x2 are_lindependent2 implies x1 <> 0* n )
assume A1: ( x1,x2 are_lindependent2 & not x1 <> 0* n ) ; :: thesis: contradiction
then 1 * x1 = 0* n by EUCLID_4:2;
then (1 * x1) + (0 * x2) = (0* n) + (0* n) by EUCLID_4:3
.= 0* n by EUCLID_4:1 ;
hence contradiction by A1, Def2; :: thesis: verum