let B0 be Subset of ; :: 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 ;
len (0* (len x0)) = len x0 ;
then |((0* (len x0)),(0* (len x0)))| = 0 by EUCLID_2:17;
then A3: |.(0* (len x0)).| = 0 by EUCLID_2:16;
0* (len x0) = <*> (REAL 0 ) ;
hence contradiction by A1, A2, A3, Def4; :: thesis: verum