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
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) ) }
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
EUCLID_7:def 5,EUCLID_7:def 7 ( RN_Base n is R-normal & RN_Base n is complete )proof
let x,
y be
real-valued FinSequence;
EUCLID_7:def 3 ( 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
;
|(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;
verum
end;
thus
RN_Base n is R-normal
RN_Base n is complete
let B2 be R-orthonormal Subset of (REAL n); EUCLID_7:def 6 ( RN_Base n c= B2 implies B2 = RN_Base n )
assume A7:
RN_Base n c= B2
; B2 = RN_Base n
now B2 c= RN_Base nassume
not
B2 c= RN_Base n
;
contradictionthen 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 not rx <> 0* nassume
rx <> 0* n
;
contradictionthen 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;
verum end;
|.(0* n).| = 0
by EUCLID:7;
hence
contradiction
by A8, A10, Def4;
verum end;
hence
B2 = RN_Base n
by A7, XBOOLE_0:def 10; verum