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