let n be Nat; :: thesis: for a being Real
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; :: 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 ;
then a * |(p,q)| = 0 ;
then |((a * p),q)| = 0 by Th131;
hence a * p,q are_orthogonal ; :: thesis: verum