let n be 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 that
A1: x1,x2 are_lindependent2 and
A2: not x1 <> 0* n ; :: thesis: contradiction
1 * x1 = 0* n by A2, 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; :: thesis: verum