let n be Element of NAT ; :: thesis: for x, y0, y1 being Element of REAL n st x _|_ y0 & y0 // y1 holds
x _|_ y1
let x, y0, y1 be Element of REAL n; :: thesis: ( x _|_ y0 & y0 // y1 implies x _|_ y1 )
assume A1: ( x _|_ y0 & y0 // y1 ) ; :: thesis: x _|_ y1
then A2: ( x <> 0* n & y0 <> 0* n & x,y0 are_orthogonal ) by Def3;
A3: ( y0 <> 0* n & y1 <> 0* n & ex r being Real st y1 = r * y0 ) by A1, Def1;
consider r being Real such that
A4: y1 = r * y0 by A1, Def1;
|(x,y1)| = r * |(x,y0)| by A4, EUCLID_4:27
.= r * 0 by A2, EUCLID_2:def 3
.= 0 ;
then x,y1 are_orthogonal by EUCLID_2:def 3;
hence x _|_ y1 by A2, A3, Def3; :: thesis: verum