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 ;
len x0 = 0 by EUCLID:2;
then A3: x0 = <*> (REAL 0 ) ;
A4: len (0* (len x0)) = len x0 by EUCLID:2;
then |((0* (len x0)),(0* (len x0)))| = 0 by EUCLID_2:17;
then A5: |.(0* (len x0)).| = 0 by EUCLID_2:16;
0* (len x0) = <*> (REAL 0 ) by A4, EUCLID:2;
hence contradiction by A1, A2, A3, A5, Def5; :: thesis: verum