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