:: deftheorem defines is_orthogonal_with INTEGRA9:def 2 :
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL holds
( f is_orthogonal_with g,A iff |||(f,g,A)||| = 0 );