let n be Element of NAT ; :: thesis: for x, y being Element of REAL n st x _|_ y holds
x,y are_lindependent2
let x, y be Element of REAL n; :: thesis: ( x _|_ y implies x,y are_lindependent2 )
assume x _|_ y ; :: thesis: x,y are_lindependent2
then A1: ( x <> 0* n & y <> 0* n & x,y are_orthogonal ) by Def3;
then A2: |(x,y)| = 0 by EUCLID_2:def 3;
A3: ( |(x,x)| <> 0 & |(y,y)| <> 0 ) by A1, EUCLID_4:22;
then A4: ( |(x,x)| > 0 & |(y,y)| > 0 ) by EUCLID_2:11;
for a, b being Real st (a * x) + (b * y) = 0* n holds
( a = 0 & b = 0 )

proof

let a, b be Real; :: thesis: ( (a * x) + (b * y) = 0* n implies ( a = 0 & b = 0 ) )
assume (a * x) + (b * y) = 0* n ; :: thesis: ( a = 0 & b = 0 )
then A5: 0 = |(((a * x) + (b * y)),((a * x) + (b * y)))| by EUCLID_4:22
.= (|((a * x),(a * x))| + (2 * |((a * x),(b * y))|)) + |((b * y),(b * y))| by EUCLID_4:37
.= ((a * |(x,(a * x))|) + (2 * |((a * x),(b * y))|)) + |((b * y),(b * y))| by EUCLID_4:26
.= ((a * |(x,(a * x))|) + (2 * (a * |(x,(b * y))|))) + |((b * y),(b * y))| by EUCLID_4:26
.= ((a * |(x,(a * x))|) + ((2 * a) * |(x,(b * y))|)) + (b * |(y,(b * y))|) by EUCLID_4:26
.= ((a * (a * |(x,x)|)) + ((2 * a) * |(x,(b * y))|)) + (b * |(y,(b * y))|) by EUCLID_4:27
.= (((a * a) * |(x,x)|) + ((2 * a) * (b * |(x,y)|))) + (b * |(y,(b * y))|) by EUCLID_4:27
.= (((a * a) * |(x,x)|) + (((2 * a) * b) * |(x,y)|)) + (b * (b * |(y,y)|)) by EUCLID_4:27
.= ((a * a) * |(x,x)|) + ((b * b) * |(y,y)|) by A2 ;
( a * a >= 0 & b * b >= 0 ) by XREAL_1:65;
then A6: ( (a * a) * |(x,x)| >= 0 & (b * b) * |(y,y)| >= 0 ) by A4;
A7: a * a = 0

proof

assume a * a <> 0 ; :: thesis: contradiction
then a * a > 0 by XREAL_1:65;
then (a * a) * |(x,x)| > 0 by A4, XREAL_1:131;
then ((a * a) * |(x,x)|) + ((b * b) * |(y,y)|) > 0 + 0 by A6;
hence contradiction by A5; :: thesis: verum

end;

then b * b = 0 by A3, A5, XCMPLX_1:6;
hence ( a = 0 & b = 0 ) by A7, XCMPLX_1:6; :: thesis: verum

end;

hence x,y are_lindependent2 by Def2; :: thesis: verum