let n be Nat; :: thesis: for a being real number
for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
a * p,q are_orthogonal
let a be real number ; :: 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 by Def3;
then a * |(p,q)| = 0 ;
then |((a * p),q)| = 0 by Th41;
hence a * p,q are_orthogonal by Def3; :: thesis: verum