let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n holds
x1 // x2
let x1, x2 be Element of REAL n; :: thesis: ( x1,x2 are_ldependent2 & x1 <> 0* n & x2 <> 0* n implies x1 // x2 )
assume that
A1: x1,x2 are_ldependent2 and
A2: ( x1 <> 0* n & x2 <> 0* n ) ; :: thesis: x1 // x2
consider a1, a2 being Real such that
A3: (a1 * x1) + (a2 * x2) = 0* n and
A4: ( a1 <> 0 or a2 <> 0 ) by A1;
now :: thesis: ( ( a1 <> 0 & ex t being set st x1 // x2 ) or ( a2 <> 0 & ex s being set st x1 // x2 ) )
per cases ( a1 <> 0 or a2 <> 0 ) by A4;
case A5: a1 <> 0 ; :: thesis: ex t being set st x1 // x2
set t = (- a2) / a1;
take t = (- a2) / a1; :: thesis: x1 // x2
A6: a1 * x1 = (0* n) - (a2 * x2) by A3, Th6
.= - (a2 * x2) by RVSUM_1:33 ;
x1 = 1 * x1 by EUCLID_4:3
.= (a1 / a1) * x1 by A5, XCMPLX_1:60
.= (1 / a1) * (a1 * x1) by Th1
.= (1 / a1) * ((- a2) * x2) by A6, Th3
.= ((- a2) / a1) * x2 by Th1 ;
hence x1 // x2 by A2; :: thesis: verum
end;
case A7: a2 <> 0 ; :: thesis: ex s being set st x1 // x2
set s = (- a1) / a2;
take s = (- a1) / a2; :: thesis: x1 // x2
A8: a2 * x2 = (0* n) - (a1 * x1) by A3, Th6
.= - (a1 * x1) by RVSUM_1:33 ;
x2 = 1 * x2 by EUCLID_4:3
.= (a2 / a2) * x2 by A7, XCMPLX_1:60
.= (1 / a2) * (a2 * x2) by Th1
.= (1 / a2) * ((- a1) * x1) by A8, Th3
.= ((- a1) / a2) * x1 by Th1 ;
hence x1 // x2 by A2, Def1; :: thesis: verum
end;
end;
end;
hence x1 // x2 ; :: thesis: verum