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
consider x being Element of B0;
x in B0 by A2;
then reconsider x0 = x as Element of REAL 0 ;
|((0* (len x0)),(0* (len x0)))| = 0 by EUCLID_2:17;
then |.(0* (len x0)).| = 0 by EUCLID_2:16;
hence contradiction by A1, A2, Def4; :: thesis: verum