let n be Nat; :: thesis: for a being real number
for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds
a * p,q are_orthogonal
let a be real number ; :: thesis: for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds
a * p,q are_orthogonal
let p, q be Element of n -tuples_on REAL ; :: 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