prvect_2.miz



    begin

    theorem :: PRVECT_2:1

    for s,t be Real_Sequence, g be Real st for n be Element of NAT holds (t . n) = |.((s . n) - g).| holds s is convergent & ( lim s) = g iff t is convergent & ( lim t) = 0

    proof

      let s,t be Real_Sequence, g be Real;

      assume

       A1: for n be Element of NAT holds (t . n) = |.((s . n) - g).|;

      hereby

        assume

         A2: s is convergent & ( lim s) = g;

         A3:

        now

          let r be Real;

          assume 0 < r;

          then

          consider n be Nat such that

           A4: for m be Nat st n <= m holds |.((s . m) - g).| < r by A2, SEQ_2:def 7;

          take n;

          now

            let m be Nat;

            

             A5: m in NAT by ORDINAL1:def 12;

            assume n <= m;

            then |. |.((s . m) - g).|.| < r by A4;

            hence |.((t . m) - 0 ).| < r by A1, A5;

          end;

          hence for m be Nat st n <= m holds |.((t . m) - 0 ).| < r;

        end;

        hence t is convergent by SEQ_2:def 6;

        hence ( lim t) = 0 by A3, SEQ_2:def 7;

      end;

      assume

       A6: t is convergent & ( lim t) = 0 ;

       A7:

      now

        let r be Real;

        assume 0 < r;

        then

        consider n be Nat such that

         A8: for m be Nat st n <= m holds |.((t . m) - 0 ).| < r by A6, SEQ_2:def 7;

        take n;

        now

          let m be Nat;

          

           A9: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then |.((t . m) - 0 ).| < r by A8;

          then |. |.((s . m) - g).|.| < r by A1, A9;

          hence |.((s . m) - g).| < r;

        end;

        hence for m be Nat st n <= m holds |.((s . m) - g).| < r;

      end;

      hence s is convergent by SEQ_2:def 6;

      hence thesis by A7, SEQ_2:def 7;

    end;

    theorem :: PRVECT_2:2

    

     Th2: for x,y be FinSequence of REAL st ( len x) = ( len y) & for i be Element of NAT st i in ( Seg ( len x)) holds 0 <= (x . i) & (x . i) <= (y . i) holds |.x.| <= |.y.|

    proof

      let x,y be FinSequence of REAL such that

       A1: ( len x) = ( len y) and

       A2: for i be Element of NAT st i in ( Seg ( len x)) holds 0 <= (x . i) & (x . i) <= (y . i);

      

       A3: for i be Nat st i in ( Seg ( len x)) holds (( sqr x) . i) <= (( sqr y) . i)

      proof

        let i be Nat;

        assume i in ( Seg ( len x));

        then

         A4: 0 <= (x . i) & (x . i) <= (y . i) by A2;

        ((x . i) ^2 ) = (( sqr x) . i) & ((y . i) ^2 ) = (( sqr y) . i) by VALUED_1: 11;

        hence thesis by A4, SQUARE_1: 15;

      end;

      ( Seg ( len ( sqr y))) = ( dom ( sqr y)) & ( dom ( sqr y)) = ( dom y) by FINSEQ_1:def 3, VALUED_1: 11;

      then

       A5: ( len ( sqr y)) = ( len y) by FINSEQ_1:def 3;

      ( Seg ( len ( sqr x))) = ( dom ( sqr x)) & ( dom ( sqr x)) = ( dom x) by FINSEQ_1:def 3, VALUED_1: 11;

      then

       A6: ( len ( sqr x)) = ( len x) by FINSEQ_1:def 3;

      

       A7: 0 <= ( Sum ( sqr x)) by RVSUM_1: 86;

      ( sqr x) is Element of (( len ( sqr x)) -tuples_on REAL ) & ( sqr y) is Element of (( len ( sqr y)) -tuples_on REAL ) by FINSEQ_2: 92;

      hence thesis by A1, A3, A6, A5, A7, RVSUM_1: 82, SQUARE_1: 26;

    end;

    theorem :: PRVECT_2:3

    

     Th3: for F be FinSequence of REAL st for i be Element of NAT st i in ( dom F) holds (F . i) = 0 holds ( Sum F) = 0

    proof

      let F be FinSequence of REAL ;

      set i = ( len F);

      set R1 = (i |-> 0 );

      reconsider R2 = F as Element of (i -tuples_on REAL ) by FINSEQ_2: 92;

      

       A1: ( Seg ( len F)) = ( dom F) by FINSEQ_1:def 3;

      assume

       A2: for i be Element of NAT st i in ( dom F) holds 0 = (F . i);

      

       A3: for j be Nat st j in ( Seg i) holds (R1 . j) = (R2 . j) by A2, A1;

      ( len R1) = i by CARD_1:def 7;

      then ( dom R1) = ( dom R2) by FINSEQ_3: 29;

      then R1 = R2 by A1, A3, FINSEQ_1: 13;

      hence thesis by RVSUM_1: 81;

    end;

    definition

      let f be Function;

      let X be set;

      :: PRVECT_2:def1

      mode MultOps of X,f -> Function means

      : Def1: ( dom it ) = ( dom f) & for i be set st i in ( dom f) holds (it . i) is Function of [:X, (f . i):], (f . i);

      existence

      proof

        deffunc F( object) = ( pr2 (X,(f . $1)));

        consider g be Function such that

         A1: ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        take g;

        thus ( dom g) = ( dom f) by A1;

        let i be set;

        assume i in ( dom f);

        then (g . i) = ( pr2 (X,(f . i))) by A1;

        hence thesis;

      end;

    end

    registration

      let F be Domain-Sequence;

      let X be set;

      cluster -> FinSequence-like for MultOps of X, F;

      coherence

      proof

        let f be MultOps of X, F;

        ( dom F) = ( dom f) & ( dom F) = ( Seg ( len F)) by Def1, FINSEQ_1:def 3;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    theorem :: PRVECT_2:4

    

     Th4: for X be set, F be Domain-Sequence, p be FinSequence holds (p is MultOps of X, F iff ( len p) = ( len F) & for i be set st i in ( dom F) holds (p . i) is Function of [:X, (F . i):], (F . i))

    proof

      let X be set;

      let F be Domain-Sequence;

      let p be FinSequence;

      ( dom p) = ( dom F) iff ( len p) = ( len F) by FINSEQ_3: 29;

      hence thesis by Def1;

    end;

    definition

      let F be Domain-Sequence;

      let X be set;

      let p be MultOps of X, F;

      let i be Element of ( dom F);

      :: original: .

      redefine

      func p . i -> Function of [:X, (F . i):], (F . i) ;

      coherence by Th4;

    end

    theorem :: PRVECT_2:5

    

     Th5: for X be non empty set, F be Domain-Sequence, f,g be Function of [:X, ( product F):], ( product F) st for x be Element of X, d be Element of ( product F), i be Element of ( dom F) holds ((f . (x,d)) . i) = ((g . (x,d)) . i) holds f = g

    proof

      let X be non empty set;

      let F be Domain-Sequence;

      let f,g be Function of [:X, ( product F):], ( product F) such that

       A1: for x be Element of X, d be Element of ( product F), i be Element of ( dom F) holds ((f . (x,d)) . i) = ((g . (x,d)) . i);

      now

        let x be Element of X, d be Element of ( product F);

        

         A2: ( dom (f . (x,d))) = ( dom F) & ( dom (g . (x,d))) = ( dom F) by CARD_3: 9;

        for v be object st v in ( dom F) holds ((f . (x,d)) . v) = ((g . (x,d)) . v) by A1;

        hence (f . (x,d)) = (g . (x,d)) by A2, FUNCT_1: 2;

      end;

      hence thesis by BINOP_1: 2;

    end;

    definition

      let F be Domain-Sequence;

      let X be non empty set;

      let p be MultOps of X, F;

      :: PRVECT_2:def2

      func [:p:] -> Function of [:X, ( product F):], ( product F) means

      : Def2: for x be Element of X, d be Element of ( product F), i be Element of ( dom F) holds ((it . (x,d)) . i) = ((p . i) . (x,(d . i)));

      existence

      proof

        defpred Q[ Element of X, Element of ( product F), Element of ( product F)] means for i be Element of ( dom F) holds ($3 . i) = ((p . i) . ($1,($2 . i)));

        

         A1: for x be Element of X, d be Element of ( product F) holds ex z be Element of ( product F) st Q[x, d, z]

        proof

          let x be Element of X, d be Element of ( product F);

          defpred P[ object, object] means ex i be Element of ( dom F) st $1 = i & $2 = ((p . i) . (x,(d . i)));

          

           A2: for w be object st w in ( dom F) holds ex z be object st P[w, z]

          proof

            let w be object;

            assume w in ( dom F);

            then

            reconsider i = w as Element of ( dom F);

            take ((p . i) . (x,(d . i)));

            thus thesis;

          end;

          consider z be Function such that

           A3: ( dom z) = ( dom F) & for w be object st w in ( dom F) holds P[w, (z . w)] from CLASSES1:sch 1( A2);

          now

            let w be object;

            assume w in ( dom F);

            then ex i be Element of ( dom F) st w = i & (z . w) = ((p . i) . (x,(d . i))) by A3;

            hence (z . w) in (F . w);

          end;

          then

          reconsider z9 = z as Element of ( product F) by A3, CARD_3: 9;

          take z9;

          let i be Element of ( dom F);

          ex j be Element of ( dom F) st j = i & (z . i) = ((p . j) . (x,(d . j))) by A3;

          hence thesis;

        end;

        thus ex P be Function of [:X, ( product F):], ( product F) st for x be Element of X, d be Element of ( product F) holds Q[x, d, (P . (x,d))] from BINOP_1:sch 3( A1);

      end;

      uniqueness

      proof

        let P,Q be Function of [:X, ( product F):], ( product F) such that

         A4: for x be Element of X, f be Element of ( product F), i be Element of ( dom F) holds ((P . (x,f)) . i) = ((p . i) . (x,(f . i))) and

         A5: for x be Element of X, f be Element of ( product F), i be Element of ( dom F) holds ((Q . (x,f)) . i) = ((p . i) . (x,(f . i)));

        now

          let x be Element of X, f be Element of ( product F);

          let i be Element of ( dom F);

          ((P . (x,f)) . i) = ((p . i) . (x,(f . i))) by A4;

          hence ((P . (x,f)) . i) = ((Q . (x,f)) . i) by A5;

        end;

        hence thesis by Th5;

      end;

    end

    definition

      let R be Relation;

      :: PRVECT_2:def3

      attr R is RealLinearSpace-yielding means

      : Def3: for S be set st S in ( rng R) holds S is RealLinearSpace;

    end

    registration

      cluster non empty RealLinearSpace-yielding for FinSequence;

      existence

      proof

        set S = the RealLinearSpace;

        take <*S*>;

        thus <*S*> is non empty;

        let x be set;

        assume that

         A1: x in ( rng <*S*>) and

         A2: not x is RealLinearSpace;

        x in {S} by A1, FINSEQ_1: 38;

        hence contradiction by A2, TARSKI:def 1;

      end;

    end

    definition

      mode RealLinearSpace-Sequence is non empty RealLinearSpace-yielding FinSequence;

    end

    definition

      let G be RealLinearSpace-Sequence;

      let j be Element of ( dom G);

      :: original: .

      redefine

      func G . j -> RealLinearSpace ;

      coherence

      proof

        (G . j) in ( rng G) by FUNCT_1:def 3;

        hence thesis by Def3;

      end;

    end

    registration

      cluster RealLinearSpace-yielding -> non-empty-addLoopStr-yielding for Relation;

      coherence

      proof

        let R be Relation;

        assume R is RealLinearSpace-yielding;

        then for x be set st x in ( rng R) holds x is non empty addLoopStr;

        hence thesis by PRVECT_1:def 9;

      end;

    end

    definition

      let G be RealLinearSpace-Sequence, j be Element of ( dom ( carr G));

      :: original: .

      redefine

      func G . j -> RealLinearSpace ;

      coherence

      proof

        ( dom G) = ( Seg ( len G)) & ( Seg ( len ( carr G))) = ( dom ( carr G)) by FINSEQ_1:def 3;

        then

        reconsider j9 = j as Element of ( dom G) by PRVECT_1:def 11;

        (G . j9) is RealLinearSpace;

        hence thesis;

      end;

    end

    definition

      ::$Canceled

      let G be RealLinearSpace-Sequence;

      :: PRVECT_2:def8

      func multop G -> MultOps of REAL , ( carr G) means

      : Def8: ( len it ) = ( len ( carr G)) & for j be Element of ( dom ( carr G)) holds (it . j) = the Mult of (G . j);

      existence

      proof

        deffunc F( Element of ( dom ( carr G))) = the Mult of (G . $1);

        consider p be non empty FinSequence such that

         A20: ( len p) = ( len ( carr G)) & for j be Element of ( dom ( carr G)) holds (p . j) = F(j) from PRVECT_1:sch 1;

        now

          let ai be set;

          assume ai in ( dom ( carr G));

          then

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

          ( len G) = ( len ( carr G)) by PRVECT_1:def 11;

          then

          reconsider j = i as Element of ( dom G) by FINSEQ_3: 29;

          (p . i) = the Mult of (G . i) & the carrier of (G . j) = (( carr G) . j) by A20, PRVECT_1:def 11;

          hence (p . ai) is Function of [: REAL , (( carr G) . ai):], (( carr G) . ai);

        end;

        then

        reconsider p9 = p as MultOps of REAL , ( carr G) by A20, Th4;

        take p9;

        thus thesis by A20;

      end;

      uniqueness

      proof

        let f,h be MultOps of REAL , ( carr G);

        assume that

         A21: ( len f) = ( len ( carr G)) and

         A22: for j be Element of ( dom ( carr G)) holds (f . j) = the Mult of (G . j) and

         A23: ( len h) = ( len ( carr G)) and

         A24: for j be Element of ( dom ( carr G)) holds (h . j) = the Mult of (G . j);

        reconsider f9 = f, h9 = h as FinSequence;

         A25:

        now

          let i be Nat;

          assume i in ( dom f9);

          then

          reconsider i9 = i as Element of ( dom ( carr G)) by A21, FINSEQ_3: 29;

          (f9 . i) = the Mult of (G . i9) by A22;

          hence (f9 . i) = (h9 . i) by A24;

        end;

        ( dom f9) = ( Seg ( len f9)) & ( dom h9) = ( Seg ( len h9)) by FINSEQ_1:def 3;

        hence thesis by A21, A23, A25, FINSEQ_1: 13;

      end;

    end

    definition

      let G be RealLinearSpace-Sequence;

      :: PRVECT_2:def9

      func product G -> strict non empty RLSStruct equals RLSStruct (# ( product ( carr G)), ( zeros G), [:( addop G):], [:( multop G):] #);

      coherence ;

    end

    

     Lm1: for LS be non empty addLoopStr st the addF of LS is commutative associative holds LS is Abelian add-associative by BINOP_1:def 2, BINOP_1:def 3;

    

     Lm2: for LS be non empty addLoopStr st the ZeroF of LS is_a_unity_wrt the addF of LS holds LS is right_zeroed by BINOP_1: 3;

    

     Lm3: for G be RealLinearSpace-Sequence holds for v1,w1 be Element of ( product ( carr G)), i be Element of ( dom ( carr G)) holds (( [:( addop G):] . (v1,w1)) . i) = (the addF of (G . i) . ((v1 . i),(w1 . i))) & for vi,wi be VECTOR of (G . i) st vi = (v1 . i) & wi = (w1 . i) holds (( [:( addop G):] . (v1,w1)) . i) = (vi + wi)

    proof

      let G be RealLinearSpace-Sequence;

      let v1,w1 be Element of ( product ( carr G));

      let i be Element of ( dom ( carr G));

      (( [:( addop G):] . (v1,w1)) . i) = ((( addop G) . i) . ((v1 . i),(w1 . i))) by PRVECT_1:def 8;

      hence thesis by PRVECT_1:def 12;

    end;

    

     Lm4: for G be RealLinearSpace-Sequence, r be Element of REAL , v be Element of ( product ( carr G)), i be Element of ( dom ( carr G)) holds (( [:( multop G):] . (r,v)) . i) = (the Mult of (G . i) . (r,(v . i))) & for vi be VECTOR of (G . i) st vi = (v . i) holds (( [:( multop G):] . (r,v)) . i) = (r * vi)

    proof

      let G be RealLinearSpace-Sequence;

      let r be Element of REAL , v be Element of ( product ( carr G));

      let i be Element of ( dom ( carr G));

      (( [:( multop G):] . (r,v)) . i) = ((( multop G) . i) . (r,(v . i))) by Def2;

      hence thesis by Def8;

    end;

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

    

     Lm5: for G be RealLinearSpace-Sequence holds ( product G) is vector-distributive scalar-distributive scalar-associative scalar-unital

    proof

      deffunc ad( addLoopStr) = the addF of $1;

      let G be RealLinearSpace-Sequence;

      reconsider GS = RLSStruct (# ( product ( carr G)), ( zeros G), [:( addop G):], [:( multop G):] #) as non empty RLSStruct;

      ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      then ( dom G) = ( Seg ( len ( carr G))) by PRVECT_1:def 11;

      then

       A1: ( dom G) = ( dom ( carr G)) by FINSEQ_1:def 3;

      now

        let a1,b1 be Real;

        reconsider a = a1, b = b1 as Element of REAL by XREAL_0:def 1;

        let v,w be VECTOR of GS;

        reconsider v1 = v, w1 = w as Element of ( product ( carr G));

         A2:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

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

          reconsider vi = (v1 . i) as VECTOR of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . (jj,v1)) . x) = (1 * vi) by Lm4;

          hence (( [:( multop G):] . (jj,v1)) . x) = (v1 . x) by RLVECT_1:def 8;

        end;

         A3:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

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

          reconsider vi = (v1 . i) as VECTOR of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . ((a + b),v1)) . i) = ((a + b) * vi) by Lm4

          .= ((a * vi) + (b * vi)) by RLVECT_1:def 6

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(b * vi))) by Lm4

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(( [:( multop G):] . (b,v1)) . i))) by Lm4;

          hence (( [:( multop G):] . ((a + b),v1)) . x) = (( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (b,v1)))) . x) by Lm3;

        end;

         A4:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

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

          reconsider vi = (v1 . i), wi = (w1 . i) as VECTOR of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . (a,( [:( addop G):] . (v1,w1)))) . i) = (the Mult of (G . i) . (a,(( [:( addop G):] . (v1,w1)) . i))) by Lm4

          .= (a * (vi + wi)) by Lm3

          .= ((a * vi) + (a * wi)) by RLVECT_1:def 5

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(a * wi))) by Lm4

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(( [:( multop G):] . (a,w1)) . i))) by Lm4;

          hence (( [:( multop G):] . (a,( [:( addop G):] . (v1,w1)))) . x) = (( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (a,w1)))) . x) by Lm3;

        end;

        ( dom ( [:( multop G):] . (a,( [:( addop G):] . (v1,w1))))) = ( dom ( carr G)) & ( dom ( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (a,w1))))) = ( dom ( carr G)) by CARD_3: 9;

        hence (a1 * (v + w)) = ((a1 * v) + (a1 * w)) by A4, FUNCT_1: 2;

         A5:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

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

          reconsider vi = (v1 . i) as VECTOR of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . ((a * b),v1)) . i) = ((a * b) * vi) by Lm4

          .= (a * (b * vi)) by RLVECT_1:def 7

          .= (the Mult of (G . i) . (a,(( [:( multop G):] . (b,v1)) . i))) by Lm4;

          hence (( [:( multop G):] . ((a * b),v1)) . x) = (( [:( multop G):] . (a,( [:( multop G):] . (b,v1)))) . x) by Lm4;

        end;

        ( dom ( [:( multop G):] . ((a + b),v1))) = ( dom ( carr G)) & ( dom ( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (b,v1))))) = ( dom ( carr G)) by CARD_3: 9;

        hence ((a1 + b1) * v) = ((a1 * v) + (b1 * v)) by A3, FUNCT_1: 2;

        ( dom ( [:( multop G):] . ((a * b),v1))) = ( dom ( carr G)) & ( dom ( [:( multop G):] . (a,( [:( multop G):] . (b,v1))))) = ( dom ( carr G)) by CARD_3: 9;

        hence ((a1 * b1) * v) = (a1 * (b1 * v)) by A5, FUNCT_1: 2;

        ( dom ( [:( multop G):] . (jj,v1))) = ( dom ( carr G)) & ( dom v1) = ( dom ( carr G)) by CARD_3: 9;

        hence (1 * v) = v by A2, FUNCT_1: 2;

      end;

      hence thesis;

    end;

    registration

      let G be RealLinearSpace-Sequence;

      cluster ( product G) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        deffunc zr( addLoopStr) = the ZeroF of $1;

        reconsider GS = RLSStruct (# ( product ( carr G)), ( zeros G), [:( addop G):], [:( multop G):] #) as non empty RLSStruct;

        deffunc car( 1-sorted) = the carrier of $1;

        deffunc ad( addLoopStr) = the addF of $1;

         A1:

        now

          let i be Element of ( dom ( carr G));

          ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3

          .= ( Seg ( len ( carr G))) by PRVECT_1:def 11

          .= ( dom ( carr G)) by FINSEQ_1:def 3;

          hence (( carr G) . i) = car(.) by PRVECT_1:def 11;

        end;

        now

          let i be Element of ( dom ( carr G));

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, PRVECT_1:def 12;

          hence (( addop G) . i) is associative by FVSUM_1: 2;

        end;

        then

         A2: [:( addop G):] is associative by PRVECT_1: 18;

        now

          let i be Element of ( dom ( carr G));

          

           A3: (( zeros G) . i) = ( 0. (G . i)) by PRVECT_1:def 14;

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, PRVECT_1:def 12;

          hence (( zeros G) . i) is_a_unity_wrt (( addop G) . i) by A3, PRVECT_1: 1;

        end;

        then

         A4: ( zeros G) is_a_unity_wrt [:( addop G):] by PRVECT_1: 19;

        

         A5: GS is right_complementable

        proof

          let x be Element of GS;

          reconsider y = (( Frege ( complop G)) . x) as Element of GS by FUNCT_2: 5;

          take y;

          now

            let i be Element of ( dom ( carr G));

            ( 0. (G . i)) = zr(.);

            then

             A6: zr(.) is_a_unity_wrt ad(.) by PRVECT_1: 1;

            

             A7: (( complop G) . i) = ( comp (G . i)) by PRVECT_1:def 13;

            (( carr G) . i) = car(.) & (( addop G) . i) = ad(.) by A1, PRVECT_1:def 12;

            hence (( complop G) . i) is_an_inverseOp_wrt (( addop G) . i) & (( addop G) . i) is having_a_unity by A6, A7, PRVECT_1: 2, SETWISEO:def 2;

          end;

          then ( Frege ( complop G)) is_an_inverseOp_wrt [:( addop G):] by PRVECT_1: 20;

          then ( [:( addop G):] . (x,y)) = ( the_unity_wrt [:( addop G):]) by FINSEQOP:def 1;

          hence thesis by A4, BINOP_1:def 8;

        end;

        now

          let i be Element of ( dom ( carr G));

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, PRVECT_1:def 12;

          hence (( addop G) . i) is commutative by FVSUM_1: 1;

        end;

        then [:( addop G):] is commutative by PRVECT_1: 17;

        hence thesis by A2, A4, A5, Lm1, Lm2, Lm5;

      end;

    end

    begin

    definition

      let R be Relation;

      :: PRVECT_2:def10

      attr R is RealNormSpace-yielding means

      : Def10: for x be set st x in ( rng R) holds x is RealNormSpace;

    end

    registration

      cluster non empty RealNormSpace-yielding for FinSequence;

      existence

      proof

        set A = the RealNormSpace;

        take <*A*>;

        thus <*A*> is non empty;

        let x be set;

        assume that

         A1: x in ( rng <*A*>) and

         A2: not x is RealNormSpace;

        x in {A} by A1, FINSEQ_1: 38;

        hence contradiction by A2, TARSKI:def 1;

      end;

    end

    definition

      mode RealNormSpace-Sequence is non empty RealNormSpace-yielding FinSequence;

    end

    definition

      let G be RealNormSpace-Sequence;

      let j be Element of ( dom G);

      :: original: .

      redefine

      func G . j -> RealNormSpace ;

      coherence

      proof

        (G . j) in ( rng G) by FUNCT_1:def 3;

        hence thesis by Def10;

      end;

    end

    registration

      cluster RealNormSpace-yielding -> RealLinearSpace-yielding for FinSequence;

      coherence ;

    end

    definition

      let G be RealNormSpace-Sequence;

      let x be Element of ( product ( carr G));

      :: PRVECT_2:def11

      func normsequence (G,x) -> Element of ( REAL ( len G)) means

      : Def11: ( len it ) = ( len G) & for j be Element of ( dom G) holds (it . j) = (the normF of (G . j) . (x . j));

      existence

      proof

        deffunc F( Element of ( dom G)) = ( In ((the normF of (G . $1) . (x . $1)), REAL ));

        consider f be Function of ( dom G), REAL such that

         A1: for j be Element of ( dom G) holds (f . j) = F(j) from FUNCT_2:sch 4;

        

         A2: ( rng f) c= REAL ;

        ( dom f) = ( dom G) by FUNCT_2:def 1;

        then

         A3: ( dom f) = ( Seg ( len G)) by FINSEQ_1:def 3;

        then f is FinSequence by FINSEQ_1:def 2;

        then

        reconsider f as FinSequence of REAL by A2, FINSEQ_1:def 4;

        

         A4: f in ( REAL * ) by FINSEQ_1:def 11;

        ( len f) = ( len G) by A3, FINSEQ_1:def 3;

        then f in (( len G) -tuples_on REAL ) by A4;

        then

        reconsider f as Element of ( REAL ( len G));

        take f;

        thus ( len f) = ( len G) by CARD_1:def 7;

        let j be Element of ( dom G);

        (f . j) = F(j) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Element of ( REAL ( len G));

        assume that ( len f) = ( len G) and

         A5: for j be Element of ( dom G) holds (f . j) = (the normF of (G . j) . (x . j)) and ( len g) = ( len G) and

         A6: for j be Element of ( dom G) holds (g . j) = (the normF of (G . j) . (x . j));

        now

          let j be Nat;

          assume j in ( Seg ( len G));

          then

          reconsider j1 = j as Element of ( dom G) by FINSEQ_1:def 3;

          (f . j) = (the normF of (G . j1) . (x . j1)) by A5;

          hence (f . j) = (g . j) by A6;

        end;

        hence thesis by FINSEQ_2: 119;

      end;

    end

    definition

      let G be RealNormSpace-Sequence;

      :: PRVECT_2:def12

      func productnorm G -> Function of ( product ( carr G qua RealLinearSpace-Sequence)), REAL means

      : Def12: for x be Element of ( product ( carr G)) holds (it . x) = |.( normsequence (G,x)).|;

      existence

      proof

        deffunc F( Element of ( product ( carr G))) = ( In ( |.( normsequence (G,$1)).|, REAL ));

        consider f be Function of ( product ( carr G)), REAL such that

         A1: for x be Element of ( product ( carr G)) holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let x be Element of ( product ( carr G));

        (f . x) = F(x) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of ( product ( carr G)), REAL ;

        assume that

         A2: for x be Element of ( product ( carr G)) holds (f . x) = |.( normsequence (G,x)).| and

         A3: for x be Element of ( product ( carr G)) holds (g . x) = |.( normsequence (G,x)).|;

        now

          let x be Element of ( product ( carr G));

          (f . x) = |.( normsequence (G,x)).| by A2;

          hence (f . x) = (g . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let G be RealNormSpace-Sequence;

      :: PRVECT_2:def13

      func product G -> strict non empty NORMSTR means

      : Def13: the RLSStruct of it = ( product G qua RealLinearSpace-Sequence) & the normF of it = ( productnorm G);

      existence

      proof

        reconsider G0 = NORMSTR (# ( product ( carr G)), ( zeros G), [:( addop G):], [:( multop G):], ( productnorm G) #) as strict non empty NORMSTR;

        take G0;

        thus thesis;

      end;

      uniqueness ;

    end

    reserve G for RealNormSpace-Sequence;

    theorem :: PRVECT_2:6

    

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

    proof

       the RLSStruct of ( product G) = ( product G qua RealLinearSpace-Sequence) by Def13;

      hence thesis by Def13;

    end;

    theorem :: PRVECT_2:7

    

     Th7: for x be VECTOR of ( product G), y be Element of ( product ( carr G)) st x = y holds ||.x.|| = |.( normsequence (G,y)).|

    proof

      let x be VECTOR of ( product G);

      let y be Element of ( product ( carr G));

      assume

       A1: x = y;

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

      hence thesis by A1, Def12;

    end;

    theorem :: PRVECT_2:8

    

     Th8: for x,y,z be Element of ( product ( carr G)), i be Nat st i in ( dom x) & z = ( [:( addop G):] . (x,y)) holds (( normsequence (G,z)) . i) <= ((( normsequence (G,x)) + ( normsequence (G,y))) . i)

    proof

      let x,y,z be Element of ( product ( carr G)), i be Nat such that

       A1: i in ( dom x) and

       A2: z = ( [:( addop G):] . (x,y));

      reconsider i0 = i as Element of ( dom ( carr G)) by A1, CARD_3: 9;

      

       A3: (z . i0) = ((( addop G) . i0) . ((x . i0),(y . i0))) by A2, PRVECT_1:def 8;

      ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3

      .= ( Seg ( len ( carr G))) by PRVECT_1:def 11

      .= ( dom ( carr G)) by FINSEQ_1:def 3;

      then

      reconsider i0 = i as Element of ( dom G) by A1, CARD_3: 9;

      ( dom x) = ( dom ( carr G)) & (( carr G) . i0) = the carrier of (G . i0) by PRVECT_1:def 11, CARD_3: 9;

      then

      reconsider xi0 = (x . i0), yi0 = (y . i0), zi0 = (z . i0) as Element of (G . i0) by A1, CARD_3: 9;

       ||.zi0.|| = ||.(xi0 + yi0).|| by A3, PRVECT_1:def 12;

      then

       A4: ||.zi0.|| <= ( ||.xi0.|| + ||.yi0.||) by NORMSP_1:def 1;

      

       A5: ((( normsequence (G,x)) . i0) + (( normsequence (G,y)) . i0)) = ((( normsequence (G,x)) + ( normsequence (G,y))) . i0) by RVSUM_1: 11;

      (the normF of (G . i0) . yi0) = (( normsequence (G,y)) . i0) & (the normF of (G . i0) . zi0) = (( normsequence (G,z)) . i0) by Def11;

      hence thesis by A4, A5, Def11;

    end;

    theorem :: PRVECT_2:9

    

     Th9: for x be Element of ( product ( carr G)), i be Nat st i in ( dom x) holds 0 <= (( normsequence (G,x)) . i)

    proof

      let x be Element of ( product ( carr G)), i be Nat such that

       A1: i in ( dom x);

      ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3

      .= ( Seg ( len ( carr G))) by PRVECT_1:def 11

      .= ( dom ( carr G)) by FINSEQ_1:def 3;

      then

      reconsider i0 = i as Element of ( dom G) by A1, CARD_3: 9;

      ( dom x) = ( dom ( carr G)) & (( carr G) . i0) = the carrier of (G . i0) by PRVECT_1:def 11, CARD_3: 9;

      then

      reconsider xi0 = (x . i0) as Element of (G . i0) by A1, CARD_3: 9;

       0 <= ||.xi0.|| by NORMSP_1: 4;

      hence thesis by Def11;

    end;

    

     Lm6: ( product G) is reflexive discerning RealNormSpace-like

    proof

      

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

      

       A2: ( len G) = ( len ( carr G)) by PRVECT_1:def 11;

      reconsider n = ( len G) as Element of NAT ;

      thus ( product G) is reflexive

      proof

        reconsider z = ( 0. ( product G)) as Element of ( product ( carr G)) by A1;

        

         A3: for i be Element of ( dom ( carr G)) holds (( normsequence (G,z)) . i) = 0

        proof

          let i be Element of ( dom ( carr G));

          reconsider i0 = i as Element of ( dom G) by A2, FINSEQ_3: 29;

          (( carr G) . i0) = the carrier of (G . i0) by PRVECT_1:def 11;

          then

          reconsider zi0 = (z . i0) as Element of (G . i0) by CARD_3: 9;

          (z . i) = ( 0. (G . i)) by A1, PRVECT_1:def 14;

          then ||.zi0.|| = 0 ;

          hence thesis by Def11;

        end;

        for i be Element of NAT st i in ( dom ( sqr ( normsequence (G,z)))) holds (( sqr ( normsequence (G,z))) . i) = 0

        proof

          let i be Element of NAT ;

          assume

           A4: i in ( dom ( sqr ( normsequence (G,z))));

          ( len ( normsequence (G,z))) = ( len G) by Def11;

          then

           A5: ( dom ( normsequence (G,z))) = ( dom G) by FINSEQ_3: 29;

          ( dom ( carr G)) = ( dom G) by A2, FINSEQ_3: 29;

          then ( dom ( sqr ( normsequence (G,z)))) = ( dom ( carr G)) by A5, VALUED_1: 11;

          then ((( normsequence (G,z)) . i) ^2 ) = ( 0 ^2 ) by A3, A4;

          hence thesis by VALUED_1: 11;

        end;

        then |.( normsequence (G,z)).| = 0 by Th3, SQUARE_1: 17;

        hence ||.( 0. ( product G)).|| = 0 by Th7;

      end;

      thus ( product G) is discerning

      proof

        let x be Point of ( product G);

        reconsider z = x as Element of ( product ( carr G)) by A1;

        assume

         A6: ||.x.|| = 0 ;

        now

          let i be Element of ( dom ( carr G));

          reconsider i0 = i as Element of ( dom G) by A2, FINSEQ_3: 29;

          (( carr G) . i0) = the carrier of (G . i0) by PRVECT_1:def 11;

          then

          reconsider zzi0 = (z . i0) as Element of (G . i0) by CARD_3: 9;

           ||.x.|| = |.( normsequence (G,z)).| by Th7;

          then ( normsequence (G,z)) = ( 0* n) by A6, EUCLID: 8;

          then (( normsequence (G,z)) . i) = 0 ;

          then ||.zzi0.|| = 0 by Def11;

          hence (z . i) = ( 0. (G . i)) by NORMSP_0:def 5;

        end;

        hence thesis by A1, PRVECT_1:def 14;

      end;

      let x,y be Point of ( product G), a be Real;

      reconsider z = x as Element of ( product ( carr G)) by A1;

      reconsider xx = x, yy = y as Element of ( product ( carr G)) by A1;

      reconsider ax = (a * x) as Element of ( product ( carr G)) by A1;

      

       A7: ||.y.|| = |.( normsequence (G,yy)).| & |.(( normsequence (G,xx)) + ( normsequence (G,yy))).| <= ( |.( normsequence (G,xx)).| + |.( normsequence (G,yy)).|) by Th7, EUCLID: 12;

      

       A8: ( len ( normsequence (G,ax))) = n by CARD_1:def 7;

      then

       A9: ( dom ( normsequence (G,ax))) = ( Seg n) by FINSEQ_1:def 3;

      

       A10: for i be Nat st i in ( dom ( normsequence (G,ax))) holds (( normsequence (G,ax)) . i) = (( |.a.| * ( normsequence (G,z))) . i)

      proof

        let i be Nat;

        assume i in ( dom ( normsequence (G,ax)));

        then

        reconsider i0 = i as Element of ( dom G) by A9, FINSEQ_1:def 3;

        reconsider i1 = i0 as Element of ( dom ( carr G)) by A2, FINSEQ_3: 29;

        (( carr G) . i0) = the carrier of (G . i0) & ( dom ( carr G)) = ( dom G) by A2, PRVECT_1:def 11, FINSEQ_3: 29;

        then

        reconsider axi0 = (ax . i0), zi0 = (z . i0) as Element of (G . i0) by CARD_3: 9;

        reconsider aa = a as Element of REAL by XREAL_0:def 1;

        (( [:( multop G):] . (aa,z)) . i1) = ((( multop G) . i1) . (a,zi0)) by Def2;

        then axi0 = (a * zi0) by A1, Def8;

        then ||.axi0.|| = ( |.a.| * ||.zi0.||) by NORMSP_1:def 1;

        then ||.axi0.|| = ( |.a.| * (( normsequence (G,z)) . i0)) by Def11;

        then ||.axi0.|| = (( |.a.| * ( normsequence (G,z))) . i0) by RVSUM_1: 44;

        hence thesis by Def11;

      end;

      ( len ( |.a.| * ( normsequence (G,z)))) = n by CARD_1:def 7;

      then |.( normsequence (G,ax)).| = |.( |.a.| * ( normsequence (G,z))).| by A8, A10, FINSEQ_2: 9;

      then

       A11: |.( normsequence (G,ax)).| = ( |. |.a.|.| * |.( normsequence (G,z)).|) by EUCLID: 11;

      reconsider z = (x + y) as Element of ( product ( carr G)) by A1;

      

       A12: for i be Element of NAT st i in ( Seg n) holds 0 <= (( normsequence (G,z)) . i) & (( normsequence (G,z)) . i) <= ((( normsequence (G,xx)) + ( normsequence (G,yy))) . i)

      proof

        

         A13: ( dom xx) = ( dom ( carr G)) by CARD_3: 9;

        

         A14: ( Seg n) = ( dom G) & ( dom ( carr G)) = ( dom G) by A2, FINSEQ_1:def 3, FINSEQ_3: 29;

        let i be Element of NAT such that

         A15: i in ( Seg n);

        i in ( dom z) by A15, A14, CARD_3: 9;

        hence thesis by A1, A15, A14, A13, Th8, Th9;

      end;

      

       A16: ( len ( normsequence (G,z))) = n by Def11;

      then ( len ( normsequence (G,z))) = ( len (( normsequence (G,xx)) + ( normsequence (G,yy)))) by CARD_1:def 7;

      then

       A17: |.( normsequence (G,z)).| <= |.(( normsequence (G,xx)) + ( normsequence (G,yy))).| by A16, A12, Th2;

       ||.(x + y).|| = |.( normsequence (G,z)).| & ||.x.|| = |.( normsequence (G,xx)).| by Th7;

      hence thesis by A11, A17, A7, Th7, XXREAL_0: 2;

    end;

    registration

      let G be RealNormSpace-Sequence;

      cluster ( product G) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence

      proof

        reconsider G1 = G as RealLinearSpace-Sequence;

        

         A1: the RLSStruct of ( product G) = ( product G qua RealLinearSpace-Sequence) by Def13;

         A2:

        now

          let v be VECTOR of ( product G);

          reconsider v1 = v as VECTOR of ( product G1) by A1;

          (1 * v) = (1 * v1) by A1;

          hence (1 * v) = v by RLVECT_1:def 8;

        end;

        

         A3: ( product G) is right_complementable

        proof

          let v be VECTOR of ( product G);

          reconsider v1 = v as VECTOR of ( product G1) by A1;

          reconsider w = ( - v1) as VECTOR of ( product G) by A1;

          take w;

          (v + w) = (v1 - v1) by A1;

          then (v + w) = ( 0. ( product G1)) by RLVECT_1: 15;

          hence thesis by A1;

        end;

         A4:

        now

          let a be Real;

          let v,w be VECTOR of ( product G);

          reconsider v1 = v, w1 = w as VECTOR of ( product G1) by A1;

          (a * (v + w)) = (a * (v1 + w1)) by A1;

          then (a * (v + w)) = ((a * v1) + (a * w1)) by RLVECT_1:def 5;

          hence (a * (v + w)) = ((a * v) + (a * w)) by A1;

        end;

         A5:

        now

          let a,b be Real, v be VECTOR of ( product G);

          reconsider v1 = v as VECTOR of ( product G1) by A1;

          ((a * b) * v) = ((a * b) * v1) by A1;

          then ((a * b) * v) = (a * (b * v1)) by RLVECT_1:def 7;

          hence ((a * b) * v) = (a * (b * v)) by A1;

        end;

         A6:

        now

          let a,b be Real, v be VECTOR of ( product G);

          reconsider v1 = v as VECTOR of ( product G1) by A1;

          ((a + b) * v) = ((a + b) * v1) by A1;

          then ((a + b) * v) = ((a * v1) + (b * v1)) by RLVECT_1:def 6;

          hence ((a + b) * v) = ((a * v) + (b * v)) by A1;

        end;

        

         A7: ( product G) is add-associative

        proof

          let v,w,x be VECTOR of ( product G);

          reconsider v1 = v, w1 = w, x1 = x as VECTOR of ( product G1) by A1;

          ((v + w) + x) = ((v1 + w1) + x1) by A1;

          then ((v + w) + x) = (v1 + (w1 + x1)) by RLVECT_1:def 3;

          hence thesis by A1;

        end;

        

         A8: ( product G) is Abelian

        proof

          let v,w be VECTOR of ( product G);

          reconsider v1 = v, w1 = w as VECTOR of ( product G1) by A1;

          (v + w) = (v1 + w1) by A1;

          then (v + w) = (w1 + v1);

          hence thesis by A1;

        end;

        ( product G) is right_zeroed

        proof

          let v be VECTOR of ( product G);

          reconsider v1 = v as VECTOR of ( product G1) by A1;

          (v + ( 0. ( product G))) = (v1 + ( 0. ( product G1))) by A1;

          hence thesis;

        end;

        hence thesis by A8, A7, A3, A4, A6, A5, A2, Lm6;

      end;

    end

    theorem :: PRVECT_2:10

    

     Th10: for G be RealNormSpace-Sequence, i be Element of ( dom G), x be Point of ( product G), y be Element of ( product ( carr G)), xi be Point of (G . i) st y = x & xi = (y . i) holds ||.xi.|| <= ||.x.||

    proof

      let G be RealNormSpace-Sequence, i be Element of ( dom G), x be Point of ( product G), y be Element of ( product ( carr G)), xi be Point of (G . i);

      reconsider n = ( len G) as Element of NAT ;

      assume that

       A1: y = x and

       A2: xi = (y . i);

      

       A3: ((( normsequence (G,y)) . i) ^2 ) = (( sqr ( normsequence (G,y))) . i) by VALUED_1: 11;

      

       A4: for i be Nat st i in ( Seg n) holds 0 <= (( sqr ( normsequence (G,y))) . i)

      proof

        let i be Nat such that i in ( Seg n);

        ((( normsequence (G,y)) . i) ^2 ) >= 0 by XREAL_1: 63;

        hence thesis by VALUED_1: 11;

      end;

      ( dom G) = ( Seg n) by FINSEQ_1:def 3;

      then

       A5: 0 <= ((( normsequence (G,y)) . i) ^2 ) & (( sqr ( normsequence (G,y))) . i) <= ( Sum ( sqr ( normsequence (G,y)))) by A4, REAL_NS1: 7, XREAL_1: 63;

       ||.xi.|| = (( normsequence (G,y)) . i) by A2, Def11;

      then ( sqrt (( sqr ( normsequence (G,y))) . i)) = (( normsequence (G,y)) . i) by A3, NORMSP_1: 4, SQUARE_1: 22;

      then

       A6: ||.xi.|| = ( sqrt (( sqr ( normsequence (G,y))) . i)) by A2, Def11;

       ||.x.|| = |.( normsequence (G,y)).| by A1, Th7;

      hence thesis by A3, A5, A6, SQUARE_1: 26;

    end;

    

     Lm7: for RNS be RealNormSpace, S be sequence of RNS, g be Point of RNS holds S is convergent & ( lim S) = g iff ||.(S - g).|| is convergent & ( lim ||.(S - g).||) = 0

    proof

      let RNS be RealNormSpace, S be sequence of RNS, g be Point of RNS;

      now

        assume

         A1: ||.(S - g).|| is convergent & ( lim ||.(S - g).||) = 0 ;

         A2:

        now

          let r be Real;

          reconsider p = r as Real;

          assume 0 < r;

          then

          consider n be Nat such that

           A3: for m be Nat st n <= m holds |.(( ||.(S - g).|| . m) - 0 ).| < p by A1, SEQ_2:def 7;

          reconsider n as Nat;

          take n;

          let m be Nat;

          assume n <= m;

          then |.(( ||.(S - g).|| . m) - 0 ).| < p by A3;

          then |. ||.((S - g) . m).||.| < p by NORMSP_0:def 4;

          then |. ||.((S . m) - g).||.| < p by NORMSP_1:def 4;

          hence ||.((S . m) - g).|| < r by ABSVALUE:def 1, NORMSP_1: 4;

        end;

        hence S is convergent;

        hence ( lim S) = g by A2, NORMSP_1:def 7;

      end;

      hence thesis by NORMSP_1: 24;

    end;

    theorem :: PRVECT_2:11

    

     Th11: for G be RealNormSpace-Sequence, i be Element of ( dom G), x,y be Point of ( product G), xi,yi be Point of (G . i), zx,zy be Element of ( product ( carr G)) st xi = (zx . i) & zx = x & yi = (zy . i) & zy = y holds ||.(yi - xi).|| <= ||.(y - x).||

    proof

      let G be RealNormSpace-Sequence, i be Element of ( dom G), x,y be Point of ( product G), xi,yi be Point of (G . i), zx,zy be Element of ( product ( carr G));

      assume that

       A1: xi = (zx . i) and

       A2: zx = x and

       A3: yi = (zy . i) and

       A4: zy = y;

      reconsider zyi = (zy . i), zxi = (zx . i) as Element of (G . i) by A1, A3;

      

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

      then

      reconsider mzx = ( - x) as Element of ( product ( carr G));

      ( len G) = ( len ( carr G)) by PRVECT_1:def 11;

      then

       A6: ( dom G) = ( dom ( carr G)) by FINSEQ_3: 29;

      ( - x) = (( - 1) * x) by RLVECT_1: 16;

      then

       A7: (mzx . i) = (( - jj) * zxi) by A2, A5, A6, Lm4;

      then

      reconsider mzxi = (mzx . i) as Element of (G . i);

      reconsider zyMm = (y - x) as Element of ( product ( carr G)) by A5;

      (zyMm . i) = (zyi + mzxi) by A4, A5, A6, Lm3;

      then (zyMm . i) = (zyi + ( - zxi)) by A7, RLVECT_1: 16;

      hence thesis by A1, A3, Th10;

    end;

    theorem :: PRVECT_2:12

    for G be RealNormSpace-Sequence, seq be sequence of ( product G), x0 be Point of ( product G), y0 be Element of ( product ( carr G)) st x0 = y0 & seq is convergent & ( lim seq) = x0 holds for i be Element of ( dom G) holds ex seqi be sequence of (G . i) st seqi is convergent & (y0 . i) = ( lim seqi) & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i)

    proof

      let G be RealNormSpace-Sequence, seq be sequence of ( product G), x0 be Point of ( product G), y0 be Element of ( product ( carr G));

      assume that

       A1: x0 = y0 and

       A2: seq is convergent & ( lim seq) = x0;

      let i be Element of ( dom G);

      defpred P1[ Nat, Element of (G . i)] means ex seqm be Element of ( product ( carr G)) st seqm = (seq . $1) & $2 = (seqm . i);

      ( len G) = ( len ( carr G)) by PRVECT_1:def 11;

      then

       A3: ( dom G) = ( dom ( carr G)) by FINSEQ_3: 29;

      then (y0 . i) in (( carr G) . i) by CARD_3: 9;

      then

      reconsider x0i = (y0 . i) as Point of (G . i) by PRVECT_1:def 11;

      

       A4: for x be Element of NAT holds ex y be Element of (G . i) st P1[x, y]

      proof

        let x be Element of NAT ;

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

        then

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

         A5: seqm = (seq . x);

        take (seqm . i);

        (( carr G) . i) = the carrier of (G . i) by PRVECT_1:def 11;

        hence thesis by A3, A5, CARD_3: 9;

      end;

      consider f be sequence of the carrier of (G . i) such that

       A6: for x be Element of NAT holds P1[x, (f . x)] from FUNCT_2:sch 3( A4);

      for x be Nat holds P1[x, (f . x)]

      proof

        let x be Nat;

        x in NAT by ORDINAL1:def 12;

        hence thesis by A6;

      end;

      then

      consider seqi be sequence of (G . i) such that

       A7: for m be Nat holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i);

      take seqi;

      

       A8: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((seqi . n) - x0i).|| < r

      proof

        let r be Real;

        assume r > 0 ;

        then

        consider k be Nat such that

         A9: for n be Nat st k <= n holds ||.((seq . n) - x0).|| < r by A2, NORMSP_1:def 7;

        take k;

        let n be Nat;

        assume n >= k;

        then

         A10: ||.((seq . n) - x0).|| < r by A9;

        ex seqn be Element of ( product ( carr G)) st seqn = (seq . n) & (seqi . n) = (seqn . i) by A7;

        then ||.((seqi . n) - x0i).|| <= ||.((seq . n) - x0).|| by A1, Th11;

        hence ||.((seqi . n) - x0i).|| < r by A10, XXREAL_0: 2;

      end;

      then seqi is convergent;

      hence thesis by A7, A8, NORMSP_1:def 7;

    end;

    theorem :: PRVECT_2:13

    

     Th13: for G be RealNormSpace-Sequence, seq be sequence of ( product G), x0 be Point of ( product G), y0 be Element of ( product ( carr G)) st x0 = y0 & for i be Element of ( dom G) holds ex seqi be sequence of (G . i) st seqi is convergent & (y0 . i) = ( lim seqi) & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i) holds seq is convergent & ( lim seq) = x0

    proof

      let G be RealNormSpace-Sequence, seq be sequence of ( product G), x0 be Point of ( product G), y0 be Element of ( product ( carr G));

      assume that

       A1: x0 = y0 and

       A2: for i be Element of ( dom G) holds ex seqi be sequence of (G . i) st seqi is convergent & (y0 . i) = ( lim seqi) & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i);

      defpred PP[ Element of ( dom G), set] means ex rseqi be Real_Sequence, seqi be sequence of (G . $1) st rseqi = $2 & seqi is convergent & rseqi is convergent & ( lim rseqi) = 0 & rseqi = ||.(seqi - ( lim seqi)).|| & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . $1);

      

       A3: for i be Element of ( dom G) holds ex yyseqi be Element of ( Funcs ( NAT , REAL )) st PP[i, yyseqi]

      proof

        let i be Element of ( dom G);

        consider seqi be sequence of (G . i) such that

         A4: seqi is convergent and (y0 . i) = ( lim seqi) and

         A5: for m be Element of NAT holds ex Sm be Element of ( product ( carr G)) st Sm = (seq . m) & (seqi . m) = (Sm . i) by A2;

        set rseqi = ||.(seqi - ( lim seqi)).||;

        

         A6: rseqi is Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

        rseqi is convergent & ( lim rseqi) = 0 by A4, Lm7;

        hence thesis by A4, A5, A6;

      end;

      consider yyseq be Function of ( dom G), ( Funcs ( NAT , REAL )) such that

       A7: for i be Element of ( dom G) holds PP[i, (yyseq . i)] from FUNCT_2:sch 3( A3);

      reconsider I = ( len G) as Element of NAT ;

      defpred PQ[ Element of NAT , Element of ( REAL I)] means for i be Element of ( dom G) holds ((yyseq . i) . $1) = ($2 . i);

      

       A8: for k be Element of NAT holds ex yseqk be Element of ( REAL I) st PQ[k, yseqk]

      proof

        let k be Element of NAT ;

        defpred PPF[ set, object] means ex i be Element of ( dom G) st i = $1 & $2 = ((yyseq . i) . k);

        

         A9: for k be Nat st k in ( Seg I) holds ex x be object st PPF[k, x]

        proof

          let j be Nat;

          assume j in ( Seg I);

          then

          reconsider i = j as Element of ( dom G) by FINSEQ_1:def 3;

          take ((yyseq . i) . k);

          thus thesis;

        end;

        consider yseqk be FinSequence such that

         A10: ( dom yseqk) = ( Seg I) & for j be Nat st j in ( Seg I) holds PPF[j, (yseqk . j)] from FINSEQ_1:sch 1( A9);

        now

          let j be Nat;

          assume j in ( dom yseqk);

          then

          consider i be Element of ( dom G) such that i = j and

           A11: (yseqk . j) = ((yyseq . i) . k) by A10;

          (yyseq . i) is sequence of REAL by FUNCT_2: 66;

          hence (yseqk . j) in REAL by A11, FUNCT_2: 5;

        end;

        then

        reconsider yyy = yseqk as FinSequence of REAL by FINSEQ_2: 12;

        yyy is Element of (( len yyy) -tuples_on REAL ) by FINSEQ_2: 92;

        then

        reconsider yseqk as Element of ( REAL I) by A10, FINSEQ_1:def 3;

        now

          let j be Element of ( dom G);

          j in ( dom G);

          then j in ( Seg I) by FINSEQ_1:def 3;

          then ex i be Element of ( dom G) st i = j & (yseqk . j) = ((yyseq . i) . k) by A10;

          hence (yseqk . j) = ((yyseq . j) . k);

        end;

        hence thesis;

      end;

      consider yseq be sequence of ( REAL I) such that

       A12: for k be Element of NAT holds PQ[k, (yseq . k)] from FUNCT_2:sch 3( A8);

       A13:

      now

        let i0 be Element of NAT ;

        assume i0 in ( Seg I);

        then

        reconsider i = i0 as Element of ( dom G) by FINSEQ_1:def 3;

        take i;

        consider rseqi be Real_Sequence, seqi be sequence of (G . i) such that

         A14: rseqi = (yyseq . i) & seqi is convergent & rseqi is convergent & ( lim rseqi) = 0 & (rseqi = ||.(seqi - ( lim seqi)).|| & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i)) by A7;

        take rseqi, seqi;

        thus (for k be Element of NAT holds (rseqi . k) = ((yseq . k) . i0)) & i = i0 & seqi is convergent & rseqi is convergent & ( lim rseqi) = (( 0* I) . i) & rseqi = ||.(seqi - ( lim seqi)).|| & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i) by A12, A14;

      end;

      reconsider xseq = yseq as sequence of ( REAL-NS I) by REAL_NS1:def 4;

      xseq = yseq;

      then

      consider xseq be sequence of ( REAL-NS I), yseq be sequence of ( REAL I) such that

       A15: xseq = yseq and

       A16: for i0 be Element of NAT st i0 in ( Seg I) holds ex i be Element of ( dom G), rseqi be Real_Sequence, seqi be sequence of (G . i) st (for k be Element of NAT holds (rseqi . k) = ((yseq . k) . i0)) & i = i0 & seqi is convergent & rseqi is convergent & ( lim rseqi) = (( 0* I) . i) & rseqi = ||.(seqi - ( lim seqi)).|| & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i) by A13;

      

       A17: for i be Nat st i in ( Seg I) holds ex rseqi be Real_Sequence st (for k be Nat holds (rseqi . k) = ((yseq . k) . i)) & rseqi is convergent & (( 0* I) . i) = ( lim rseqi)

      proof

        let i0 be Nat;

        assume i0 in ( Seg I);

        then

        consider i be Element of ( dom G), rseqi be Real_Sequence, seqi be sequence of (G . i) such that

         A18: for k be Element of NAT holds (rseqi . k) = ((yseq . k) . i0) and

         A19: i = i0 & seqi is convergent & rseqi is convergent & ( lim rseqi) = (( 0* I) . i) & rseqi = ||.(seqi - ( lim seqi)).|| & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i) by A16;

        take rseqi;

        thus for k be Nat holds (rseqi . k) = ((yseq . k) . i0)

        proof

          let k be Nat;

          k in NAT by ORDINAL1:def 12;

          hence thesis by A18;

        end;

        thus thesis by A19;

      end;

      

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

      now

        let x be object;

        assume x in NAT ;

        then

        reconsider i = x as Element of NAT ;

        reconsider seqimx0 = ((seq . i) - x0) as Element of ( product ( carr G)) by A20;

         A21:

        now

          reconsider mx0 = ( - x0) as Element of ( product ( carr G)) by A20;

          let k be Nat;

          assume

           A22: k in ( dom ( normsequence (G,seqimx0)));

          

           A23: ( len G) = ( len ( normsequence (G,seqimx0))) by Def11;

          then

          reconsider k0 = k as Element of ( dom G) by A22, FINSEQ_3: 29;

          k in ( Seg I) by A22, A23, FINSEQ_1:def 3;

          then

          consider k1 be Element of ( dom G), rseqk1i be Real_Sequence, seqk1i be sequence of (G . k1) such that

           A24: for j be Element of NAT holds (rseqk1i . j) = ((yseq . j) . k) and

           A25: k1 = k and seqk1i is convergent and rseqk1i is convergent and ( lim rseqk1i) = (( 0* I) . k1) and

           A26: rseqk1i = ||.(seqk1i - ( lim seqk1i)).|| and

           A27: for m be Element of NAT holds ex seqk1m be Element of ( product ( carr G)) st seqk1m = (seq . m) & (seqk1i . m) = (seqk1m . k1) by A16;

          consider seqk0 be sequence of (G . k0) such that seqk0 is convergent and

           A28: (y0 . k0) = ( lim seqk0) and

           A29: for m be Element of NAT holds ex seqm0 be Element of ( product ( carr G)) st seqm0 = (seq . m) & (seqk0 . m) = (seqm0 . k0) by A2;

          

           A30: ex seqm0 be Element of ( product ( carr G)) st seqm0 = (seq . i) & (seqk0 . i) = (seqm0 . k0) by A29;

          now

            let x be object;

            assume x in NAT ;

            then

            reconsider m = x as Element of NAT ;

            (ex seqk1m be Element of ( product ( carr G)) st seqk1m = (seq . m) & (seqk1i . m) = (seqk1m . k1)) & ex seqm0 be Element of ( product ( carr G)) st seqm0 = (seq . m) & (seqk0 . m) = (seqm0 . k0) by A29, A27;

            hence (seqk1i . x) = (seqk0 . x) by A25;

          end;

          then

           A31: seqk1i = seqk0 by A25, FUNCT_2: 12;

          ( len G) = ( len ( carr G)) by PRVECT_1:def 11;

          then

           A32: ( dom G) = ( dom ( carr G)) by FINSEQ_3: 29;

          ( - x0) = (( - 1) * x0) by RLVECT_1: 16;

          then (mx0 . k0) = (( - jj) * ( lim seqk0)) by A1, A20, A28, A32, Lm4;

          then ( - ( lim seqk0)) = (mx0 . k0) by RLVECT_1: 16;

          then

           A33: (seqimx0 . k0) = ((seqk0 . i) - ( lim seqk0)) by A20, A30, A32, Lm3;

          

          thus (( normsequence (G,seqimx0)) . k) = (the normF of (G . k0) . (seqimx0 . k0)) by Def11

          .= ||.((seqk0 - ( lim seqk0)) . i).|| by A33, NORMSP_1:def 4

          .= ( ||.(seqk1i - ( lim seqk1i)).|| . i) by A25, A31, NORMSP_0:def 4

          .= ((yseq . i) . k) by A24, A26;

        end;

        ( len (yseq . i)) = I by CARD_1:def 7;

        then ( len (yseq . i)) = ( len ( normsequence (G,seqimx0))) by Def11;

        then ( dom (yseq . i)) = ( dom ( normsequence (G,seqimx0))) by FINSEQ_3: 29;

        then

         A34: (yseq . i) = ( normsequence (G,seqimx0)) by A21, FINSEQ_1: 13;

        

        thus ( ||.(xseq - ( 0. ( REAL-NS I))).|| . x) = ||.((xseq - ( 0. ( REAL-NS I))) . i).|| by NORMSP_0:def 4

        .= ||.((xseq . i) - ( 0. ( REAL-NS I))).|| by NORMSP_1:def 4

        .= ||.(xseq . i).||

        .= |.(yseq . i).| by A15, REAL_NS1: 1

        .= ||.((seq . i) - x0).|| by A34, Th7

        .= ||.((seq - x0) . i).|| by NORMSP_1:def 4

        .= ( ||.(seq - x0).|| . x) by NORMSP_0:def 4;

      end;

      then

       A35: ||.(xseq - ( 0. ( REAL-NS I))).|| = ||.(seq - x0).|| by FUNCT_2: 12;

      ( 0* I) = ( 0. ( REAL-NS I)) by REAL_NS1:def 4;

      then xseq is convergent & ( lim xseq) = ( 0. ( REAL-NS I)) by A15, A17, REAL_NS1: 11;

      then ||.(seq - x0).|| is convergent & ( lim ||.(seq - x0).||) = 0 by A35, Lm7;

      hence thesis by Lm7;

    end;

    theorem :: PRVECT_2:14

    for G be RealNormSpace-Sequence st for i be Element of ( dom G) holds (G . i) is complete holds ( product G) is complete

    proof

      let G be RealNormSpace-Sequence such that

       A1: for i be Element of ( dom G) holds (G . i) 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 be sequence of ( product G) holds seq is Cauchy_sequence_by_Norm implies seq is convergent

      proof

        let seq be sequence of ( product G);

        defpred PPG[ Nat, object] means ex i be Element of ( dom G) st i = $1 & ex seqi be sequence of (G . i) st seqi is convergent & $2 = ( lim seqi) & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i);

        assume

         A3: seq is Cauchy_sequence_by_Norm;

        

         A4: for k be Nat st k in ( Seg I) holds ex x be object st PPG[k, x]

        proof

          let k be Nat;

          assume k in ( Seg I);

          then

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

          defpred P1[ Element of NAT , Element of (G . i)] means ex seqm be Element of ( product ( carr G)) st seqm = (seq . $1) & $2 = (seqm . i);

          

           A5: for x be Element of NAT holds ex y be Element of (G . i) st P1[x, y]

          proof

            let x be Element of NAT ;

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

             A6: seqm = (seq . x) by A2;

            ( len G) = ( len ( carr G)) by PRVECT_1:def 11;

            then

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

            take (seqm . i);

            (( carr G) . i) = the carrier of (G . i) by PRVECT_1:def 11;

            hence thesis by A6, A7, CARD_3: 9;

          end;

          ex f be sequence of the carrier of (G . i) st for x be Element of NAT holds P1[x, (f . x)] from FUNCT_2:sch 3( A5);

          then

          consider seqi be sequence of (G . i) such that

           A8: for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i);

          

           A9: for m be Nat holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i)

          proof

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            hence thesis by A8;

          end;

          take ( lim seqi);

          now

            let r1 be Real such that

             A10: r1 > 0 ;

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

            consider k be Nat such that

             A11: for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by A3, A10, RSSPACE3: 8;

            take k;

            let n,m be Nat;

            assume n >= k & m >= k;

            then

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

            (ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i)) & ex seqn be 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;

          end;

          then

           A13: seqi is Cauchy_sequence_by_Norm by RSSPACE3: 8;

          (G . i) is complete by A1;

          hence thesis by A8, A13, LOPBAN_1:def 15;

        end;

        consider yy0 be FinSequence such that

         A14: ( dom yy0) = ( Seg I) & for j be Nat st j in ( Seg I) holds PPG[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 PRVECT_1:def 11;

         A17:

        now

          let i be object;

          assume i in ( dom ( carr G));

          then

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

          reconsider 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 be Element of ( dom G) st i0 = j & ex seqi be sequence of (G . i0) st seqi is convergent & (yy0 . j) = ( lim seqi) & for m be Element of NAT holds ex seqm be 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 PRVECT_1:def 11;

        end;

        ( dom ( carr G)) = ( Seg ( len ( carr G))) & ( len G) = ( len ( carr G)) by PRVECT_1:def 11, FINSEQ_1:def 3;

        then

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

         A18:

        now

          let i be Element of ( dom G);

          reconsider j = i as Element of NAT ;

          i in ( dom G);

          then i in ( Seg I) by FINSEQ_1:def 3;

          then

          consider i0 be Element of ( dom G) such that

           A19: i0 = j and

           A20: ex seqi be sequence of (G . i0) st seqi is convergent & (yy0 . j) = ( lim seqi) & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i0) by A14;

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

           A21: seqi is convergent & (yy0 . j) = ( lim seqi) & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i0) by A20;

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

          take seqi;

          thus seqi is convergent & (y0 . i) = ( lim seqi) & for m be Element of NAT holds ex seqm be Element of ( product ( carr G)) st seqm = (seq . m) & (seqi . m) = (seqm . i) by A19, A21;

        end;

        reconsider x0 = y0 as Point of ( product G) by A2;

        x0 = y0;

        hence thesis by A18, Th13;

      end;

      hence thesis by LOPBAN_1:def 15;

    end;