let n be Nat; :: thesis: 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
let B0 be Subset of (REAL n); :: thesis: 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
let y be Element of REAL n; :: thesis: ( B0 is orthogonal_basis & ( for x being Element of REAL n st x in B0 holds
|(x,y)| = 0 ) implies y = 0* n )
assume that
A1: B0 is orthogonal_basis and
A2: for x being Element of REAL n st x in B0 holds
|(x,y)| = 0 ; :: thesis: y = 0* n

now

reconsider y1 = (1 / |.y.|) * y as Element of REAL n ;
reconsider B3 = {y1} as Subset of (REAL n) ;
reconsider B1 = B0 \/ {y1} as Subset of (REAL n) ;
y1 in {y1} by TARSKI:def 1;
then A3: y1 in B1 by XBOOLE_0:def 3;
A4: len y = n by FINSEQ_1:def 18;
for x2, y2 being real-valued FinSequence st x2 in B1 & y2 in B1 & x2 <> y2 holds
|(x2,y2)| = 0

proof

let x2, y2 be real-valued FinSequence; :: thesis: ( x2 in B1 & y2 in B1 & x2 <> y2 implies |(x2,y2)| = 0 )
assume that
A5: x2 in B1 and
A6: y2 in B1 and
A7: x2 <> y2 ; :: thesis: |(x2,y2)| = 0
reconsider X2 = x2, Y2 = y2 as Element of REAL n by A5, A6;
A8: len Y2 = n by FINSEQ_1:def 18;

per cases ( x2 in B0 or x2 in {y1} ) by A5, XBOOLE_0:def 3;

suppose A9: x2 in B0 ; :: thesis: |(x2,y2)| = 0

per cases ( y2 in B0 or y2 in {y1} ) by A6, XBOOLE_0:def 3;

suppose y2 in B0 ; :: thesis: |(x2,y2)| = 0

hence |(x2,y2)| = 0 by A1, A7, A9, Def3; :: thesis: verum

end;

suppose A10: y2 in {y1} ; :: thesis: |(x2,y2)| = 0

A11: len X2 = n by FINSEQ_1:def 18;
|(x2,y)| = 0 by A2, A9;
then A12: (1 / |.y.|) * |(x2,y)| = 0 ;
y2 = y1 by A10, TARSKI:def 1;
hence |(x2,y2)| = 0 by A4, A11, A12, RVSUM_1:151; :: thesis: verum

end;

end;

end;

suppose A13: x2 in {y1} ; :: thesis: |(x2,y2)| = 0

then x2 = y1 by TARSKI:def 1;
then not y2 in {y1} by A7, TARSKI:def 1;
then y2 in B0 by A6, XBOOLE_0:def 3;
then |(y2,y)| = 0 by A2;
then (1 / |.y.|) * |(y2,y)| = 0 ;
then |(Y2,((1 / |.y.|) * y))| = 0 by A4, A8, RVSUM_1:151;
hence |(x2,y2)| = 0 by A13, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A14: B1 is R-orthogonal by Def3;
reconsider B = B0 as R-orthonormal Subset of (REAL n) by A1;
assume A15: y <> 0* n ; :: thesis: contradiction
A16: |.y1.| = (abs (1 / |.y.|)) * |.y.| by EUCLID:14
.= (1 / |.y.|) * |.y.| by ABSVALUE:def 1
.= 1 by A15, EUCLID:11, XCMPLX_1:107 ;
for x being real-valued FinSequence st x in B1 holds
|.x.| = 1

proof

let x be real-valued FinSequence; :: thesis: ( x in B1 implies |.x.| = 1 )
assume x in B1 ; :: thesis: |.x.| = 1
then ( x in B0 or x in {y1} ) by XBOOLE_0:def 3;
hence |.x.| = 1 by A1, A16, Def4, TARSKI:def 1; :: thesis: verum

end;

then A17: B1 is R-normal by Def4;
A18: len y1 = n by FINSEQ_1:def 18;

A19: now

assume y1 in B0 ; :: thesis: contradiction
then |(y1,y)| = 0 by A2;
then (1 / |.y.|) * |(y1,y)| = 0 ;
then |(y1,((1 / |.y.|) * y))| = 0 by A4, A18, RVSUM_1:151;
hence contradiction by A16, EUCLID_2:16; :: thesis: verum

end;

B0 c= B1 by XBOOLE_1:7;
hence contradiction by A1, A19, A3, A14, A17, Def6; :: thesis: verum

end;

hence y = 0* n ; :: thesis: verum