let n be Nat; :: thesis: for a being Real

for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

a * p,q are_orthogonal

let a be Real; :: thesis: for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

a * p,q are_orthogonal

let p, q be Point of (TOP-REAL n); :: thesis: ( p,q are_orthogonal implies a * p,q are_orthogonal )

assume p,q are_orthogonal ; :: thesis: a * p,q are_orthogonal

then |(p,q)| = 0 ;

then a * |(p,q)| = 0 ;

then |((a * p),q)| = 0 by Th17;

hence a * p,q are_orthogonal ; :: thesis: verum

for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

a * p,q are_orthogonal

let a be Real; :: thesis: for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds

a * p,q are_orthogonal

let p, q be Point of (TOP-REAL n); :: thesis: ( p,q are_orthogonal implies a * p,q are_orthogonal )

assume p,q are_orthogonal ; :: thesis: a * p,q are_orthogonal

then |(p,q)| = 0 ;

then a * |(p,q)| = 0 ;

then |((a * p),q)| = 0 by Th17;

hence a * p,q are_orthogonal ; :: thesis: verum