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

assume A3: y <> 0* n ; :: thesis: contradiction
reconsider y1 = (1 / |.y.|) * y as Element of REAL n ;
A4: |.y1.| = (abs (1 / |.y.|)) * |.y.| by EUCLID:14
.= (1 / |.y.|) * |.y.| by ABSVALUE:def 1
.= 1 by A3, EUCLID:11, XCMPLX_1:107 ;
A5: ( len y = n & len y1 = n ) by FINSEQ_1:def 18;

A6: 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 A5, EUCLID_2:21;
hence contradiction by A4, EUCLID_2:16; :: thesis: verum

end;

A7: y1 in {y1} by TARSKI:def 1;
reconsider B3 = {y1} as Subset of (REAL n) ;
reconsider B1 = B0 \/ {y1} as Subset of (REAL n) ;
A8: y1 in B1 by A7, XBOOLE_0:def 3;
A9: B0 c= B1 by XBOOLE_1:7;
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 A10: ( x2 in B1 & y2 in B1 & x2 <> y2 ) ; :: thesis: |(x2,y2)| = 0
then reconsider X2 = x2, Y2 = y2 as Element of REAL n ;
A11: len Y2 = n by FINSEQ_1:def 18;

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

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

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

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

hence |(x2,y2)| = 0 by A1, A10, A12, Def4; :: thesis: verum

end;

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

then A13: y2 = y1 by TARSKI:def 1;
A14: len X2 = n by FINSEQ_1:def 18;
|(x2,y)| = 0 by A2, A12;
then (1 / |.y.|) * |(x2,y)| = 0 ;
hence |(x2,y2)| = 0 by A5, A13, A14, EUCLID_2:21; :: thesis: verum

end;

end;

end;

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

then x2 = y1 by TARSKI:def 1;
then not y2 in {y1} by A10, TARSKI:def 1;
then y2 in B0 by A10, XBOOLE_0:def 3;
then |(y2,y)| = 0 by A2;
then (1 / |.y.|) * |(y2,y)| = 0 ;
then |(Y2,((1 / |.y.|) * y))| = 0 by A5, A11, EUCLID_2:21;
hence |(x2,y2)| = 0 by A15, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then A16: B1 is R-orthogonal by Def4;
reconsider B = B0 as R-orthonormal Subset of (REAL n) by A1;
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, A4, Def5, TARSKI:def 1; :: thesis: verum

end;

then B1 is R-normal by Def5;
hence contradiction by A6, A8, A9, A1, A16, Def7; :: thesis: verum

end;

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