let t be Real; :: thesis: for n being Element of NAT
for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 + (t * x2),x2 are_lindependent2
let n be Element of NAT ; :: thesis: for x1, x2 being Element of REAL n st x1,x2 are_lindependent2 holds
x1 + (t * x2),x2 are_lindependent2
let x1, x2 be Element of REAL n; :: thesis: ( x1,x2 are_lindependent2 implies x1 + (t * x2),x2 are_lindependent2 )
assume A1: x1,x2 are_lindependent2 ; :: thesis: x1 + (t * x2),x2 are_lindependent2
for a, b being Real st (a * (x1 + (t * x2))) + (b * x2) = 0* n holds
( a = 0 & b = 0 )

proof

let a, b be Real; :: thesis: ( (a * (x1 + (t * x2))) + (b * x2) = 0* n implies ( a = 0 & b = 0 ) )
assume (a * (x1 + (t * x2))) + (b * x2) = 0* n ; :: thesis: ( a = 0 & b = 0 )
then A2: 0* n = (a * ((1 * x1) + (t * x2))) + (b * x2) by EUCLID_4:3
.= (((a * 1) * x1) + ((a * t) * x2)) + (b * x2) by Th26
.= (a * x1) + (((a * t) * x2) + (b * x2)) by RVSUM_1:15
.= (a * x1) + (((a * t) + b) * x2) by EUCLID_4:7 ;
then a = 0 by A1, Def2;
hence ( a = 0 & b = 0 ) by A1, A2, Def2; :: thesis: verum

end;

hence x1 + (t * x2),x2 are_lindependent2 by Def2; :: thesis: verum