let G be RealNormSpace-Sequence; :: thesis: ( ( for i being Element of dom G holds G . i is complete ) implies product G is complete )

assume A1: for i being Element of dom G holds G . i is complete ; :: thesis: product G is complete

reconsider I = len G as Element of NAT ;

A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

for seq being sequence of (product G) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

assume A1: for i being Element of dom G holds G . i is complete ; :: thesis: product G is complete

reconsider I = len G as Element of NAT ;

A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

for seq being sequence of (product G) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

proof

hence
product G is complete
by LOPBAN_1:def 15; :: thesis: verum
let seq be sequence of (product G); :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )

defpred S_{1}[ Nat, object ] means ex i being Element of dom G st

( i = $1 & ex seqi being sequence of (G . i) st

( seqi is convergent & $2 = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) );

assume A3: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

A4: for k being Nat st k in Seg I holds

ex x being object st S_{1}[k,x]

A14: ( dom yy0 = Seg I & ( for j being Nat st j in Seg I holds

S_{1}[j,yy0 . j] ) )
from FINSEQ_1:sch 1(A4);

A15: len yy0 = I by A14, FINSEQ_1:def 3;

then A16: len yy0 = len (carr G) by Def4;

then reconsider y0 = yy0 as Element of product (carr G) by A14, A17, CARD_3:9;

x0 = y0 ;

hence seq is convergent by A18, Th13; :: thesis: verum

end;defpred S

( i = $1 & ex seqi being sequence of (G . i) st

( seqi is convergent & $2 = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) );

assume A3: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

A4: for k being Nat st k in Seg I holds

ex x being object st S

proof

consider yy0 being FinSequence such that
let k be Nat; :: thesis: ( k in Seg I implies ex x being object st S_{1}[k,x] )

assume k in Seg I ; :: thesis: ex x being object st S_{1}[k,x]

then reconsider i = k as Element of dom G by FINSEQ_1:def 3;

defpred S_{2}[ Element of NAT , Element of (G . i)] means ex seqm being Element of product (carr G) st

( seqm = seq . $1 & $2 = seqm . i );

A5: for x being Element of NAT ex y being Element of (G . i) st S_{2}[x,y]

for x being Element of NAT holds S_{2}[x,f . x]
from FUNCT_2:sch 3(A5);

then consider seqi being sequence of (G . i) such that

A8: for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ;

A9: for m being Nat ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i )_{1}[k, lim seqi]

G . i is complete by A1;

then seqi is convergent by A13, LOPBAN_1:def 15;

hence S_{1}[k, lim seqi]
by A8; :: thesis: verum

end;assume k in Seg I ; :: thesis: ex x being object st S

then reconsider i = k as Element of dom G by FINSEQ_1:def 3;

defpred S

( seqm = seq . $1 & $2 = seqm . i );

A5: for x being Element of NAT ex y being Element of (G . i) st S

proof

ex f being sequence of the carrier of (G . i) st
let x be Element of NAT ; :: thesis: ex y being Element of (G . i) st S_{2}[x,y]

consider seqm being Element of product (carr G) such that

A6: seqm = seq . x by A2;

len G = len (carr G) by Def4;

then A7: dom G = dom (carr G) by FINSEQ_3:29;

take seqm . i ; :: thesis: ( seqm . i is Element of (G . i) & S_{2}[x,seqm . i] )

(carr G) . i = the carrier of (G . i) by Def4;

hence ( seqm . i is Element of (G . i) & S_{2}[x,seqm . i] )
by A6, A7, CARD_3:9; :: thesis: verum

end;consider seqm being Element of product (carr G) such that

A6: seqm = seq . x by A2;

len G = len (carr G) by Def4;

then A7: dom G = dom (carr G) by FINSEQ_3:29;

take seqm . i ; :: thesis: ( seqm . i is Element of (G . i) & S

(carr G) . i = the carrier of (G . i) by Def4;

hence ( seqm . i is Element of (G . i) & S

for x being Element of NAT holds S

then consider seqi being sequence of (G . i) such that

A8: for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ;

A9: for m being Nat ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i )

proof

take
lim seqi
; :: thesis: S
let n be Nat; :: thesis: ex seqm being Element of product (carr G) st

( seqm = seq . n & seqi . n = seqm . i )

n in NAT by ORDINAL1:def 12;

hence ex seqm being Element of product (carr G) st

( seqm = seq . n & seqi . n = seqm . i ) by A8; :: thesis: verum

end;( seqm = seq . n & seqi . n = seqm . i )

n in NAT by ORDINAL1:def 12;

hence ex seqm being Element of product (carr G) st

( seqm = seq . n & seqi . n = seqm . i ) by A8; :: thesis: verum

now :: thesis: for r1 being Real st r1 > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1

then A13:
seqi is Cauchy_sequence_by_Norm
by RSSPACE3:8;ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1

let r1 be Real; :: thesis: ( r1 > 0 implies ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1 )

assume A10: r1 > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1

reconsider r = r1 as Element of REAL by XREAL_0:def 1;

consider k being Nat such that

A11: for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r by A3, A10, RSSPACE3:8;

take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seqi . n) - (seqi . m)).|| < r1 )

