:: deftheorem defines are_orthogonal RVSUM_1:def 17 :
for p, q being real-valued FinSequence holds
( p,q are_orthogonal iff |(p,q)| = 0 );