let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 <> x2
let x1, x2 be Element of REAL n; :: thesis: ( x1,x2 are_lindependent2 implies x1 <> x2 )
assume A1: x1,x2 are_lindependent2 ; :: thesis: x1 <> x2
assume A2: x1 = x2 ; :: thesis: contradiction
(1 * x1) + ((- 1) * x2) = 1 * (x1 - x2) by Th12
.= 1 * (0* n) by A2, Th2
.= 0* n by EUCLID_4:2 ;
hence contradiction by A1; :: thesis: verum