let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1 // x2 holds
x1,x2 are_ldependent2
let x1, x2 be Element of REAL n; :: thesis: ( x1 // x2 implies x1,x2 are_ldependent2 )
assume x1 // x2 ; :: thesis: x1,x2 are_ldependent2
then consider r being Real such that
A1: x1 = r * x2 ;
assume A2: x1,x2 are_lindependent2 ; :: thesis: contradiction
0* n = x1 - x1 by Th2
.= (1 * x1) + (- (r * x2)) by A1, EUCLID_4:3
.= (1 * x1) + ((- r) * x2) by Th3 ;
hence contradiction by A2; :: thesis: verum