let B0 be Subset of (REAL 0); :: thesis: ( B0 is orthogonal_basis implies B0 = {} )
assume that
A1: B0 is orthogonal_basis and
A2: B0 <> {} ; :: thesis: contradiction
set x = the Element of B0;
the Element of B0 in B0 by A2;
then reconsider x0 = the Element of B0 as Element of REAL 0 ;
|((0* (len x0)),(0* (len x0)))| = 0 by EUCLID_2:9;
then |.(0* (len x0)).| = 0 ;
hence contradiction by A1, A2, Def4; :: thesis: verum