theorem :: EUCLID_7:19

for n being Nat
for B0 being Subset of (REAL n)
for y being Element of REAL n st B0 is orthogonal_basis & ( for x being Element of REAL n st x in B0 holds
|(x,y)| = 0 ) holds
y = 0* n