set B = RN_Base n;
A1: { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) } c= RN_Base n

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) } or y in RN_Base n )
assume y in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) } ; :: thesis: y in RN_Base n
then ex x being Element of REAL n st
( y = x & ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) ) ;
hence y in RN_Base n ; :: thesis: verum

end;

RN_Base n c= { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in RN_Base n or y in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) } )
assume y in RN_Base n ; :: thesis: y in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) }
then ex i2 being Element of NAT st
( y = Base_FinSeq (n,i2) & 1 <= i2 & i2 <= n ) ;
hence y in { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) } ; :: thesis: verum

end;

then A2: RN_Base n = { x where x is Element of REAL n : ex i being Element of NAT st
( 1 <= i & i <= n & x = Base_FinSeq (n,i) ) } by A1, XBOOLE_0:def 10;
thus RN_Base n is R-orthogonal :: according to EUCLID_7:def 5,EUCLID_7:def 7 :: thesis: ( RN_Base n is R-normal & RN_Base n is complete )

proof

let x, y be real-valued FinSequence; :: according to EUCLID_7:def 3 :: thesis: ( x in RN_Base n & y in RN_Base n & x <> y implies |(x,y)| = 0 )
assume that
A3: x in RN_Base n and
A4: y in RN_Base n and
A5: x <> y ; :: thesis: |(x,y)| = 0
A6: ex y0 being Element of REAL n st
( y = y0 & ex i being Element of NAT st
( 1 <= i & i <= n & y0 = Base_FinSeq (n,i) ) ) by A2, A4;
ex x0 being Element of REAL n st
( x = x0 & ex i being Element of NAT st
( 1 <= i & i <= n & x0 = Base_FinSeq (n,i) ) ) by A2, A3;
hence |(x,y)| = 0 by A5, A6, Th28; :: thesis: verum

end;

thus RN_Base n is R-normal :: thesis: RN_Base n is complete

proof

let x be real-valued FinSequence; :: according to EUCLID_7:def 4 :: thesis: ( x in RN_Base n implies |.x.| = 1 )
assume x in RN_Base n ; :: thesis: |.x.| = 1
then ex x0 being Element of REAL n st
( x = x0 & ex i being Element of NAT st
( 1 <= i & i <= n & x0 = Base_FinSeq (n,i) ) ) by A2;
hence |.x.| = 1 by Th27; :: thesis: verum

end;

let B2 be R-orthonormal Subset of (REAL n); :: according to EUCLID_7:def 6 :: thesis: ( RN_Base n c= B2 implies B2 = RN_Base n )
assume A7: RN_Base n c= B2 ; :: thesis: B2 = RN_Base n

now :: thesis: B2 c= RN_Base n

assume not B2 c= RN_Base n ; :: thesis: contradiction
then consider x being object such that
A8: x in B2 and
A9: not x in RN_Base n ;
reconsider rx = x as Element of REAL n by A8;

A10: now :: thesis: not rx <> 0* n

assume rx <> 0* n ; :: thesis: contradiction
then consider i being Element of NAT such that
A11: 1 <= i and
A12: i <= n and
A13: rx . i <> 0 by JORDAN2C:46;
Base_FinSeq (n,i) in RN_Base n by A11, A12;
then |(rx,(Base_FinSeq (n,i)))| = 0 by A7, A8, A9, Def3;
hence contradiction by A11, A12, A13, Th29; :: thesis: verum

end;

|.(0* n).| = 0 by EUCLID:7;
hence contradiction by A8, A10, Def4; :: thesis: verum

end;

hence B2 = RN_Base n by A7, XBOOLE_0:def 10; :: thesis: verum