assume ( n >= k & m >= k ) ; :: thesis: ||.((seqi . n) - (seqi . m)).|| < r1

then A12: ||.((seq . n) - (seq . m)).|| < r by A11;

( ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) & ex seqn being Element of product (carr G) st

( seqn = seq . n & seqi . n = seqn . i ) ) by A9;

then ||.((seqi . n) - (seqi . m)).|| <= ||.((seq . n) - (seq . m)).|| by Th11;

hence ||.((seqi . n) - (seqi . m)).|| < r1 by A12, XXREAL_0:2; :: thesis: verum

end;for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1 )

assume A10: r1 > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1

reconsider r = r1 as Element of REAL by XREAL_0:def 1;

consider k being Nat such that

A11: for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r by A3, A10, RSSPACE3:8;

take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds

||.((seqi . n) - (seqi . m)).|| < r1

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seqi . n) - (seqi . m)).|| < r1 )

assume ( n >= k & m >= k ) ; :: thesis: ||.((seqi . n) - (seqi . m)).|| < r1

then A12: ||.((seq . n) - (seq . m)).|| < r by A11;

( ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) & ex seqn being Element of product (carr G) st

( seqn = seq . n & seqi . n = seqn . i ) ) by A9;

then ||.((seqi . n) - (seqi . m)).|| <= ||.((seq . n) - (seq . m)).|| by Th11;

hence ||.((seqi . n) - (seqi . m)).|| < r1 by A12, XXREAL_0:2; :: thesis: verum

G . i is complete by A1;

then seqi is convergent by A13, LOPBAN_1:def 15;

hence S

A14: ( dom yy0 = Seg I & ( for j being Nat st j in Seg I holds

S

A15: len yy0 = I by A14, FINSEQ_1:def 3;

then A16: len yy0 = len (carr G) by Def4;

A17: now :: thesis: for i being object st i in dom (carr G) holds

yy0 . i in (carr G) . i

( dom (carr G) = Seg (len (carr G)) & len G = len (carr G) )
by Def4, FINSEQ_1:def 3;yy0 . i in (carr G) . i

let i be object ; :: thesis: ( i in dom (carr G) implies yy0 . i in (carr G) . i )

assume i in dom (carr G) ; :: thesis: yy0 . i in (carr G) . i

then reconsider x = i as Element of dom (carr G) ;

reconsider x = x as Element of dom G by A15, A16, FINSEQ_3:29;

reconsider j = x as Element of NAT ;

j in dom G ;

then j in Seg I by FINSEQ_1:def 3;

then ex i0 being Element of dom G st

( i0 = j & ex seqi being sequence of (G . i0) st

( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i0 ) ) ) ) by A14;

then yy0 . x in the carrier of (G . x) ;

hence yy0 . i in (carr G) . i by Def4; :: thesis: verum

end;assume i in dom (carr G) ; :: thesis: yy0 . i in (carr G) . i

then reconsider x = i as Element of dom (carr G) ;

reconsider x = x as Element of dom G by A15, A16, FINSEQ_3:29;

reconsider j = x as Element of NAT ;

j in dom G ;

then j in Seg I by FINSEQ_1:def 3;

then ex i0 being Element of dom G st

( i0 = j & ex seqi being sequence of (G . i0) st

( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i0 ) ) ) ) by A14;

then yy0 . x in the carrier of (G . x) ;

hence yy0 . i in (carr G) . i by Def4; :: thesis: verum

then reconsider y0 = yy0 as Element of product (carr G) by A14, A17, CARD_3:9;

A18: now :: thesis: for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

reconsider x0 = y0 as Point of (product G) by A2;( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let i be Element of dom G; :: thesis: ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

reconsider j = i as Element of NAT ;

i in dom G ;

then i in Seg I by FINSEQ_1:def 3;

then consider i0 being Element of dom G such that

A19: i0 = j and

A20: ex seqi being sequence of (G . i0) st

( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A14;

consider seqi being sequence of (G . i0) such that

A21: ( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A20;

reconsider seqi = seqi as sequence of (G . i) by A19;

take seqi = seqi; :: thesis: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

thus ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) by A19, A21; :: thesis: verum

end;( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

reconsider j = i as Element of NAT ;

i in dom G ;

then i in Seg I by FINSEQ_1:def 3;

then consider i0 being Element of dom G such that

A19: i0 = j and

A20: ex seqi being sequence of (G . i0) st

( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A14;

consider seqi being sequence of (G . i0) such that

A21: ( seqi is convergent & yy0 . j = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i0 ) ) ) by A20;

reconsider seqi = seqi as sequence of (G . i) by A19;

take seqi = seqi; :: thesis: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

thus ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) by A19, A21; :: thesis: verum

x0 = y0 ;

hence seq is convergent by A18, Th13; :: thesis: verum