let n be Element of NAT ; :: thesis: for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds
( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )
let q1, q2 be Point of (TOP-REAL n); :: thesis: ( q1,q2 are_lindependent2 implies ( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) ) )
assume A1: q1,q2 are_lindependent2 ; :: thesis: ( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )
assume A2: ( q1 = q2 or q1 = 0. (TOP-REAL n) or q2 = 0. (TOP-REAL n) ) ; :: thesis: contradiction
now :: thesis: ( ( q1 = q2 & contradiction ) or ( q1 = 0. (TOP-REAL n) & contradiction ) or ( q2 = 0. (TOP-REAL n) & contradiction ) )
per cases ( q1 = q2 or q1 = 0. (TOP-REAL n) or q2 = 0. (TOP-REAL n) ) by A2;
case A3: q1 = q2 ; :: thesis: contradiction
(1 * q1) + ((- 1) * q2) = (1 * q1) + (- q2) by RLVECT_1:16
.= q1 + (- q2) by RLVECT_1:def 8
.= 0. (TOP-REAL n) by A3, RLVECT_1:5 ;
hence contradiction by A1; :: thesis: verum
end;
case q1 = 0. (TOP-REAL n) ; :: thesis: contradiction
then (1 * q1) + (0 * q2) = (0. (TOP-REAL n)) + (0 * q2) by RLVECT_1:10
.= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by RLVECT_1:10
.= 0. (TOP-REAL n) by RLVECT_1:4 ;
hence contradiction by A1; :: thesis: verum
end;
case q2 = 0. (TOP-REAL n) ; :: thesis: contradiction
then (0 * q1) + (1 * q2) = (0 * q1) + (0. (TOP-REAL n)) by RLVECT_1:10
.= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by RLVECT_1:10
.= 0. (TOP-REAL n) by RLVECT_1:4 ;
hence contradiction by A1; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum