let n be 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 that
A1: x _|_ y0 and
A2: y0 // y1 ; :: thesis: x _|_ y1
A3: x,y0 are_orthogonal by A1;
consider r being Real such that
A4: y1 = r * y0 by A2, Def1;
|(x,y1)| = r * |(x,y0)| by A4, EUCLID_4:22
.= r * 0 by A3, RVSUM_1:def 17
.= 0 ;
then A5: x,y1 are_orthogonal by RVSUM_1:def 17;
( x <> 0* n & y1 <> 0* n ) by A1, A2;
hence x _|_ y1 by A5; :: thesis: verum