let n be Nat; :: thesis: for x1, x2 being Element of REAL n st x1 // x2 holds
not x1 _|_ x2
let x1, x2 be Element of REAL n; :: thesis: ( x1 // x2 implies not x1 _|_ x2 )
assume A1: x1 // x2 ; :: thesis: not x1 _|_ x2
then consider r being Real such that
A2: x1 = r * x2 ;
x2 <> 0* n by A1;
then A3: |(x2,x2)| <> 0 by EUCLID_4:17;
x1 <> 0* n by A1;
then A4: r <> 0 by A2, EUCLID_4:3;
|(x1,x2)| = r * |(x2,x2)| by A2, EUCLID_4:21;
then |(x1,x2)| <> 0 by A4, A3, XCMPLX_1:6;
then not x1,x2 are_orthogonal by RVSUM_1:def 17;
hence not x1 _|_ x2 ; :: thesis: verum