theorem :: EUCLIDLP:39

for t being Real
for n being Nat
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 + (t * x2),x2 are_lindependent2