euclid_7.miz



    begin

    reserve i,j,m,n for Nat,

z,B0 for set,

f,x0 for real-valued FinSequence;

    ::$Canceled

    theorem :: EUCLID_7:2

    

     Th1: for R be Relation, Y be set st ( rng R) c= Y holds (R " Y) = ( dom R)

    proof

      let R be Relation, Y be set;

      assume ( rng R) c= Y;

      then (( rng R) /\ Y) = ( rng R) by XBOOLE_1: 28;

      

      hence (R " Y) = (R " ( rng R)) by RELAT_1: 133

      .= ( dom R) by RELAT_1: 134;

    end;

    

     Lm1: for X be set, Y be non empty set, f be Function of X, Y st f is bijective holds ( card X) = ( card Y) by EULER_1: 11;

    theorem :: EUCLID_7:3

    ( <*z*> * <*1*>) = <*z*>

    proof

      

       A1: ( dom <*z*>) = ( Seg 1) by FINSEQ_1: 38;

      ( rng <*1*>) = {1} by FINSEQ_1: 38;

      then

       A2: ( dom ( <*z*> * <*1*>)) = ( dom <*1*>) by A1, FINSEQ_1: 2, RELAT_1: 27;

      

       A3: ( dom <*1*>) = ( Seg 1) by FINSEQ_1: 38;

      then 1 in ( dom <*1*>) by FINSEQ_1: 2, TARSKI:def 1;

      

      then (( <*z*> * <*1*>) . 1) = ( <*z*> . ( <*1*> . 1)) by FUNCT_1: 13

      .= ( <*z*> . 1) by FINSEQ_1: 40

      .= z by FINSEQ_1: 40;

      hence thesis by A3, A2, FINSEQ_1:def 8;

    end;

    theorem :: EUCLID_7:4

    for x be Element of ( REAL 0 ) holds x = ( <*> REAL );

    theorem :: EUCLID_7:5

    

     Th4: for a,b,c be Element of ( REAL n) holds (((a - b) + c) + b) = (a + c)

    proof

      let a,b,c be Element of ( REAL n);

      reconsider a2 = a, b2 = b, c2 = c as Element of (n -tuples_on REAL );

      (((a2 - b2) + c2) + b2) = (((a2 + ( - b2)) + b2) + c2) by RFUNCT_1: 8

      .= ((a2 + (b2 + ( - b2))) + c2) by RFUNCT_1: 8

      .= ((a2 + (n |-> ( In ( 0 , REAL )))) + c2) by RVSUM_1: 22

      .= (a2 + c2) by RVSUM_1: 16;

      hence thesis;

    end;

    registration

      let f1,f2 be FinSequence;

      cluster <:f1, f2:> -> FinSequence-like;

      coherence

      proof

        ( dom <:f1, f2:>) = (( dom f1) /\ ( dom f2)) by FUNCT_3:def 7;

        hence thesis by VALUED_1: 19;

      end;

    end

    definition

      let D be set, f1,f2 be FinSequence of D;

      :: original: <:

      redefine

      func <:f1,f2:> -> FinSequence of [:D, D:] ;

      coherence

      proof

        

         A1: [:( rng f1), ( rng f2):] c= [:D, D:] by ZFMISC_1: 96;

        ( rng <:f1, f2:>) c= [:( rng f1), ( rng f2):] by FUNCT_3: 51;

        then ( rng <:f1, f2:>) c= [:D, D:] by A1;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    

     Lm2: n < m implies ex k be Nat st m = ((n + 1) + k)

    proof

      assume

       A1: n < m;

      then

      consider k1 be Nat such that

       A2: m = (n + k1) by NAT_1: 10;

      k1 <> 0 by A1, A2;

      then

      consider n1 be Nat such that

       A3: k1 = (n1 + 1) by NAT_1: 6;

      take n1;

      thus m = ((n + 1) + n1) by A2, A3;

    end;

    definition

      let h be real-valued FinSequence;

      :: original: increasing

      redefine

      :: EUCLID_7:def1

      attr h is increasing means for i be Nat st 1 <= i & i < ( len h) holds (h . i) < (h . (i + 1));

      compatibility

      proof

        hereby

          assume

           A1: h is increasing;

          let i be Nat such that

           A2: 1 <= i and

           A3: i < ( len h);

          

           A4: 1 <= (i + 1) by NAT_1: 12;

          (i + 1) <= ( len h) by A3, NAT_1: 13;

          then

           A5: (i + 1) in ( dom h) by A4, FINSEQ_3: 25;

          

           A6: i < (i + 1) by NAT_1: 16;

          i in ( dom h) by A2, A3, FINSEQ_3: 25;

          hence (h . i) < (h . (i + 1)) by A1, A5, A6, VALUED_0:def 13;

        end;

        assume

         A7: for i be Nat st 1 <= i & i < ( len h) holds (h . i) < (h . (i + 1));

        now

          let n,m be ExtReal;

          assume

           A8: n in ( dom h);

          assume

           A9: m in ( dom h);

          then

          reconsider m1 = m, n1 = n as Element of NAT by A8;

          defpred X[ Nat] means (n1 + $1) < ( len h) implies (h . n) < (h . ((n1 + 1) + $1));

           A10:

          now

            let a be Nat such that

             A11: X[a];

            thus X[(a + 1)]

            proof

              

               A12: ((n1 + a) + 0 ) < ((n1 + a) + 1) by XREAL_1: 6;

              assume

               A13: (n1 + (a + 1)) < ( len h);

              1 <= (1 + (n1 + a)) by NAT_1: 11;

              then (h . ((n1 + 1) + a)) < (h . (((n1 + 1) + a) + 1)) by A7, A13;

              hence thesis by A11, A13, A12, XXREAL_0: 2;

            end;

          end;

          1 <= n by A8, FINSEQ_3: 25;

          then

           A14: X[ 0 ] by A7;

          

           A15: for k be Nat holds X[k] from NAT_1:sch 2( A14, A10);

          assume n < m;

          then

          consider k be Nat such that

           A16: m1 = ((n1 + 1) + k) by Lm2;

          m <= ( len h) by A9, FINSEQ_3: 25;

          then (m1 - 1) < (( len h) - 0 ) by XREAL_1: 15;

          then (n1 + k) < ( len h) by A16;

          hence (h . n) < (h . m) by A16, A15;

        end;

        hence thesis by VALUED_0:def 13;

      end;

    end

    theorem :: EUCLID_7:6

    

     Th5: for h be real-valued FinSequence st h is increasing holds for i,j be Nat st i < j & 1 <= i & j <= ( len h) holds (h . i) < (h . j)

    proof

      let h be real-valued FinSequence;

      assume

       A1: h is increasing;

      let i,j be Nat;

      assume that

       A2: i < j and

       A3: 1 <= i and

       A4: j <= ( len h);

      defpred P[ Nat] means ((i + 1) + $1) <= ( len h) implies (h . i) < (h . ((i + 1) + $1));

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A6: P[k];

        ((i + 1) + (k + 1)) <= ( len h) implies (h . i) < (h . ((i + 1) + (k + 1)))

        proof

          

           A7: (i + 1) <= ((i + 1) + k) by NAT_1: 11;

          i < (i + 1) by XREAL_1: 29;

          then i < ((i + 1) + k) by A7, XXREAL_0: 2;

          then

           A8: 1 < ((i + 1) + k) by A3, XXREAL_0: 2;

          k < (k + 1) by XREAL_1: 29;

          then

           A9: ((i + 1) + k) < ((i + 1) + (k + 1)) by XREAL_1: 6;

          assume

           A10: ((i + 1) + (k + 1)) <= ( len h);

          then ((i + 1) + k) < ( len h) by A9, XXREAL_0: 2;

          then (h . ((i + 1) + k)) < (h . (((i + 1) + k) + 1)) by A1, A8;

          hence (h . i) < (h . ((i + 1) + (k + 1))) by A6, A10, A9, XXREAL_0: 2;

        end;

        hence P[(k + 1)];

      end;

      i < ( len h) by A2, A4, XXREAL_0: 2;

      then

       A11: P[ 0 ] by A1, A3;

      for k be Nat holds P[k] from NAT_1:sch 2( A11, A5);

      then

       A12: ((i + 1) + (j -' (i + 1))) <= ( len h) implies (h . i) < (h . ((i + 1) + (j -' (i + 1))));

      (i + 1) <= j by A2, NAT_1: 13;

      then (j -' (i + 1)) = (j - (i + 1)) by XREAL_1: 233;

      hence (h . i) < (h . j) by A4, A12;

    end;

    theorem :: EUCLID_7:7

    

     Th6: for h be real-valued FinSequence st h is increasing holds for i,j be Nat st i <= j & 1 <= i & j <= ( len h) holds (h . i) <= (h . j)

    proof

      let h be real-valued FinSequence;

      assume

       A1: h is increasing;

      let i,j be Nat;

      assume that

       A2: i <= j and

       A3: 1 <= i and

       A4: j <= ( len h);

      i < j or i = j by A2, XXREAL_0: 1;

      hence thesis by A1, A3, A4, Th5;

    end;

    theorem :: EUCLID_7:8

    

     Th7: for h be natural-valued FinSequence st h is increasing holds for i be Nat st i <= ( len h) & 1 <= (h . 1) holds i <= (h . i)

    proof

      let h be natural-valued FinSequence;

      assume

       A1: h is increasing;

      defpred P[ Nat] means $1 <= ( len h) implies $1 <= (h . $1);

      let i be Nat;

      assume that

       A2: i <= ( len h) and

       A3: 1 <= (h . 1);

      

       A4: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A5: P[k];

        (k + 1) <= ( len h) implies (k + 1) <= (h . (k + 1))

        proof

          

           A6: k < (k + 1) by XREAL_1: 29;

          assume

           A7: (k + 1) <= ( len h);

          then

           A8: k < ( len h) by A6, XXREAL_0: 2;

          per cases ;

            suppose k = 0 ;

            hence (k + 1) <= (h . (k + 1)) by A3;

          end;

            suppose k > 0 ;

            then ( 0 + 1) <= k by NAT_1: 13;

            then (h . k) < (h . (k + 1)) by A1, A8;

            then k < (h . (k + 1)) by A5, A7, A6, XXREAL_0: 2;

            hence (k + 1) <= (h . (k + 1)) by NAT_1: 13;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A9: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A9, A4);

      hence i <= (h . i) by A2;

    end;

    theorem :: EUCLID_7:9

    

     Th8: for V be RealLinearSpace, X be Subspace of V st V is strict & X is strict & the carrier of X = the carrier of V holds X = V

    proof

      let V be RealLinearSpace, X be Subspace of V;

      assume that

       A1: V is strict and

       A2: X is strict and

       A3: the carrier of X = the carrier of V;

      

       A4: the Mult of X = (the Mult of V | [: REAL , the carrier of V:]) by A3, RLSUB_1:def 2

      .= the Mult of V;

      

       A5: ( 0. X) = ( 0. V) by RLSUB_1:def 2;

      the addF of X = (the addF of V || the carrier of V) by A3, RLSUB_1:def 2

      .= (the addF of V | [:the carrier of V, the carrier of V:]) by REALSET1:def 2

      .= the addF of V;

      hence X = V by A1, A2, A3, A5, A4;

    end;

    definition

      let D be set;

      let F be FinSequence of D;

      let h be Permutation of ( dom F);

      :: EUCLID_7:def2

      func F (*) h -> FinSequence of D equals (F * h);

      coherence

      proof

        reconsider G = F as Function;

        

         A1: (h " ( dom G)) = (h " ( rng h)) by FUNCT_2:def 3

        .= ( dom h) by RELAT_1: 134;

        ( dom (G * h)) = (h " ( dom G)) by RELAT_1: 147

        .= ( dom F) by A1, FUNCT_2: 52

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

        then

         A2: (F * h) is FinSequence by FINSEQ_1:def 2;

        ( rng (F * h)) c= D;

        hence thesis by A2, FINSEQ_1:def 4;

      end;

    end

    theorem :: EUCLID_7:10

    

     Th9: for D be non empty set, f be FinSequence of D st 1 <= i & i <= ( len f) & 1 <= j & j <= ( len f) holds (( Swap (f,i,j)) . i) = (f . j) & (( Swap (f,i,j)) . j) = (f . i)

    proof

      let D be non empty set, f be FinSequence of D;

      assume that

       A1: 1 <= i and

       A2: i <= ( len f) and

       A3: 1 <= j and

       A4: j <= ( len f);

      

       A5: ( len ( Replace (f,i,(f /. j)))) = ( len f) by FINSEQ_7: 5;

      

       A6: ( len ( Swap (f,i,j))) = ( len f) by FINSEQ_7: 18;

      then (( Swap (f,i,j)) /. j) = (( Swap (f,i,j)) . j) by A3, A4, FINSEQ_4: 15;

      

      then

       A7: (( Swap (f,i,j)) . j) = (( Replace (( Replace (f,i,(f /. j))),j,(f /. i))) /. j) by A1, A2, A3, A4, FINSEQ_7:def 2

      .= (f /. i) by A3, A4, A5, FINSEQ_7: 8

      .= (f . i) by A1, A2, FINSEQ_4: 15;

      

       A8: ( Swap (f,i,j)) = ( Swap (f,j,i)) by FINSEQ_7: 21;

      

       A9: ( len ( Replace (f,j,(f /. i)))) = ( len f) by FINSEQ_7: 5;

      (( Swap (f,i,j)) /. i) = (( Swap (f,i,j)) . i) by A1, A2, A6, FINSEQ_4: 15;

      

      then (( Swap (f,i,j)) . i) = (( Replace (( Replace (f,j,(f /. i))),i,(f /. j))) /. i) by A1, A2, A3, A4, A8, FINSEQ_7:def 2

      .= (f /. j) by A1, A2, A9, FINSEQ_7: 8

      .= (f . j) by A3, A4, FINSEQ_4: 15;

      hence thesis by A7;

    end;

    theorem :: EUCLID_7:11

    

     Th10: {} is Permutation of {}

    proof

      

       A1: ( rng {} ) = {} ;

      ( dom {} ) = {} ;

      then

      reconsider f = {} as Function of {} , {} by A1, FUNCT_2: 1;

      f is one-to-one onto Function of {} , {} by A1, FUNCT_2:def 3;

      hence thesis;

    end;

    theorem :: EUCLID_7:12

     <*1*> is Permutation of {1}

    proof

      set g = <*1*>;

      

       A1: ( rng g) = {1} by FINSEQ_1: 38;

      ( dom g) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      then

      reconsider f = g as Function of {1}, {1} by A1, FUNCT_2: 1;

      f is one-to-one onto Function of {1}, {1} by A1, FUNCT_2:def 3;

      hence thesis;

    end;

    theorem :: EUCLID_7:13

    

     Th12: for h be FinSequence of REAL holds h is one-to-one iff ( sort_a h) is one-to-one

    proof

      let h be FinSequence of REAL ;

      

       A1: (h,( sort_a h)) are_fiberwise_equipotent by RFINSEQ2:def 6;

      then ex H be Function st ( dom H) = ( dom ( sort_a h)) & ( rng H) = ( dom h) & H is one-to-one & ( sort_a h) = (h * H) by CLASSES1: 77;

      hence h is one-to-one implies ( sort_a h) is one-to-one;

      ex G be Function st ( dom G) = ( dom h) & ( rng G) = ( dom ( sort_a h)) & G is one-to-one & h = (( sort_a h) * G) by A1, CLASSES1: 77;

      hence ( sort_a h) is one-to-one implies h is one-to-one;

    end;

    theorem :: EUCLID_7:14

    

     Th13: for h be FinSequence of NAT st h is one-to-one holds ex h3 be Permutation of ( dom h), h2 be FinSequence of NAT st h2 = (h * h3) & h2 is increasing & ( dom h) = ( dom h2) & ( rng h) = ( rng h2)

    proof

      let h be FinSequence of NAT ;

      assume

       A1: h is one-to-one;

      per cases ;

        suppose

         A2: ( dom h) <> {} ;

        ( rng h) c= REAL by NUMBERS: 19;

        then

        reconsider hr = h as FinSequence of REAL by FINSEQ_1:def 4;

        

         A3: (hr,( sort_a hr)) are_fiberwise_equipotent by RFINSEQ2:def 6;

        then

        consider H be Function such that

         A4: ( dom H) = ( dom ( sort_a hr)) and

         A5: ( rng H) = ( dom hr) and

         A6: H is one-to-one and

         A7: ( sort_a hr) = (hr * H) by CLASSES1: 77;

        ( rng ( sort_a hr)) = ( rng hr) by A3, CLASSES1: 75;

        then

        reconsider h4 = ( sort_a hr) as FinSequence of NAT by FINSEQ_1:def 4;

        

         A8: ( rng h) = ( rng h4) by A5, A7, RELAT_1: 28;

        

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

        for i be Nat st 1 <= i & i < ( len h4) holds (h4 . i) < (h4 . (i + 1))

        proof

          let i be Nat;

          assume that

           A10: 1 <= i and

           A11: i < ( len h4);

          

           A12: (i + 1) <= ( len h4) by A11, NAT_1: 13;

          

           A13: i in ( dom h4) by A9, A10, A11, FINSEQ_1: 1;

          1 < (i + 1) by A10, XREAL_1: 29;

          then

           A14: (i + 1) in ( dom h4) by A9, A12, FINSEQ_1: 1;

          

           A15: h4 is one-to-one by A1, Th12;

           A16:

          now

            assume (h4 . i) = (h4 . (i + 1));

            then i = (i + 1) by A14, A13, A15, FUNCT_1:def 4;

            hence contradiction;

          end;

          (h4 . i) <= (h4 . (i + 1)) by A14, A13, INTEGRA2:def 1;

          hence (h4 . i) < (h4 . (i + 1)) by A16, XXREAL_0: 1;

        end;

        then

         A17: h4 is increasing;

        ( dom ( sort_a hr)) = ( dom hr) by RFINSEQ2: 31;

        then

        reconsider H2 = H as Function of ( dom h), ( dom h) by A4, A5, FUNCT_2: 1;

        H2 is onto by A5, FUNCT_2:def 3;

        then

        reconsider h5 = H as Permutation of ( dom h) by A6;

        

         A18: h4 = (h * h5) by A7;

        ( dom h) = ( dom h5) by A2, FUNCT_2:def 1

        .= ( dom h4) by A4;

        hence thesis by A18, A17, A8;

      end;

        suppose

         A19: ( dom h) = {} ;

        then ( rng h) = {} by RELAT_1: 42;

        then

        reconsider h5 = h as Function of {} , {} by A19, FUNCT_2: 1;

        reconsider h22 = (h * h5) as FinSequence of NAT ;

        h22 is increasing;

        hence thesis by A19, Th10;

      end;

    end;

    begin

    definition

      let B0 be set;

      :: EUCLID_7:def3

      attr B0 is R-orthogonal means

      : Def3: for x,y be real-valued FinSequence st x in B0 & y in B0 & x <> y holds |(x, y)| = 0 ;

    end

    registration

      cluster empty -> R-orthogonal for set;

      coherence ;

    end

    theorem :: EUCLID_7:15

    B0 is R-orthogonal iff for x,y be real-valued FinSequence st x in B0 & y in B0 & x <> y holds (x,y) are_orthogonal

    proof

      thus B0 is R-orthogonal implies for x,y be real-valued FinSequence st x in B0 & y in B0 & x <> y holds (x,y) are_orthogonal ;

      assume

       A1: for x,y be real-valued FinSequence st x in B0 & y in B0 & x <> y holds (x,y) are_orthogonal ;

      let x,y be real-valued FinSequence;

      assume that

       A2: x in B0 and

       A3: y in B0 and

       A4: x <> y;

      (x,y) are_orthogonal by A1, A2, A3, A4;

      hence |(x, y)| = 0 ;

    end;

    definition

      let B0 be set;

      :: EUCLID_7:def4

      attr B0 is R-normal means

      : Def4: for x be real-valued FinSequence st x in B0 holds |.x.| = 1;

    end

    registration

      cluster empty -> R-normal for set;

      coherence ;

    end

    registration

      cluster R-normal for set;

      existence

      proof

        take {} ;

        thus thesis;

      end;

    end

    registration

      let B0,B1 be R-normal set;

      cluster (B0 \/ B1) -> R-normal;

      coherence

      proof

        let x be real-valued FinSequence;

        assume x in (B0 \/ B1);

        then x in B0 or x in B1 by XBOOLE_0:def 3;

        hence thesis by Def4;

      end;

    end

    theorem :: EUCLID_7:16

    

     Th15: |.f.| = 1 implies {f} is R-normal by TARSKI:def 1;

    theorem :: EUCLID_7:17

    

     Th16: B0 is R-normal & |.x0.| = 1 implies (B0 \/ {x0}) is R-normal

    proof

      assume that

       A1: B0 is R-normal and

       A2: |.x0.| = 1;

       {x0} is R-normal by A2, Th15;

      hence (B0 \/ {x0}) is R-normal by A1;

    end;

    definition

      let B0 be set;

      :: EUCLID_7:def5

      attr B0 is R-orthonormal means B0 is R-orthogonal R-normal;

    end

    registration

      cluster R-orthonormal -> R-orthogonal R-normal for set;

      coherence ;

      cluster R-orthogonal R-normal -> R-orthonormal for set;

      coherence ;

    end

    registration

      cluster { <*1*>} -> R-orthonormal;

      coherence

      proof

        set B0 = { <*1*>};

        thus for x,y be real-valued FinSequence st x in B0 & y in B0 & x <> y holds |(x, y)| = 0

        proof

          let x,y be real-valued FinSequence;

          assume that

           A1: x in B0 and

           A2: y in B0;

          x = <*1*> by A1, TARSKI:def 1;

          hence thesis by A2, TARSKI:def 1;

        end;

        let x be real-valued FinSequence;

        assume x in B0;

        then x = <*1*> by TARSKI:def 1;

        then ( sqr x) = <*(1 ^2 )*> by RVSUM_1: 55;

        hence thesis by RVSUM_1: 73, SQUARE_1: 18;

      end;

    end

    registration

      cluster R-orthonormal non empty for set;

      existence

      proof

        take { <*1*>};

        thus thesis;

      end;

    end

    registration

      let n;

      cluster R-orthonormal for Subset of ( REAL n);

      existence

      proof

        ( {} ( REAL n)) is R-orthonormal;

        hence thesis;

      end;

    end

    definition

      let n be Nat;

      let B0 be Subset of ( REAL n);

      :: EUCLID_7:def6

      attr B0 is complete means

      : Def6: for B be R-orthonormal Subset of ( REAL n) st B0 c= B holds B = B0;

    end

    definition

      let n be Nat, B0 be Subset of ( REAL n);

      :: EUCLID_7:def7

      attr B0 is orthogonal_basis means B0 is R-orthonormal complete;

    end

    registration

      let n be Nat;

      cluster orthogonal_basis -> R-orthonormal complete for Subset of ( REAL n);

      coherence ;

      cluster R-orthonormal complete -> orthogonal_basis for Subset of ( REAL n);

      coherence ;

    end

    theorem :: EUCLID_7:18

    

     Th17: for B0 be Subset of ( REAL 0 ) st B0 is orthogonal_basis holds B0 = {}

    proof

      let B0 be Subset of ( REAL 0 );

      assume that

       A1: B0 is orthogonal_basis and

       A2: B0 <> {} ;

      set x = the Element of B0;

      x in B0 by A2;

      then

      reconsider x0 = x as Element of ( REAL 0 );

       |(( 0* ( len x0)), ( 0* ( len x0)))| = 0 by EUCLID_2: 9;

      then |.( 0* ( len x0)).| = 0 by EUCLID_2: 8;

      hence contradiction by A1, A2, Def4;

    end;

    theorem :: EUCLID_7:19

    for B0 be Subset of ( REAL n), y be Element of ( REAL n) st B0 is orthogonal_basis & (for x be Element of ( REAL n) st x in B0 holds |(x, y)| = 0 ) holds y = ( 0* n)

    proof

      let B0 be Subset of ( REAL n), y be Element of ( REAL n);

      assume that

       A1: B0 is orthogonal_basis and

       A2: for x be Element of ( REAL n) st x in B0 holds |(x, y)| = 0 ;

      now

        reconsider y1 = ((1 / |.y.|) * y) as Element of ( REAL n);

        reconsider B1 = (B0 \/ {y1}) as Subset of ( REAL n);

        y1 in {y1} by TARSKI:def 1;

        then

         A3: y1 in B1 by XBOOLE_0:def 3;

        

         A4: ( len y) = n by CARD_1:def 7;

        for x2,y2 be real-valued FinSequence st x2 in B1 & y2 in B1 & x2 <> y2 holds |(x2, y2)| = 0

        proof

          let x2,y2 be real-valued FinSequence;

          assume that

           A5: x2 in B1 and

           A6: y2 in B1 and

           A7: x2 <> y2;

          reconsider X2 = x2, Y2 = y2 as Element of ( REAL n) by A5, A6;

          

           A8: ( len Y2) = n by CARD_1:def 7;

          per cases by A5, XBOOLE_0:def 3;

            suppose

             A9: x2 in B0;

            per cases by A6, XBOOLE_0:def 3;

              suppose y2 in B0;

              hence |(x2, y2)| = 0 by A1, A7, A9, Def3;

            end;

              suppose

               A10: y2 in {y1};

              

               A11: ( len X2) = n by CARD_1:def 7;

               |(x2, y)| = 0 by A2, A9;

              then

               A12: ((1 / |.y.|) * |(x2, y)|) = 0 ;

              y2 = y1 by A10, TARSKI:def 1;

              hence |(x2, y2)| = 0 by A4, A11, A12, RVSUM_1: 121;

            end;

          end;

            suppose

             A13: x2 in {y1};

            then x2 = y1 by TARSKI:def 1;

            then not y2 in {y1} by A7, TARSKI:def 1;

            then y2 in B0 by A6, XBOOLE_0:def 3;

            then |(y2, y)| = 0 by A2;

            then ((1 / |.y.|) * |(y2, y)|) = 0 ;

            then |(Y2, ((1 / |.y.|) * y))| = 0 by A4, A8, RVSUM_1: 121;

            hence |(x2, y2)| = 0 by A13, TARSKI:def 1;

          end;

        end;

        then

         A14: B1 is R-orthogonal;

        assume

         A15: y <> ( 0* n);

        

         A16: |.y1.| = ( |.(1 / |.y.|).| * |.y.|) by EUCLID: 11

        .= ((1 / |.y.|) * |.y.|) by ABSVALUE:def 1

        .= 1 by A15, EUCLID: 8, XCMPLX_1: 106;

        for x be real-valued FinSequence st x in B1 holds |.x.| = 1

        proof

          let x be real-valued FinSequence;

          assume x in B1;

          then x in B0 or x in {y1} by XBOOLE_0:def 3;

          hence |.x.| = 1 by A1, A16, Def4, TARSKI:def 1;

        end;

        then

         A17: B1 is R-normal;

        

         A18: ( len y1) = n by CARD_1:def 7;

         A19:

        now

          assume y1 in B0;

          then |(y1, y)| = 0 by A2;

          then ((1 / |.y.|) * |(y1, y)|) = 0 ;

          then |(y1, ((1 / |.y.|) * y))| = 0 by A4, A18, RVSUM_1: 121;

          hence contradiction by A16, EUCLID_2: 8;

        end;

        B0 c= B1 by XBOOLE_1: 7;

        hence contradiction by A1, A19, A3, A14, A17, Def6;

      end;

      hence y = ( 0* n);

    end;

    begin

    definition

      let n;

      let X be Subset of ( REAL n);

      :: EUCLID_7:def8

      attr X is linear_manifold means for x,y be Element of ( REAL n), a,b be Element of REAL st x in X & y in X holds ((a * x) + (b * y)) in X;

    end

    registration

      let n;

      cluster ( [#] ( REAL n)) -> linear_manifold;

      coherence

      proof

        let x,y be Element of ( REAL n), a,b be Element of REAL ;

        assume that x in ( [#] ( REAL n)) and y in ( [#] ( REAL n));

        ((a * x) + (b * y)) in ( REAL n);

        hence thesis by SUBSET_1:def 3;

      end;

    end

    theorem :: EUCLID_7:20

    

     Th19: {( 0* n)} is linear_manifold

    proof

      let x,y be Element of ( REAL n), a,b be Element of REAL ;

      assume that

       A1: x in {( 0* n)} and

       A2: y in {( 0* n)};

      reconsider nn = n as Element of NAT by ORDINAL1:def 12;

      

       A3: y = ( 0* n) by A2, TARSKI:def 1;

      x = ( 0* n) by A1, TARSKI:def 1;

      

      then ((a * x) + (b * y)) = (( 0* nn) + (b * ( 0* nn))) by A3, EUCLID_4: 2

      .= (( 0* nn) + ( 0* nn)) by EUCLID_4: 2

      .= ( 0* nn) by EUCLID_4: 1;

      hence ((a * x) + (b * y)) in {( 0* n)} by TARSKI:def 1;

    end;

    registration

      let n;

      cluster {( 0* n)} -> linear_manifold;

      coherence by Th19;

    end

    definition

      let n;

      let X be Subset of ( REAL n);

      :: EUCLID_7:def9

      func L_Span X -> Subset of ( REAL n) equals ( meet { Y where Y be Subset of ( REAL n) : Y is linear_manifold & X c= Y });

      correctness

      proof

        X c= ( REAL n);

        then X c= ( [#] ( REAL n)) by SUBSET_1:def 3;

        then ( [#] ( REAL n)) in { Y where Y be Subset of ( REAL n) : Y is linear_manifold & X c= Y };

        hence thesis by SETFAM_1: 7;

      end;

    end

    registration

      let n;

      let X be Subset of ( REAL n);

      cluster ( L_Span X) -> linear_manifold;

      coherence

      proof

        X c= ( REAL n);

        then X c= ( [#] ( REAL n)) by SUBSET_1:def 3;

        then ( [#] ( REAL n)) in { Y where Y be Subset of ( REAL n) : Y is linear_manifold & X c= Y };

        then

        reconsider Z = { Y where Y be Subset of ( REAL n) : Y is linear_manifold & X c= Y } as non empty set;

        let x,y be Element of ( REAL n), a,b be Element of REAL ;

        assume that

         A1: x in ( L_Span X) and

         A2: y in ( L_Span X);

        

         A3: for Y4 be set st Y4 in { Y where Y be Subset of ( REAL n) : Y is linear_manifold & X c= Y } holds ((a * x) + (b * y)) in Y4

        proof

          let Y4 be set;

          assume

           A4: Y4 in { Y where Y be Subset of ( REAL n) : Y is linear_manifold & X c= Y };

          then

           A5: ex Y0 be Subset of ( REAL n) st Y4 = Y0 & Y0 is linear_manifold & X c= Y0;

          

           A6: y in Y4 by A2, A4, SETFAM_1:def 1;

          x in Y4 by A1, A4, SETFAM_1:def 1;

          hence ((a * x) + (b * y)) in Y4 by A6, A5;

        end;

        Z <> {} ;

        hence ((a * x) + (b * y)) in ( L_Span X) by A3, SETFAM_1:def 1;

      end;

    end

    definition

      let n be Nat, f be FinSequence of ( REAL n);

      :: EUCLID_7:def10

      func accum f -> FinSequence of ( REAL n) means

      : Def10: ( len f) = ( len it ) & (f . 1) = (it . 1) & for i be Nat st 1 <= i & i < ( len f) holds (it . (i + 1)) = ((it /. i) + (f /. (i + 1)));

      existence

      proof

        per cases ;

          suppose

           A1: ( len f) > 0 ;

          reconsider q = <*(f /. 1)*> as FinSequence of ( REAL n);

          

           A2: ( 0 + 1) <= ( len f) by A1, NAT_1: 13;

          then (f /. 1) = (f . 1) by FINSEQ_4: 15;

          then

           A3: (q . 1) = (f . 1) by FINSEQ_1: 40;

          defpred P[ Nat] means ($1 + 1) <= ( len f) implies ex g be FinSequence of ( REAL n) st ($1 + 1) = ( len g) & (f . 1) = (g . 1) & (for i be Nat st 1 <= i & i < ($1 + 1) holds (g . (i + 1)) = ((g /. i) + (f /. (i + 1))));

          

           A4: for i be Nat st 1 <= i & i < ( 0 + 1) holds (q . (i + 1)) = ((q /. i) + (f /. (i + 1)));

          

           A5: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             A6: P[k];

            now

              per cases ;

                case

                 A7: ((k + 1) + 1) <= ( len f);

                (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

                then

                consider g be FinSequence of ( REAL n) such that

                 A8: (k + 1) = ( len g) and

                 A9: (f . 1) = (g . 1) and

                 A10: for i be Nat st 1 <= i & i < (k + 1) holds (g . (i + 1)) = ((g /. i) + (f /. (i + 1))) by A6, A7, XXREAL_0: 2;

                reconsider g2 = (g ^ <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*>) as FinSequence of ( REAL n);

                

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

                

                 A12: ( len g2) = (( len g) + ( len <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*>)) by FINSEQ_1: 22

                .= ((k + 1) + 1) by A8, FINSEQ_1: 40;

                

                 A13: for i be Nat st 1 <= i & i < ((k + 1) + 1) holds (g2 . (i + 1)) = ((g2 /. i) + (f /. (i + 1)))

                proof

                  let i be Nat;

                  assume that

                   A14: 1 <= i and

                   A15: i < ((k + 1) + 1);

                  

                   A16: i <= (k + 1) by A15, NAT_1: 13;

                  per cases by A16, XXREAL_0: 1;

                    suppose

                     A17: i < (k + 1);

                    

                     A18: 1 <= (i + 1) by NAT_1: 12;

                    (i + 1) <= (k + 1) by A17, NAT_1: 13;

                    then (i + 1) in ( Seg ( len g)) by A8, A18, FINSEQ_1: 1;

                    then

                     A19: (g2 . (i + 1)) = (g . (i + 1)) by A11, FINSEQ_1:def 7;

                    i in ( Seg ( len g)) by A8, A14, A16, FINSEQ_1: 1;

                    then

                     A20: (g2 . i) = (g . i) by A11, FINSEQ_1:def 7;

                    

                     A21: (g /. i) = (g . i) by A8, A14, A17, FINSEQ_4: 15;

                    (g2 /. i) = (g2 . i) by A12, A14, A15, FINSEQ_4: 15;

                    hence thesis by A10, A14, A17, A19, A20, A21;

                  end;

                    suppose

                     A22: i = (k + 1);

                    

                     A23: (g2 /. i) = (g2 . i) by A12, A14, A15, FINSEQ_4: 15;

                    i in ( Seg ( len g)) by A8, A14, A16, FINSEQ_1: 1;

                    then

                     A24: (g . i) = (g2 . i) by A11, FINSEQ_1:def 7;

                    (g /. i) = (g . i) by A8, A14, A16, FINSEQ_4: 15;

                    hence thesis by A8, A22, A24, A23, FINSEQ_1: 42;

                  end;

                end;

                1 <= (k + 1) by NAT_1: 11;

                then 1 in ( Seg ( len g)) by A8, FINSEQ_1: 1;

                then (g2 . 1) = (f . 1) by A9, A11, FINSEQ_1:def 7;

                hence P[(k + 1)] by A12, A13;

              end;

                case ((k + 1) + 1) > ( len f);

                hence P[(k + 1)];

              end;

            end;

            hence P[(k + 1)];

          end;

          (( len f) -' 1) = (( len f) - 1) by A2, XREAL_1: 233;

          then

           A25: ((( len f) -' 1) + 1) = ( len f);

          ( len q) = 1 by FINSEQ_1: 40;

          then

           A26: P[ 0 ] by A3, A4;

          for k be Nat holds P[k] from NAT_1:sch 2( A26, A5);

          hence thesis by A25;

        end;

          suppose

           A27: ( len f) <= 0 ;

          take f;

          thus ( len f) = ( len f) & (f . 1) = (f . 1);

          let i be Nat;

          thus thesis by A27;

        end;

      end;

      uniqueness

      proof

        let g1,g2 be FinSequence of ( REAL n);

        assume that

         A28: ( len f) = ( len g1) and

         A29: (f . 1) = (g1 . 1) and

         A30: for i be Nat st 1 <= i & i < ( len f) holds (g1 . (i + 1)) = ((g1 /. i) + (f /. (i + 1)));

        defpred P[ Nat] means 1 <= $1 & $1 <= ( len f) implies (g1 . $1) = (g2 . $1);

        assume that

         A31: ( len f) = ( len g2) and

         A32: (f . 1) = (g2 . 1) and

         A33: for i be Nat st 1 <= i & i < ( len f) holds (g2 . (i + 1)) = ((g2 /. i) + (f /. (i + 1)));

        

         A34: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A35: P[k];

          1 <= (k + 1) & (k + 1) <= ( len f) implies (g1 . (k + 1)) = (g2 . (k + 1))

          proof

            assume that 1 <= (k + 1) and

             A36: (k + 1) <= ( len f);

            

             A37: k < (k + 1) by XREAL_1: 29;

            then

             A38: k < ( len f) by A36, XXREAL_0: 2;

            per cases ;

              suppose

               A39: 1 <= k;

              then

               A40: (g2 . (k + 1)) = ((g2 /. k) + (f /. (k + 1))) by A33, A38;

              

               A41: k <= ( len g2) by A31, A36, A37, XXREAL_0: 2;

              

               A42: (g1 /. k) = (g1 . k) by A28, A38, A39, FINSEQ_4: 15;

              (g1 . (k + 1)) = ((g1 /. k) + (f /. (k + 1))) by A30, A38, A39;

              hence thesis by A35, A36, A37, A39, A40, A42, A41, FINSEQ_4: 15, XXREAL_0: 2;

            end;

              suppose 1 > k;

              then ( 0 + 1) > k;

              then k = 0 by NAT_1: 13;

              hence (g1 . (k + 1)) = (g2 . (k + 1)) by A29, A32;

            end;

          end;

          hence P[(k + 1)];

        end;

        

         A43: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A43, A34);

        hence g1 = g2 by A28, A31, FINSEQ_1: 14;

      end;

    end

    definition

      let n be Nat;

      let f be FinSequence of ( REAL n);

      :: EUCLID_7:def11

      func Sum f -> Element of ( REAL n) equals

      : Def11: (( accum f) . ( len f)) if ( len f) > 0

      otherwise ( 0* n);

      coherence

      proof

        

         A1: ( len f) = ( len ( accum f)) by Def10;

        now

          per cases ;

            case ( len f) > 0 ;

            then ( 0 + 1) <= ( len f) by NAT_1: 13;

            then ( len f) in ( dom ( accum f)) by A1, FINSEQ_3: 25;

            then (( accum f) . ( len f)) in ( rng ( accum f)) by FUNCT_1:def 3;

            hence (( accum f) . ( len f)) is Element of ( REAL n);

          end;

            case ( len f) <= 0 ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: EUCLID_7:21

    

     Th20: for F,F2 be FinSequence of ( REAL n), h be Permutation of ( dom F) st F2 = (F (*) h) holds ( Sum F2) = ( Sum F)

    proof

      let F,F2 be FinSequence of ( REAL n), h be Permutation of ( dom F);

      assume

       A1: F2 = (F (*) h);

      per cases ;

        suppose

         A2: ( len F) > 0 ;

        then

         A3: ( 0 + 1) <= ( len F) by NAT_1: 13;

        then

         A4: 1 in ( Seg ( len F)) by FINSEQ_1: 1;

        then

         A5: 1 in ( dom F) by FINSEQ_1:def 3;

        then

         A6: ( dom h) = ( dom F) by FUNCT_2:def 1;

        then ( rng h) = ( dom h) by FUNCT_2:def 3;

        then

         A7: ( dom F2) = ( dom h) by A1, RELAT_1: 27;

        then

         A8: ( Seg ( len F2)) = ( dom F) by A6, FINSEQ_1:def 3;

        set gF = ( accum F);

        

         A9: ( len F) = ( len gF) by Def10;

        

         A10: for i be Nat st 1 <= i & i < ( len F) holds (gF . (i + 1)) = ((gF /. i) + (F /. (i + 1))) by Def10;

        defpred P[ Nat] means for h2 be Permutation of ( dom F) st $1 < ( len F) & (for i be Nat st ($1 + 1) < i & i <= ( len F) holds (h2 . i) = i) holds (gF . ($1 + 1)) = (( accum (F (*) h2)) . ($1 + 1));

        

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

        1 in ( Seg ( len F2)) by A5, A6, A7, FINSEQ_1:def 3;

        then

         A12: 1 <= ( len F2) by FINSEQ_1: 1;

        

         A13: (( len F) -' 1) = (( len F) - 1) by A3, XREAL_1: 233;

        then

         A14: for i be Nat st ((( len F) -' 1) + 1) < i & i <= ( len F) holds (h . i) = i;

        

         A15: ( dom F) <> {} by A4, FINSEQ_1:def 3;

        

         A16: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A17: P[k];

          for h2 be Permutation of ( dom F) st (k + 1) < ( len F) & (for i be Nat st ((k + 1) + 1) < i & i <= ( len F) holds (h2 . i) = i) holds (gF . ((k + 1) + 1)) = (( accum (F (*) h2)) . ((k + 1) + 1))

          proof

            

             A18: 1 <= (k + 1) by NAT_1: 11;

            

             A19: (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

            let h2 be Permutation of ( dom F);

            assume that

             A20: (k + 1) < ( len F) and

             A21: for i be Nat st ((k + 1) + 1) < i & i <= ( len F) holds (h2 . i) = i;

            

             A22: ((k + 1) + 1) <= ( len F) by A20, NAT_1: 13;

            k < (k + 1) by XREAL_1: 29;

            then

             A23: k < ( len F) by A20, XXREAL_0: 2;

            

             A24: 1 < ((k + 1) + 1) by XREAL_1: 29;

            then

             A25: ((k + 1) + 1) in ( Seg ( len F)) by A22, FINSEQ_1: 1;

            then

             A26: ((k + 1) + 1) in ( dom F) by FINSEQ_1:def 3;

            

             A27: ( dom h2) = ( dom F) by A5, FUNCT_2:def 1;

            then

             A28: ( rng h2) = ( dom h2) by FUNCT_2:def 3;

            

            then

             A29: ( dom (F (*) h2)) = ( dom h2) by RELAT_1: 27

            .= ( dom F) by A5, FUNCT_2:def 1;

            then

             A30: ( Seg ( len (F (*) h2))) = ( dom F) by FINSEQ_1:def 3;

            then

             A31: ( Seg ( len (F (*) h2))) = ( Seg ( len F)) by FINSEQ_1:def 3;

            

             A32: ( len (F (*) h2)) = ( len F) by A30, FINSEQ_1:def 3;

            h2 is FinSequence by A11, A27, FINSEQ_1:def 2;

            then

            reconsider h2r = h2 as FinSequence of NAT by A27, A28, FINSEQ_1:def 4;

            ( dom h2) = ( Seg ( len F)) by A2, A11, FUNCT_2:def 1;

            then

             A33: ( len h2r) = ( len F) by FINSEQ_1:def 3;

            consider x be object such that

             A34: x in ( dom h2) and

             A35: ((k + 1) + 1) = (h2 . x) by A11, A27, A28, A25, FUNCT_1:def 3;

            reconsider nx = x as Element of NAT by A27, A34;

            

             A36: nx <= ( len F) by A11, A34, FINSEQ_1: 1;

            reconsider h2b = ( Swap (h2r,nx,((k + 1) + 1))) as FinSequence of NAT ;

            

             A37: ( rng h2b) = ( rng h2) by FINSEQ_7: 22

            .= ( dom F) by FUNCT_2:def 3;

            

             A38: ( len h2b) = ( len h2r) by FINSEQ_7: 18;

            then ( dom h2b) = ( Seg ( len h2r)) by FINSEQ_1:def 3;

            

            then

             A39: ( dom h2b) = ( dom h2) by FINSEQ_1:def 3

            .= ( dom F) by A15, FUNCT_2:def 1;

            then

            reconsider h2d = h2b as Function of ( dom F), ( dom F) by A37, FUNCT_2: 1;

            

             A40: h2d is one-to-one by INT_5: 39;

            h2d is onto by A37, FUNCT_2:def 3;

            then

            reconsider h4 = h2d as Permutation of ( dom F) by A40;

            

             A41: 1 <= nx by A11, A34, FINSEQ_1: 1;

            then

             A42: (h4 . nx) = (h2r . ((k + 1) + 1)) by A22, A24, A36, A33, Th9;

            

             A43: ( dom h4) = ( dom F) by A5, FUNCT_2:def 1;

            ( rng h4) c= ( dom F);

            

            then

             A44: ( dom (F (*) h4)) = ( dom h4) by RELAT_1: 27

            .= ( dom F) by A5, FUNCT_2:def 1;

            then ( Seg ( len (F (*) h4))) = ( dom F) by FINSEQ_1:def 3;

            then

             A45: ( len (F (*) h4)) = ( len F) by FINSEQ_1:def 3;

            per cases ;

              suppose

               A46: nx <= (k + 1);

              

               A47: ((k + 1) + 1) <= ( len h2r) by A20, A33, NAT_1: 13;

              

               A48: nx <= ( len h2r) by A11, A34, A33, FINSEQ_1: 1;

              

               A49: (F . ((k + 1) + 1)) = ((F (*) h2) . nx) by A34, A35, FUNCT_1: 13;

              

               A50: ( len ( accum (F (*) h4))) = ( len (F (*) h4)) by Def10;

              

               A51: 1 <= nx by A11, A34, FINSEQ_1: 1;

              

               A52: 1 <= ((k + 1) + 1) by NAT_1: 11;

              then

               A53: (h2b . ((k + 1) + 1)) = ((k + 1) + 1) by A35, A51, A48, A47, Th9;

              

               A54: for i be Nat st (k + 1) < i & i <= ( len F) holds (h4 . i) = i

              proof

                let i be Nat;

                assume that

                 A55: (k + 1) < i and

                 A56: i <= ( len F);

                

                 A57: ((k + 1) + 1) <= i by A55, NAT_1: 13;

                per cases ;

                  suppose

                   A58: ((k + 1) + 1) < i;

                  1 <= (k + 1) by NAT_1: 11;

                  then

                   A59: 1 < i by A55, XXREAL_0: 2;

                  

                  then (h4 . i) = (h2b /. i) by A33, A38, A56, FINSEQ_4: 15

                  .= (h2r /. i) by A33, A46, A55, A56, A58, A59, FINSEQ_7: 30

                  .= (h2 . i) by A33, A56, A59, FINSEQ_4: 15

                  .= i by A21, A56, A58;

                  hence (h4 . i) = i;

                end;

                  suppose ((k + 1) + 1) >= i;

                  then i = ((k + 1) + 1) by A57, XXREAL_0: 1;

                  hence (h4 . i) = i by A35, A51, A48, A52, A47, Th9;

                end;

              end;

              

               A60: (F /. ((k + 1) + 1)) = (F . ((k + 1) + 1)) by A22, A24, FINSEQ_4: 15;

              

               A61: 1 <= (k + 1) by NAT_1: 11;

              

               A62: ( len ( accum (F (*) h2))) = ( len (F (*) h2)) by Def10;

              

               A63: nx < ((k + 1) + 1) by A19, A46, XXREAL_0: 2;

              

               A64: for i4 be Nat st 1 <= i4 & i4 < nx holds (( accum (F (*) h2)) . i4) = (( accum (F (*) h4)) . i4)

              proof

                defpred T[ Nat] means (1 + $1) < nx implies (( accum (F (*) h2)) . (1 + $1)) = (( accum (F (*) h4)) . (1 + $1));

                let i4 be Nat;

                assume that

                 A65: 1 <= i4 and

                 A66: i4 < nx;

                

                 A67: (1 + (i4 -' 1)) = ((i4 - 1) + 1) by A65, XREAL_1: 233

                .= i4;

                

                 A68: for k3 be Nat st T[k3] holds T[(k3 + 1)]

                proof

                  let k3 be Nat;

                  

                   A69: 1 <= (k3 + 1) by NAT_1: 11;

                  assume

                   A70: T[k3];

                  (1 + (k3 + 1)) < nx implies (( accum (F (*) h2)) . (1 + (k3 + 1))) = (( accum (F (*) h4)) . (1 + (k3 + 1)))

                  proof

                    assume

                     A71: (1 + (k3 + 1)) < nx;

                    then

                     A72: (1 + (k3 + 1)) < ( len F) by A36, XXREAL_0: 2;

                    then

                     A73: (h2r /. ((k3 + 1) + 1)) = (h2r . ((k3 + 1) + 1)) by A33, FINSEQ_4: 15, NAT_1: 11;

                    

                     A74: ((k3 + 1) + 1) < ((k + 1) + 1) by A63, A71, XXREAL_0: 2;

                    

                     A75: (h2b /. ((k3 + 1) + 1)) = (h2b . ((k3 + 1) + 1)) by A33, A38, A72, FINSEQ_4: 15, NAT_1: 11;

                    1 <= (1 + (k3 + 1)) by NAT_1: 11;

                    then ((k3 + 1) + 1) in ( Seg ( len F)) by A72, FINSEQ_1: 1;

                    then

                     A76: ((k3 + 1) + 1) in ( dom (F (*) h2)) by A29, FINSEQ_1:def 3;

                    

                    then

                     A77: ((F (*) h2) . ((k3 + 1) + 1)) = (F . (h2 . ((k3 + 1) + 1))) by FUNCT_1: 12

                    .= (F . (h4 . ((k3 + 1) + 1))) by A33, A71, A72, A74, A73, A75, FINSEQ_7: 30, NAT_1: 11

                    .= ((F (*) h4) . ((k3 + 1) + 1)) by A44, A29, A76, FUNCT_1: 12;

                    

                     A78: ((F (*) h4) /. ((k3 + 1) + 1)) = ((F (*) h4) . ((k3 + 1) + 1)) by A45, A72, FINSEQ_4: 15, NAT_1: 11;

                    

                     A79: (k3 + 1) < (1 + (k3 + 1)) by XREAL_1: 29;

                    then

                     A80: (k3 + 1) < nx by A71, XXREAL_0: 2;

                    then

                     A81: (k3 + 1) < ( len F) by A36, XXREAL_0: 2;

                    (k3 + 1) < ( len (F (*) h2)) by A36, A32, A80, XXREAL_0: 2;

                    then

                     A82: (( accum (F (*) h4)) /. (1 + k3)) = (( accum (F (*) h4)) . (1 + k3)) by A45, A32, A50, FINSEQ_4: 15, NAT_1: 11;

                    (( accum (F (*) h2)) /. (1 + k3)) = (( accum (F (*) h2)) . (1 + k3)) by A32, A62, A81, FINSEQ_4: 15, NAT_1: 11;

                    

                    then (( accum (F (*) h2)) . (1 + (k3 + 1))) = ((( accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h2) /. ((k3 + 1) + 1))) by A32, A70, A69, A71, A79, A81, A82, Def10, XXREAL_0: 2

                    .= ((( accum (F (*) h4)) /. (k3 + 1)) + ((F (*) h4) /. ((k3 + 1) + 1))) by A32, A72, A77, A78, FINSEQ_4: 15, NAT_1: 11;

                    hence (( accum (F (*) h2)) . (1 + (k3 + 1))) = (( accum (F (*) h4)) . (1 + (k3 + 1))) by A45, A69, A81, Def10;

                  end;

                  hence T[(k3 + 1)];

                end;

                 0 < (k + 1);

                then

                 A83: 1 <> ((k + 1) + 1);

                

                 A84: (h2b /. 1) = (h2b . 1) by A3, A33, A38, FINSEQ_4: 15;

                

                 A85: (h2r /. 1) = (h2r . 1) by A3, A33, FINSEQ_4: 15;

                ((F (*) h2) . 1) = (F . (h2 . 1)) by A5, A29, FUNCT_1: 12

                .= (F . (h4 . 1)) by A3, A33, A65, A66, A83, A85, A84, FINSEQ_7: 30

                .= ((F (*) h4) . 1) by A5, A44, FUNCT_1: 12;

                

                then (( accum (F (*) h2)) . (1 + 0 )) = ((F (*) h4) . 1) by Def10

                .= (( accum (F (*) h4)) . (1 + 0 )) by Def10;

                then

                 A86: T[ 0 ];

                for k3 be Nat holds T[k3] from NAT_1:sch 2( A86, A68);

                hence (( accum (F (*) h2)) . i4) = (( accum (F (*) h4)) . i4) by A66, A67;

              end;

              

               A87: for i be Nat st nx <= i & i < ((k + 1) + 1) holds (( accum (F (*) h2)) . i) = (((( accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx))

              proof

                defpred S[ Nat] means nx <= (nx + $1) & (nx + $1) < ((k + 1) + 1) implies (( accum (F (*) h2)) . (nx + $1)) = (((( accum (F (*) h4)) /. (nx + $1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx));

                let i be Nat;

                assume that

                 A88: nx <= i and

                 A89: i < ((k + 1) + 1);

                

                 A90: ( len ( accum (F (*) h4))) = ( len (F (*) h4)) by Def10;

                

                 A91: ( len ( accum (F (*) h2))) = ( len (F (*) h2)) by Def10;

                

                 A92: for k3 be Nat st S[k3] holds S[(k3 + 1)]

                proof

                  let k3 be Nat;

                  assume

                   A93: S[k3];

                  nx <= (nx + (k3 + 1)) & (nx + (k3 + 1)) < ((k + 1) + 1) implies (( accum (F (*) h2)) . (nx + (k3 + 1))) = (((( accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx))

                  proof

                    reconsider f3 = ((F (*) h2) /. ((nx + k3) + 1)) as Element of ( REAL n);

                    

                     A94: nx <= (nx + k3) by NAT_1: 11;

                    reconsider f2 = ((F (*) h2) /. ((k + 1) + 1)) as Element of ( REAL n);

                    

                     A95: (nx + k3) < ((nx + k3) + 1) by XREAL_1: 29;

                    reconsider f4 = ((F (*) h2) /. nx) as Element of ( REAL n);

                    reconsider f1 = (( accum (F (*) h4)) /. (nx + k3)) as Element of ( REAL n);

                    assume that nx <= (nx + (k3 + 1)) and

                     A96: (nx + (k3 + 1)) < ((k + 1) + 1);

                    

                     A97: (nx + (k3 + 1)) < ( len ( accum (F (*) h4))) by A22, A45, A90, A96, XXREAL_0: 2;

                    

                     A98: (nx + k3) < ((nx + k3) + 1) by XREAL_1: 29;

                    then (nx + k3) < ((k + 1) + 1) by A96, XXREAL_0: 2;

                    then

                     A99: (nx + k3) < ( len (F (*) h2)) by A33, A32, A47, XXREAL_0: 2;

                    then

                     A100: ((nx + k3) + 1) <= ( len (F (*) h2)) by NAT_1: 13;

                    (nx + k3) >= ( 0 + 1) by A41, NAT_1: 13;

                    then

                     A101: 1 < (nx + (k3 + 1)) by A98, XXREAL_0: 2;

                    then

                     A102: ((F (*) h4) /. ((nx + k3) + 1)) = ((F (*) h4) . ((nx + k3) + 1)) by A45, A32, A100, FINSEQ_4: 15;

                    ((nx + k3) + 1) in ( Seg ( len (F (*) h2))) by A101, A100, FINSEQ_1: 1;

                    then

                     A103: ((nx + k3) + 1) in ( dom (F (*) h2)) by FINSEQ_1:def 3;

                    

                    then

                     A104: ((F (*) h4) . ((nx + k3) + 1)) = (F . (h4 . ((nx + k3) + 1))) by A44, A29, FUNCT_1: 12

                    .= (F . (h2b /. ((nx + k3) + 1))) by A33, A38, A32, A101, A100, FINSEQ_4: 15

                    .= (F . (h2r /. ((nx + k3) + 1))) by A33, A32, A96, A101, A100, A95, A94, FINSEQ_7: 30

                    .= (F . (h2r . ((nx + k3) + 1))) by A33, A32, A101, A100, FINSEQ_4: 15

                    .= ((F (*) h2) . ((nx + k3) + 1)) by A103, FUNCT_1: 12;

                    nx <= (nx + k3) by NAT_1: 11;

                    then

                     A105: 1 <= (nx + k3) by A51, XXREAL_0: 2;

                    

                    then (( accum (F (*) h4)) . (nx + (k3 + 1))) = ((( accum (F (*) h4)) /. (nx + k3)) + ((F (*) h4) /. ((nx + k3) + 1))) by A45, A32, A99, Def10

                    .= ((( accum (F (*) h4)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1))) by A101, A100, A104, A102, FINSEQ_4: 15;

                    

                    then

                     A106: (((( accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) = (((f1 + f3) - f2) + f4) by A101, A97, FINSEQ_4: 15

                    .= (((f1 - f2) + f3) + f4) by RFUNCT_1: 8

                    .= (((f1 - f2) + f4) + f3) by RFUNCT_1: 8;

                    (( accum (F (*) h2)) . (nx + (k3 + 1))) = ((( accum (F (*) h2)) /. (nx + k3)) + ((F (*) h2) /. ((nx + k3) + 1))) by A105, A99, Def10

                    .= ((((( accum (F (*) h4)) /. (nx + k3)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((nx + k3) + 1))) by A91, A93, A96, A98, A105, A99, FINSEQ_4: 15, NAT_1: 11, XXREAL_0: 2;

                    hence (( accum (F (*) h2)) . (nx + (k3 + 1))) = (((( accum (F (*) h4)) /. (nx + (k3 + 1))) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) by A106;

                  end;

                  hence S[(k3 + 1)];

                end;

                now

                  per cases by A41, XXREAL_0: 1;

                    case

                     A107: 1 = nx;

                    (( accum (F (*) h4)) /. (nx + 0 )) = (( accum (F (*) h4)) . 1) by A3, A45, A90, A107, FINSEQ_4: 15

                    .= ((F (*) h4) . 1) by Def10

                    .= (F . (h2 . ((k + 1) + 1))) by A5, A43, A42, A107, FUNCT_1: 13

                    .= ((F (*) h2) . ((k + 1) + 1)) by A27, A26, FUNCT_1: 13

                    .= ((F (*) h2) /. ((k + 1) + 1)) by A22, A24, A32, FINSEQ_4: 15;

                    

                    then

                     A108: (((( accum (F (*) h4)) /. (nx + 0 )) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) = (( 0* n) + ((F (*) h2) /. nx)) by EUCLIDLP: 2

                    .= ((F (*) h2) /. nx) by EUCLID_4: 1;

                    (( accum (F (*) h2)) . (nx + 0 )) = ((F (*) h2) . 1) by A107, Def10

                    .= ((F (*) h2) /. nx) by A36, A32, A107, FINSEQ_4: 15;

                    hence (( accum (F (*) h2)) . (nx + 0 )) = (((( accum (F (*) h4)) /. (nx + 0 )) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) by A108;

                  end;

                    case

                     A109: 1 < nx;

                    

                     A110: ((F (*) h4) /. nx) = ((F (*) h4) . nx) by A41, A36, A45, FINSEQ_4: 15

                    .= (F . (h2 . ((k + 1) + 1))) by A34, A43, A42, FUNCT_1: 13

                    .= ((F (*) h2) . ((k + 1) + 1)) by A27, A26, FUNCT_1: 13

                    .= ((F (*) h2) /. ((k + 1) + 1)) by A22, A24, A32, FINSEQ_4: 15;

                    

                     A111: (nx -' 1) = (nx - 1) by A109, XREAL_1: 233;

                    then (nx -' 1) > 0 by A109, XREAL_1: 50;

                    then

                     A112: (nx -' 1) >= ( 0 + 1) by NAT_1: 13;

                    nx < (nx + 1) by XREAL_1: 29;

                    then

                     A113: (nx - 1) < ((nx + 1) - 1) by XREAL_1: 9;

                    then

                     A114: (nx -' 1) < ( len (F (*) h2)) by A33, A32, A48, A111, XXREAL_0: 2;

                    then

                     A115: (( accum (F (*) h2)) /. (nx -' 1)) = (( accum (F (*) h2)) . (nx -' 1)) by A91, A112, FINSEQ_4: 15;

                    (( accum (F (*) h4)) . (nx + 0 )) = ((( accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h4) /. ((nx -' 1) + 1))) by A45, A32, A111, A112, A114, Def10

                    .= ((( accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. ((k + 1) + 1))) by A111, A110;

                    

                    then

                     A116: ((( accum (F (*) h4)) /. (nx + 0 )) - ((F (*) h2) /. ((k + 1) + 1))) = (((( accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. ((k + 1) + 1))) - ((F (*) h2) /. ((k + 1) + 1))) by A33, A45, A51, A48, A90, FINSEQ_4: 15

                    .= (( accum (F (*) h4)) /. (nx -' 1)) by RVSUM_1: 42;

                    

                     A117: (( accum (F (*) h4)) /. (nx -' 1)) = (( accum (F (*) h4)) . (nx -' 1)) by A45, A32, A90, A112, A114, FINSEQ_4: 15;

                    (( accum (F (*) h2)) . (nx + 0 )) = ((( accum (F (*) h2)) /. (nx -' 1)) + ((F (*) h2) /. ((nx -' 1) + 1))) by A111, A112, A114, Def10

                    .= ((( accum (F (*) h4)) /. (nx -' 1)) + ((F (*) h2) /. nx)) by A64, A111, A112, A113, A115, A117;

                    hence (( accum (F (*) h2)) . (nx + 0 )) = (((( accum (F (*) h4)) /. (nx + 0 )) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) by A116;

                  end;

                end;

                then

                 A118: S[ 0 ];

                

                 A119: for k3 be Nat holds S[k3] from NAT_1:sch 2( A118, A92);

                

                 A120: (i -' nx) = (i - nx) by A88, XREAL_1: 233;

                then nx <= (nx + (i -' nx)) by A88;

                hence (( accum (F (*) h2)) . i) = (((( accum (F (*) h4)) /. i) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) by A89, A119, A120;

              end;

              

               A121: ((F (*) h2) /. nx) = ((F (*) h2) . nx) by A41, A36, A32, FINSEQ_4: 15;

              

               A122: ((k + 1) + 1) in ( dom h4) by A25, A39, FINSEQ_1:def 3;

              

               A123: ((F (*) h4) /. ((k + 1) + 1)) = ((F (*) h4) . ((k + 1) + 1)) by A22, A24, A45, FINSEQ_4: 15;

              

               A124: for i be Nat st ((k + 1) + 1) <= i & i <= ( len F) holds (( accum (F (*) h2)) . i) = (( accum (F (*) h4)) . i)

              proof

                defpred Y[ Nat] means (((k + 1) + 1) + $1) <= ( len F) implies (( accum (F (*) h2)) . (((k + 1) + 1) + $1)) = (( accum (F (*) h4)) . (((k + 1) + 1) + $1));

                let i be Nat;

                assume that

                 A125: ((k + 1) + 1) <= i and

                 A126: i <= ( len F);

                

                 A127: for k3 be Nat st Y[k3] holds Y[(k3 + 1)]

                proof

                  let k3 be Nat;

                  assume

                   A128: Y[k3];

                  (((k + 1) + 1) + (k3 + 1)) <= ( len F) implies (( accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1))) = (( accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1)))

                  proof

                    

                     A129: ((k + 1) + 1) <= (((k + 1) + 1) + k3) by NAT_1: 11;

                    

                     A130: (((k + 1) + 1) + k3) < ((((k + 1) + 1) + k3) + 1) by XREAL_1: 29;

                    then

                     A131: ((k + 1) + 1) < ((((k + 1) + 1) + k3) + 1) by A129, XXREAL_0: 2;

                    assume

                     A132: (((k + 1) + 1) + (k3 + 1)) <= ( len F);

                    then

                     A133: ((F (*) h4) /. ((((k + 1) + 1) + k3) + 1)) = ((F (*) h4) . ((((k + 1) + 1) + k3) + 1)) by A45, FINSEQ_4: 15, NAT_1: 11;

                    1 <= ((((k + 1) + 1) + k3) + 1) by NAT_1: 11;

                    then ((((k + 1) + 1) + k3) + 1) in ( Seg ( len (F (*) h2))) by A31, A132, FINSEQ_1: 1;

                    then

                     A134: ((((k + 1) + 1) + k3) + 1) in ( dom (F (*) h2)) by FINSEQ_1:def 3;

                    

                    then

                     A135: ((F (*) h4) . ((((k + 1) + 1) + k3) + 1)) = (F . (h4 . ((((k + 1) + 1) + k3) + 1))) by A44, A29, FUNCT_1: 12

                    .= (F . (h2b /. ((((k + 1) + 1) + k3) + 1))) by A33, A38, A132, FINSEQ_4: 15, NAT_1: 11

                    .= (F . (h2r /. ((((k + 1) + 1) + k3) + 1))) by A33, A63, A132, A131, FINSEQ_7: 30, NAT_1: 11

                    .= (F . (h2r . ((((k + 1) + 1) + k3) + 1))) by A33, A132, FINSEQ_4: 15, NAT_1: 11

                    .= ((F (*) h2) . ((((k + 1) + 1) + k3) + 1)) by A134, FUNCT_1: 12;

                    1 <= ((k + 1) + 1) by NAT_1: 11;

                    then

                     A136: 1 <= (((k + 1) + 1) + k3) by A129, XXREAL_0: 2;

                    

                     A137: (((k + 1) + 1) + k3) < ( len F) by A132, A130, XXREAL_0: 2;

                    then

                     A138: (( accum (F (*) h4)) /. (((k + 1) + 1) + k3)) = (( accum (F (*) h4)) . (((k + 1) + 1) + k3)) by A45, A50, A136, FINSEQ_4: 15;

                    (( accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1))) = ((( accum (F (*) h2)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1))) by A32, A137, A136, Def10

                    .= ((( accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h2) /. ((((k + 1) + 1) + k3) + 1))) by A32, A62, A128, A137, A136, A138, FINSEQ_4: 15

                    .= ((( accum (F (*) h4)) /. (((k + 1) + 1) + k3)) + ((F (*) h4) /. ((((k + 1) + 1) + k3) + 1))) by A32, A132, A135, A133, FINSEQ_4: 15, NAT_1: 11;

                    hence (( accum (F (*) h2)) . (((k + 1) + 1) + (k3 + 1))) = (( accum (F (*) h4)) . (((k + 1) + 1) + (k3 + 1))) by A45, A137, A136, Def10;

                  end;

                  hence Y[(k3 + 1)];

                end;

                

                 A139: ( len ( accum (F (*) h2))) = ( len (F (*) h2)) by Def10;

                

                 A140: (( accum (F (*) h2)) . (k + 1)) = (((( accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) by A19, A46, A87;

                

                 A141: 1 <= (k + 1) by NAT_1: 11;

                (k + 1) < ( len (F (*) h2)) by A20, A30, FINSEQ_1:def 3;

                

                then (( accum (F (*) h2)) . ((k + 1) + 1)) = ((( accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1))) by A141, Def10

                .= ((((( accum (F (*) h4)) /. (k + 1)) - ((F (*) h2) /. ((k + 1) + 1))) + ((F (*) h2) /. nx)) + ((F (*) h2) /. ((k + 1) + 1))) by A20, A32, A139, A140, FINSEQ_4: 15, NAT_1: 11

                .= ((( accum (F (*) h4)) /. (k + 1)) + ((F (*) h2) /. nx)) by Th4

                .= ((( accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1))) by A122, A53, A49, A123, A121, FUNCT_1: 13;

                then

                 A142: Y[ 0 ] by A20, A18, A45, Def10;

                

                 A143: for k3 be Nat holds Y[k3] from NAT_1:sch 2( A142, A127);

                (((k + 1) + 1) + (i -' ((k + 1) + 1))) = ((i - ((k + 1) + 1)) + ((k + 1) + 1)) by A125, XREAL_1: 233

                .= i;

                hence (( accum (F (*) h2)) . i) = (( accum (F (*) h4)) . i) by A126, A143;

              end;

              

               A144: (gF /. (k + 1)) = (gF . (k + 1)) by A9, A20, FINSEQ_4: 15, NAT_1: 11;

              

               A145: ( dom h4) = ( dom F) by A5, FUNCT_2:def 1;

              ( rng h4) c= ( dom F);

              then

               A146: ( dom (F (*) h4)) = ( dom h4) by RELAT_1: 27;

              then ( Seg ( len (F (*) h4))) = ( dom h4) by FINSEQ_1:def 3;

              then

               A147: (k + 1) < ( len (F (*) h4)) by A20, A145, FINSEQ_1:def 3;

              ( Seg ( len (F (*) h4))) = ( dom F) by A145, A146, FINSEQ_1:def 3;

              then ( len (F (*) h4)) = ( len F) by FINSEQ_1:def 3;

              then

               A148: ((F (*) h4) /. ((k + 1) + 1)) = ((F (*) h4) . ((k + 1) + 1)) by A22, A24, FINSEQ_4: 15;

              ( len ( accum (F (*) h4))) = ( len (F (*) h4)) by Def10;

              then

               A149: (( accum (F (*) h4)) /. (k + 1)) = (( accum (F (*) h4)) . (k + 1)) by A147, FINSEQ_4: 15, NAT_1: 11;

              (gF . ((k + 1) + 1)) = ((gF /. (k + 1)) + (F /. ((k + 1) + 1))) by A10, A20, NAT_1: 11

              .= ((( accum (F (*) h4)) /. (k + 1)) + (F /. ((k + 1) + 1))) by A17, A23, A54, A149, A144

              .= ((( accum (F (*) h4)) /. (k + 1)) + ((F (*) h4) /. ((k + 1) + 1))) by A122, A53, A148, A60, FUNCT_1: 13

              .= (( accum (F (*) h4)) . ((k + 1) + 1)) by A61, A147, Def10;

              hence (gF . ((k + 1) + 1)) = (( accum (F (*) h2)) . ((k + 1) + 1)) by A22, A124;

            end;

              suppose nx > (k + 1);

              then

               A150: ((k + 1) + 1) <= nx by NAT_1: 13;

              per cases by A150, XXREAL_0: 1;

                suppose

                 A151: ((k + 1) + 1) = nx;

                

                 A152: for i be Nat st (k + 1) < i & i <= ( len F) holds (h2 . i) = i

                proof

                  let i be Nat;

                  assume that

                   A153: (k + 1) < i and

                   A154: i <= ( len F);

                  

                   A155: ((k + 1) + 1) <= i by A153, NAT_1: 13;

                  per cases by A155, XXREAL_0: 1;

                    suppose ((k + 1) + 1) < i;

                    hence (h2 . i) = i by A21, A154;

                  end;

                    suppose ((k + 1) + 1) = i;

                    hence (h2 . i) = i by A35, A151;

                  end;

                end;

                

                 A156: (k + 1) < ( len (F (*) h2)) by A20, A30, FINSEQ_1:def 3;

                ( len ( accum (F (*) h2))) = ( len (F (*) h2)) by Def10;

                then

                 A157: (( accum (F (*) h2)) /. (k + 1)) = (( accum (F (*) h2)) . (k + 1)) by A20, A32, FINSEQ_4: 15, NAT_1: 11;

                

                 A158: 1 <= (k + 1) by NAT_1: 11;

                

                 A159: (F . ((k + 1) + 1)) = ((F (*) h2) . nx) by A34, A35, FUNCT_1: 13;

                

                 A160: (gF /. (k + 1)) = (gF . (k + 1)) by A9, A20, FINSEQ_4: 15, NAT_1: 11;

                

                 A161: (F /. ((k + 1) + 1)) = (F . ((k + 1) + 1)) by A22, A24, FINSEQ_4: 15;

                (gF . ((k + 1) + 1)) = ((gF /. (k + 1)) + (F /. ((k + 1) + 1))) by A10, A20, NAT_1: 11

                .= ((( accum (F (*) h2)) /. (k + 1)) + (F /. ((k + 1) + 1))) by A17, A23, A152, A157, A160

                .= ((( accum (F (*) h2)) /. (k + 1)) + ((F (*) h2) /. ((k + 1) + 1))) by A22, A24, A32, A151, A161, A159, FINSEQ_4: 15

                .= (( accum (F (*) h2)) . ((k + 1) + 1)) by A158, A156, Def10;

                hence (gF . ((k + 1) + 1)) = (( accum (F (*) h2)) . ((k + 1) + 1));

              end;

                suppose ((k + 1) + 1) < nx;

                hence (gF . ((k + 1) + 1)) = (( accum (F (*) h2)) . ((k + 1) + 1)) by A21, A35, A36;

              end;

            end;

          end;

          hence P[(k + 1)];

        end;

        for h2 be Permutation of ( dom F) st for i be Nat st ( 0 + 1) < i & i <= ( len F) holds (h2 . i) = i holds (gF . ( 0 + 1)) = (( accum (F (*) h2)) . ( 0 + 1))

        proof

          let h2 be Permutation of ( dom F);

          

           A162: ( rng h2) = ( dom F) by FUNCT_2:def 3;

          

           A163: ( dom h2) = ( dom F) by A5, FUNCT_2:def 1;

          assume

           A164: for i be Nat st ( 0 + 1) < i & i <= ( len F) holds (h2 . i) = i;

           A165:

          now

            assume

             A166: (h2 . 1) <> 1;

            consider x be object such that

             A167: x in ( dom h2) and

             A168: (h2 . x) = 1 by A5, A162, FUNCT_1:def 3;

            reconsider nx = x as Element of NAT by A163, A167;

            1 <= nx by A11, A167, FINSEQ_1: 1;

            then nx = 1 or 1 < nx & nx <= ( len F) by A11, A167, FINSEQ_1: 1, XXREAL_0: 1;

            hence contradiction by A164, A166, A168;

          end;

          (( accum (F (*) h2)) . 1) = ((F (*) h2) . 1) by Def10

          .= (F . 1) by A5, A163, A165, FUNCT_1: 13;

          hence (gF . ( 0 + 1)) = (( accum (F (*) h2)) . ( 0 + 1)) by Def10;

        end;

        then

         A169: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A169, A16);

        

        then (gF . ( len F)) = (( accum (F (*) h)) . ( len F)) by A13, A14, XREAL_1: 44

        .= (( accum F2) . ( len F2)) by A1, A8, FINSEQ_1:def 3

        .= ( Sum F2) by A12, Def11;

        hence ( Sum F2) = ( Sum F) by A2, Def11;

      end;

        suppose

         A170: ( len F) <= 0 ;

        ( rng h) c= ( dom F);

        then

         A171: ( dom (F (*) h)) = ( dom h) by RELAT_1: 27;

        ( Seg ( len F)) = {} by A170;

        then ( dom F) = {} by FINSEQ_1:def 3;

        then ( Seg ( len F)) = ( dom F2) by A1, A171, FINSEQ_1:def 3;

        then

         A172: ( len F) = ( len F2) by FINSEQ_1:def 3;

        ( Sum F) = ( 0* n) by A170, Def11;

        hence ( Sum F2) = ( Sum F) by A170, A172, Def11;

      end;

    end;

    theorem :: EUCLID_7:22

    

     Th21: for k be Element of NAT holds ( Sum (k |-> ( 0* n))) = ( 0* n)

    proof

      let k be Element of NAT ;

      set g = (k |-> ( 0* n));

      

       A1: for i be Nat st i in ( dom g) holds (g . i) = ( 0* n)

      proof

        let i be Nat;

        assume i in ( dom g);

        then i in ( Seg k) by FUNCOP_1: 13;

        hence thesis by FINSEQ_2: 57;

      end;

      per cases ;

        suppose

         A2: ( len g) > 0 ;

        set g3 = ( accum g);

        

         A3: ( len g) = ( len g3) by Def10;

        

         A4: (g . 1) = (g3 . 1) by Def10;

        defpred P[ Nat] means $1 < ( len g) implies (g3 . ($1 + 1)) = ( 0* n);

        

         A5: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A6: P[k];

          

           A7: k < (k + 1) by XREAL_1: 29;

          per cases ;

            suppose

             A8: (k + 1) < ( len g);

            then

             A9: ((k + 1) + 1) <= ( len g) by NAT_1: 13;

            per cases ;

              suppose

               A10: 1 <= (k + 1);

              

               A11: 1 <= ((k + 1) + 1) by XREAL_1: 29;

              then ((k + 1) + 1) in ( Seg ( len g)) by A9, FINSEQ_1: 1;

              then ((k + 1) + 1) in ( dom g) by FINSEQ_1:def 3;

              then

               A12: (g . ((k + 1) + 1)) = ( 0* n) by A1;

              

               A13: (g3 /. (k + 1)) = (g3 . (k + 1)) by A3, A8, A10, FINSEQ_4: 15;

              (g3 . ((k + 1) + 1)) = ((g3 /. (k + 1)) + (g /. ((k + 1) + 1))) by Def10, A8, A10;

              

              then (g3 . ((k + 1) + 1)) = (( 0* n) + ( 0* n)) by A6, A7, A8, A9, A13, A11, A12, FINSEQ_4: 15, XXREAL_0: 2

              .= ( 0* n) by EUCLID_4: 1;

              hence P[(k + 1)];

            end;

              suppose 1 > (k + 1);

              hence P[(k + 1)] by NAT_1: 14;

            end;

          end;

            suppose (k + 1) >= ( len g);

            hence P[(k + 1)];

          end;

        end;

        

         A14: ( 0 + 1) <= ( len g) by A2, NAT_1: 13;

        then 1 in ( Seg ( len g)) by FINSEQ_1: 1;

        then 1 in ( dom g) by FINSEQ_1:def 3;

        then

         A15: P[ 0 ] by A1, A4;

        for k be Nat holds P[k] from NAT_1:sch 2( A15, A5);

        then

         A16: P[(( len g3) -' 1)];

        (( len g3) -' 1) = (( len g3) - 1) by A3, A14, XREAL_1: 233;

        hence ( Sum g) = ( 0* n) by A3, Def11, A16, XREAL_1: 44;

      end;

        suppose ( len g) <= 0 ;

        hence ( Sum g) = ( 0* n) by Def11;

      end;

    end;

    theorem :: EUCLID_7:23

    

     Th22: for g be FinSequence of ( REAL n), h be FinSequence of NAT , F be FinSequence of ( REAL n) st h is increasing & ( rng h) c= ( dom g) & F = (g * h) & (for i be Element of NAT st i in ( dom g) & not i in ( rng h) holds (g . i) = ( 0* n)) holds ( Sum g) = ( Sum F)

    proof

      let g be FinSequence of ( REAL n), h be FinSequence of NAT , F be FinSequence of ( REAL n);

      assume that

       A1: h is increasing and

       A2: ( rng h) c= ( dom g) and

       A3: F = (g * h) and

       A4: for i be Element of NAT st i in ( dom g) & not i in ( rng h) holds (g . i) = ( 0* n);

      

       A5: ( dom (h qua Relation * g qua Relation)) = ( dom h) by A2, RELAT_1: 27;

      ( dom (g * h)) = ( dom h) by A2, RELAT_1: 27;

      then

       A6: ( dom F) = ( Seg ( len h)) by A3, FINSEQ_1:def 3;

      then

       A7: ( len F) = ( len h) by FINSEQ_1:def 3;

      ( dom h) c= ( dom g)

      proof

        let x be object;

        assume

         A8: x in ( dom h);

        then

        reconsider nx = x as Element of NAT ;

        

         A9: (h . x) in ( rng h) by A8, FUNCT_1:def 3;

        then

        reconsider nhx = (h . x) as Element of NAT ;

        

         A10: nx in ( Seg ( len h)) by A8, FINSEQ_1:def 3;

        then

         A11: 1 <= nx by FINSEQ_1: 1;

        

         A12: nx <= ( len h) by A10, FINSEQ_1: 1;

        then 1 <= ( len h) by A11, XXREAL_0: 2;

        then 1 in ( Seg ( len h)) by FINSEQ_1: 1;

        then 1 in ( dom h) by FINSEQ_1:def 3;

        then (h . 1) in ( rng h) by FUNCT_1:def 3;

        then (h . 1) in ( dom g) by A2;

        then (h . 1) in ( Seg ( len g)) by FINSEQ_1:def 3;

        then 1 <= (h . 1) by FINSEQ_1: 1;

        then

         A13: nx <= nhx by A1, A12, Th7;

        (h . x) in ( dom g) by A2, A9;

        then (h . x) in ( Seg ( len g)) by FINSEQ_1:def 3;

        then nhx <= ( len g) by FINSEQ_1: 1;

        then nx <= ( len g) by A13, XXREAL_0: 2;

        then nx in ( Seg ( len g)) by A11, FINSEQ_1: 1;

        hence x in ( dom g) by FINSEQ_1:def 3;

      end;

      then ( dom h) c= ( Seg ( len g)) by FINSEQ_1:def 3;

      then ( Seg ( len h)) c= ( Seg ( len g)) by FINSEQ_1:def 3;

      then

       A14: ( len h) <= ( len g) by FINSEQ_1: 5;

      per cases ;

        suppose

         A15: ( len F) > 0 ;

        then

         A16: ( 0 + 1) <= ( len F) by NAT_1: 13;

        then 1 in ( Seg ( len F)) by FINSEQ_1: 1;

        then

         A17: 1 in ( dom F) by FINSEQ_1:def 3;

        then

         A18: 1 in ( Seg ( len h)) by A3, A5, FINSEQ_1:def 3;

        then

         A19: 1 <= ( len h) by FINSEQ_1: 1;

        then ( len h) in ( Seg ( len h)) by FINSEQ_1: 1;

        then ( len h) in ( dom h) by FINSEQ_1:def 3;

        then (h . ( len h)) in ( rng h) by FUNCT_1:def 3;

        then (h . ( len h)) in ( dom g) by A2;

        then

         A20: (h . ( len h)) in ( Seg ( len g)) by FINSEQ_1:def 3;

        reconsider j = (h . 1) as Nat;

        ( dom (h qua Relation * g qua Relation)) = ( dom h) by A2, RELAT_1: 27;

        then

         A21: ( Seg ( len F)) = ( dom h) by A3, FINSEQ_1:def 3;

        then

         A22: ( len F) = ( len h) by FINSEQ_1:def 3;

        

         A23: (h . 1) in ( rng h) by A3, A5, A17, FUNCT_1:def 3;

        then

         A24: (h . 1) in ( dom g) by A2;

        then

         A25: (h . 1) in ( Seg ( len g)) by FINSEQ_1:def 3;

        then

         A26: 1 <= (h . 1) by FINSEQ_1: 1;

        then

         A27: (j -' 1) = (j - 1) by XREAL_1: 233;

        ( Seg ( len g)) <> {} by A2, A23, FINSEQ_1:def 3;

        then 0 < ( len g);

        then

         A28: ( 0 + 1) <= ( len g) by NAT_1: 13;

        then

         A29: (( len g) -' 1) = (( len g) - 1) by XREAL_1: 233;

        then

         A30: (h . ( len h)) <= ((( len g) -' 1) + 1) by A20, FINSEQ_1: 1;

        

         A31: 1 <= j by A25, FINSEQ_1: 1;

        set g4 = ( accum g);

        

         A32: ( len g) = ( len g4) by Def10;

        

         A33: (g . 1) = (g4 . 1) by Def10;

        

         A34: for i be Nat st 1 <= i & i < ( len g) holds (g4 . (i + 1)) = ((g4 /. i) + (g /. (i + 1))) by Def10;

        

         A35: ( Sum g) = (g4 . ( len g)) by A7, A14, A15, Def11;

        set g2 = ( accum F);

        

         A36: ( len F) = ( len g2) by Def10;

        

         A37: (F . 1) = (g2 . 1) by Def10;

        

         A38: for i be Nat st 1 <= i & i < ( len F) holds (g2 . (i + 1)) = ((g2 /. i) + (F /. (i + 1))) by Def10;

        

         A39: ( Sum F) = (g2 . ( len F)) by A15, Def11;

        defpred Q[ Nat] means 1 <= ($1 + 1) & ($1 + 1) < j implies (g4 . ($1 + 1)) = ( 0* n);

        

         A40: for k be Nat st Q[k] holds Q[(k + 1)]

        proof

          let k be Nat;

          assume

           A41: Q[k];

          1 <= ((k + 1) + 1) & ((k + 1) + 1) < j implies (g4 . ((k + 1) + 1)) = ( 0* n)

          proof

            assume that

             A42: 1 <= ((k + 1) + 1) and

             A43: ((k + 1) + 1) < j;

            per cases by A42, XXREAL_0: 1;

              suppose

               A44: 1 < ((k + 1) + 1);

              j in ( Seg ( len g)) by A24, FINSEQ_1:def 3;

              then

               A45: j <= ( len g) by FINSEQ_1: 1;

              then ((k + 1) + 1) < ( len g) by A43, XXREAL_0: 2;

              then

               A46: (g /. ((k + 1) + 1)) = (g . ((k + 1) + 1)) by A44, FINSEQ_4: 15;

               A47:

              now

                assume ((k + 1) + 1) in ( rng h);

                then

                consider x0 be object such that

                 A48: x0 in ( dom h) and

                 A49: (h . x0) = ((k + 1) + 1) by FUNCT_1:def 3;

                reconsider nx0 = x0 as Element of NAT by A48;

                

                 A50: x0 in ( Seg ( len h)) by A48, FINSEQ_1:def 3;

                then

                 A51: nx0 <= ( len h) by FINSEQ_1: 1;

                1 <= nx0 by A50, FINSEQ_1: 1;

                hence contradiction by A1, A43, A49, A51, Th6;

              end;

              

               A52: (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

              then (k + 1) < j by A43, XXREAL_0: 2;

              then

               A53: (k + 1) < ( len g) by A45, XXREAL_0: 2;

              then

               A54: (g4 /. (k + 1)) = (g4 . (k + 1)) by A32, FINSEQ_4: 15, NAT_1: 11;

              ((k + 1) + 1) <= ( len g) by A53, NAT_1: 13;

              then ((k + 1) + 1) in ( Seg ( len g)) by A42, FINSEQ_1: 1;

              then ((k + 1) + 1) in ( dom g) by FINSEQ_1:def 3;

              then

               A55: (g . ((k + 1) + 1)) = ( 0* n) by A4, A47;

              (g4 . ((k + 1) + 1)) = ((g4 /. (k + 1)) + (g /. ((k + 1) + 1))) by A34, A53, NAT_1: 11;

              hence (g4 . ((k + 1) + 1)) = ( 0* n) by A41, A43, A52, A55, A54, A46, EUCLID_4: 1, NAT_1: 11, XXREAL_0: 2;

            end;

              suppose 1 = ((k + 1) + 1);

              hence (g4 . ((k + 1) + 1)) = ( 0* n);

            end;

          end;

          hence Q[(k + 1)];

        end;

        defpred P[ Nat] means 1 <= ($1 + 1) & ($1 + 1) <= ( len g2) implies (g4 . (h . ($1 + 1))) = (g2 . ($1 + 1));

        

         A56: 1 in ( Seg ( len g)) by A28, FINSEQ_1: 1;

        1 < j implies 1 in ( dom g) & not 1 in ( rng h)

        proof

          assume

           A57: 1 < j;

          thus 1 in ( dom g) by A56, FINSEQ_1:def 3;

          hereby

            assume 1 in ( rng h);

            then

            consider x0 be object such that

             A58: x0 in ( dom h) and

             A59: (h . x0) = 1 by FUNCT_1:def 3;

            reconsider nx0 = x0 as Element of NAT by A58;

            

             A60: x0 in ( Seg ( len h)) by A58, FINSEQ_1:def 3;

            then

             A61: nx0 <= ( len h) by FINSEQ_1: 1;

            1 <= nx0 by A60, FINSEQ_1: 1;

            hence contradiction by A1, A57, A59, A61, Th6;

          end;

        end;

        then

         A62: Q[ 0 ] by A4, A33;

        

         A63: for k be Nat holds Q[k] from NAT_1:sch 2( A62, A40);

         A64:

        now

          per cases by A26, XXREAL_0: 1;

            case 1 < j;

            then (1 + 1) <= j by NAT_1: 13;

            then

             A65: ((1 + 1) - 1) <= (j - 1) by XREAL_1: 9;

            then 1 <= (j -' 1) by A31, XREAL_1: 233;

            

            then

             A66: (((j -' 1) -' 1) + 1) = (((j -' 1) - 1) + 1) by XREAL_1: 233

            .= (j -' 1);

            

             A67: (g . j) = (g2 . 1) by A3, A5, A37, A17, FUNCT_1: 13;

            

             A68: Q[((j -' 1) -' 1)] by A63;

            

             A69: j in ( Seg ( len g)) by A24, FINSEQ_1:def 3;

            then

             A70: j <= ( len g) by FINSEQ_1: 1;

            1 <= j by A69, FINSEQ_1: 1;

            then

             A71: (g /. j) = (g . j) by A70, FINSEQ_4: 15;

            

             A72: (g2 /. 1) = (g2 . 1) by A36, A16, FINSEQ_4: 15;

            

             A73: (j -' 1) < ((j -' 1) + 1) by XREAL_1: 29;

            then

             A74: (j -' 1) < ( len g) by A27, A70, XXREAL_0: 2;

            then (g4 /. (j -' 1)) = (g4 . (j -' 1)) by A32, A27, A65, FINSEQ_4: 15;

            

            then (g4 . j) = (( 0* n) + (g2 /. 1)) by Def10, A27, A65, A73, A74, A68, A66, A71, A72, A67

            .= (g2 /. 1) by EUCLID_4: 1;

            hence P[ 0 ] by FINSEQ_4: 15;

          end;

            case j = 1;

            hence P[ 0 ] by A3, A5, A37, A33, A17, FUNCT_1: 13;

          end;

        end;

        

         A75: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat;

          assume

           A76: P[k];

          1 <= ((k + 1) + 1) & ((k + 1) + 1) <= ( len g2) implies (g4 . (h . ((k + 1) + 1))) = (g2 . ((k + 1) + 1))

          proof

            defpred R[ Nat] means (h . (k + 1)) <= ($1 + 1) & ($1 + 1) < (h . ((k + 1) + 1)) implies (g4 . ($1 + 1)) = (g2 . (k + 1));

            assume that

             A77: 1 <= ((k + 1) + 1) and

             A78: ((k + 1) + 1) <= ( len g2);

            

             A79: ((k + 1) + 1) in ( Seg ( len g2)) by A77, A78, FINSEQ_1: 1;

            then (h . ((k + 1) + 1)) in ( rng h) by A36, A21, FUNCT_1:def 3;

            then (h . ((k + 1) + 1)) in ( dom g) by A2;

            then

             A80: (h . ((k + 1) + 1)) in ( Seg ( len g)) by FINSEQ_1:def 3;

            then

             A81: 1 <= (h . ((k + 1) + 1)) by FINSEQ_1: 1;

            

             A82: (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

            then

             A83: (k + 1) < ( len g2) by A78, XXREAL_0: 2;

            now

              per cases ;

                case

                 A84: 1 <= k;

                k < (k + 1) by XREAL_1: 29;

                then

                 A85: k < ( len h) by A36, A22, A83, XXREAL_0: 2;

                then k <= (h . k) by A1, A26, Th7;

                then

                 A86: 1 <= (h . k) by A84, XXREAL_0: 2;

                (h . k) < (h . (k + 1)) by A1, A84, A85;

                hence R[ 0 ] by A86, XXREAL_0: 2;

              end;

                case k < 1;

                hence R[ 0 ] by A15, A36, A64, NAT_1: 14;

              end;

            end;

            then

             A87: R[ 0 ];

            

             A88: (h . ((k + 1) + 1)) <= ( len g) by A80, FINSEQ_1: 1;

            1 <= (k + 1) by NAT_1: 11;

            then

             A89: (h . (k + 1)) < (h . ((k + 1) + 1)) by A1, A36, A22, A83;

            

             A90: for k2 be Nat st R[k2] holds R[(k2 + 1)]

            proof

              let k2 be Nat;

              assume

               A91: R[k2];

              (h . (k + 1)) <= ((k2 + 1) + 1) & ((k2 + 1) + 1) < (h . ((k + 1) + 1)) implies (g4 . ((k2 + 1) + 1)) = (g2 . (k + 1))

              proof

                assume that

                 A92: (h . (k + 1)) <= ((k2 + 1) + 1) and

                 A93: ((k2 + 1) + 1) < (h . ((k + 1) + 1));

                per cases by A92, XXREAL_0: 1;

                  suppose

                   A94: (h . (k + 1)) < ((k2 + 1) + 1);

                   A95:

                  now

                    assume ((k2 + 1) + 1) in ( rng h);

                    then

                    consider x0 be object such that

                     A96: x0 in ( dom h) and

                     A97: (h . x0) = ((k2 + 1) + 1) by FUNCT_1:def 3;

                    reconsider nx0 = x0 as Element of NAT by A96;

                    

                     A98: x0 in ( Seg ( len h)) by A96, FINSEQ_1:def 3;

                    then nx0 <= ( len h) by FINSEQ_1: 1;

                    then

                     A99: nx0 >= ((k + 1) + 1) implies (h . nx0) >= (h . ((k + 1) + 1)) by A1, A77, Th6;

                    1 <= nx0 by A98, FINSEQ_1: 1;

                    then nx0 <= (k + 1) implies (h . nx0) <= (h . (k + 1)) by A1, A36, A22, A83, Th6;

                    hence contradiction by A93, A94, A97, A99, NAT_1: 13;

                  end;

                  (h . ((k + 1) + 1)) in ( rng h) by A36, A21, A79, FUNCT_1:def 3;

                  then (h . ((k + 1) + 1)) in ( dom g) by A2;

                  then (h . ((k + 1) + 1)) in ( Seg ( len g)) by FINSEQ_1:def 3;

                  then (h . ((k + 1) + 1)) <= ( len g) by FINSEQ_1: 1;

                  then

                   A100: ((k2 + 1) + 1) < ( len g) by A93, XXREAL_0: 2;

                  

                   A101: 1 < ((k2 + 1) + 1) by XREAL_1: 29;

                  then

                   A102: (g /. ((k2 + 1) + 1)) = (g . ((k2 + 1) + 1)) by A100, FINSEQ_4: 15;

                  

                   A103: (k2 + 1) < ((k2 + 1) + 1) by XREAL_1: 29;

                  then

                   A104: (k2 + 1) < ( len g) by A100, XXREAL_0: 2;

                  ((k2 + 1) + 1) in ( Seg ( len g)) by A100, A101, FINSEQ_1: 1;

                  then ((k2 + 1) + 1) in ( dom g) by FINSEQ_1:def 3;

                  then

                   A105: (g . ((k2 + 1) + 1)) = ( 0* n) by A4, A95;

                  (k2 + 1) < ( len g) by A103, A100, XXREAL_0: 2;

                  

                  then (g4 . ((k2 + 1) + 1)) = ((g4 /. (k2 + 1)) + (g /. ((k2 + 1) + 1))) by A34, NAT_1: 11

                  .= (g4 /. (k2 + 1)) by A105, A102, EUCLID_4: 1

                  .= (g4 . (k2 + 1)) by A32, A104, FINSEQ_4: 15, NAT_1: 11;

                  hence (g4 . ((k2 + 1) + 1)) = (g2 . (k + 1)) by A91, A93, A94, NAT_1: 13;

                end;

                  suppose (h . (k + 1)) = ((k2 + 1) + 1);

                  hence (g4 . ((k2 + 1) + 1)) = (g2 . (k + 1)) by A76, A78, A82, NAT_1: 11, XXREAL_0: 2;

                end;

              end;

              hence R[(k2 + 1)];

            end;

            

             A106: for k2 be Nat holds R[k2] from NAT_1:sch 2( A87, A90);

            then

             A107: (h . (k + 1)) <= ((((h . ((k + 1) + 1)) -' 1) -' 1) + 1) & ((((h . ((k + 1) + 1)) -' 1) -' 1) + 1) < (h . ((k + 1) + 1)) implies (g4 . ((((h . ((k + 1) + 1)) -' 1) -' 1) + 1)) = (g2 . (k + 1));

            now

              per cases ;

                case

                 A108: 1 <= k;

                k < (k + 1) by XREAL_1: 29;

                then

                 A109: k < ( len h) by A36, A22, A83, XXREAL_0: 2;

                then k <= (h . k) by A1, A26, Th7;

                then

                 A110: 1 <= (h . k) by A108, XXREAL_0: 2;

                

                 A111: (1 + (h . (k + 1))) <= (h . ((k + 1) + 1)) by A89, NAT_1: 13;

                then

                 A112: (((h . (k + 1)) + 1) - 1) <= ((h . ((k + 1) + 1)) - 1) by XREAL_1: 9;

                (h . k) < (h . (k + 1)) by A1, A108, A109;

                then 1 < (h . (k + 1)) by A110, XXREAL_0: 2;

                then (1 + 1) < ((h . (k + 1)) + 1) by XREAL_1: 6;

                then (1 + 1) < (h . ((k + 1) + 1)) by A111, XXREAL_0: 2;

                then

                 A113: ((1 + 1) - 1) < ((h . ((k + 1) + 1)) - 1) by XREAL_1: 9;

                then

                 A114: ((h . ((k + 1) + 1)) -' 1) = ((h . ((k + 1) + 1)) - 1) by XREAL_0:def 2;

                then

                 A115: (((h . ((k + 1) + 1)) -' 1) -' 1) = (((h . ((k + 1) + 1)) - 1) - 1) by A113, XREAL_1: 233;

                

                 A116: (g /. (h . ((k + 1) + 1))) = (g . (h . ((k + 1) + 1))) by A81, A88, FINSEQ_4: 15;

                

                 A117: (F . ((k + 1) + 1)) = (g . (h . ((k + 1) + 1))) by A3, A36, A21, A79, FUNCT_1: 13;

                

                 A118: (k + 1) <= ( len g2) by A78, A82, XXREAL_0: 2;

                (h . ((k + 1) + 1)) < ((h . ((k + 1) + 1)) + 1) by XREAL_1: 29;

                then

                 A119: ((h . ((k + 1) + 1)) - 1) < (((h . ((k + 1) + 1)) + 1) - 1) by XREAL_1: 9;

                then

                 A120: ((h . ((k + 1) + 1)) -' 1) < ( len g) by A88, A114, XXREAL_0: 2;

                then

                 A121: (g4 /. ((h . ((k + 1) + 1)) -' 1)) = (g4 . ((h . ((k + 1) + 1)) -' 1)) by A32, A113, A114, FINSEQ_4: 15;

                (g2 . ((k + 1) + 1)) = ((g2 /. (k + 1)) + (F /. ((k + 1) + 1))) by A36, A38, A83, NAT_1: 11

                .= ((g4 /. ((h . ((k + 1) + 1)) -' 1)) + (F /. ((k + 1) + 1))) by A107, A114, A115, A112, A119, A121, A118, FINSEQ_4: 15, NAT_1: 11

                .= ((g4 /. ((h . ((k + 1) + 1)) -' 1)) + (g /. (h . ((k + 1) + 1)))) by A36, A77, A78, A117, A116, FINSEQ_4: 15

                .= (g4 . (((h . ((k + 1) + 1)) -' 1) + 1)) by Def10, A113, A114, A120;

                hence (g4 . (h . ((k + 1) + 1))) = (g2 . ((k + 1) + 1)) by A114;

              end;

                case k < 1;

                then

                 A122: k = 0 by NAT_1: 14;

                then 1 < ( len h) by A36, A22, A78, NAT_1: 13;

                then

                 A123: (h . 1) < (h . (1 + 1)) by A1;

                then

                 A124: ((h . (1 + 1)) -' 1) = ((h . (1 + 1)) - 1) by A31, XREAL_1: 233, XXREAL_0: 2;

                then

                 A125: (((h . ((k + 1) + 1)) -' 1) + 1) = (h . ((k + 1) + 1)) by A122;

                

                 A126: (F /. 1) = (F . 1) by A19, A22, FINSEQ_4: 15;

                (k + 1) < ( len F) by A36, A78, NAT_1: 13;

                

                then

                 A127: (g2 . ((k + 1) + 1)) = ((g2 /. (k + 1)) + (F /. ((k + 1) + 1))) by A38, NAT_1: 11

                .= ((F /. 1) + (F /. (1 + 1))) by A36, A37, A19, A22, A122, A126, FINSEQ_4: 15;

                

                 A128: (F /. (1 + 1)) = (F . (1 + 1)) by A36, A78, A122, FINSEQ_4: 15;

                ((h . 1) + 1) <= (h . (1 + 1)) by A123, NAT_1: 13;

                then (((h . 1) + 1) - 1) <= ((h . (1 + 1)) - 1) by XREAL_1: 9;

                then

                 A129: (h . 1) <= ((h . (1 + 1)) -' 1) by A26, A123, XREAL_1: 233, XXREAL_0: 2;

                (h . (1 + 1)) < ((h . (1 + 1)) + 1) by XREAL_1: 29;

                then

                 A130: ((h . (1 + 1)) - 1) < (((h . (1 + 1)) + 1) - 1) by XREAL_1: 9;

                then

                 A131: ((h . (1 + 1)) -' 1) < (h . (1 + 1)) by A26, A123, XREAL_1: 233, XXREAL_0: 2;

                

                 A132: 1 < (h . (1 + 1)) by A26, A123, XXREAL_0: 2;

                then (1 + 1) <= (h . (1 + 1)) by NAT_1: 13;

                then

                 A133: ((1 + 1) - 1) <= ((h . (1 + 1)) - 1) by XREAL_1: 9;

                then (((h . (1 + 1)) -' 1) -' 1) = (((h . (1 + 1)) -' 1) - 1) by A124, XREAL_1: 233;

                then

                 A134: ((((h . (1 + 1)) -' 1) -' 1) + 1) = ((h . (1 + 1)) -' 1);

                (1 + 1) in ( Seg ( len h)) by A36, A22, A78, A122, FINSEQ_1: 1;

                then (1 + 1) in ( dom h) by FINSEQ_1:def 3;

                then (h . (1 + 1)) in ( rng h) by FUNCT_1:def 3;

                then (h . (1 + 1)) in ( dom g) by A2;

                then

                 A135: (h . (1 + 1)) in ( Seg ( len g)) by FINSEQ_1:def 3;

                then (h . (1 + 1)) <= ( len g) by FINSEQ_1: 1;

                

                then

                 A136: (g /. (h . ((k + 1) + 1))) = (g . (h . (1 + 1))) by A122, A132, FINSEQ_4: 15

                .= (F . (1 + 1)) by A3, A36, A21, A79, A122, FUNCT_1: 13;

                (h . (1 + 1)) <= ( len g) by A135, FINSEQ_1: 1;

                then ((h . (1 + 1)) -' 1) < ( len g4) by A32, A124, A130, XXREAL_0: 2;

                

                then

                 A137: (g4 /. ((h . ((k + 1) + 1)) -' 1)) = (g4 . ((h . (1 + 1)) -' 1)) by A122, A124, A133, FINSEQ_4: 15

                .= (F . 1) by A37, A106, A122, A134, A131, A129;

                (h . (1 + 1)) <= ( len g) by A135, FINSEQ_1: 1;

                then

                 A138: ((h . ((k + 1) + 1)) -' 1) < ( len g) by A122, A125, NAT_1: 13;

                1 <= ((h . ((k + 1) + 1)) -' 1) by A122, A132, A125, NAT_1: 13;

                

                then (g4 . (((h . ((k + 1) + 1)) -' 1) + 1)) = ((g4 /. ((h . ((k + 1) + 1)) -' 1)) + (g /. (h . ((k + 1) + 1)))) by Def10, A122, A124, A138

                .= ((F /. 1) + (F /. (1 + 1))) by A19, A22, A128, A137, A136, FINSEQ_4: 15;

                hence (g4 . (h . ((k + 1) + 1))) = (g2 . ((k + 1) + 1)) by A122, A124, A127;

              end;

            end;

            hence (g4 . (h . ((k + 1) + 1))) = (g2 . ((k + 1) + 1));

          end;

          hence P[(k + 1)];

        end;

        defpred R[ Nat] means (h . ( len h)) <= ($1 + 1) & ($1 + 1) <= ( len g) implies (g4 . ($1 + 1)) = (g2 . ( len g2));

        

         A139: P[ 0 ] by A64;

        

         A140: for k be Nat holds P[k] from NAT_1:sch 2( A139, A75);

        

         A141: for k be Nat st R[k] holds R[(k + 1)]

        proof

          let k be Nat;

          assume

           A142: R[k];

          (h . ( len h)) <= ((k + 1) + 1) & ((k + 1) + 1) <= ( len g) implies (g4 . ((k + 1) + 1)) = (g2 . ( len g2))

          proof

            assume that

             A143: (h . ( len h)) <= ((k + 1) + 1) and

             A144: ((k + 1) + 1) <= ( len g);

            per cases by A143, XXREAL_0: 1;

              suppose

               A145: (h . ( len h)) < ((k + 1) + 1);

               A146:

              now

                assume ((k + 1) + 1) in ( rng h);

                then

                consider x be object such that

                 A147: x in ( dom h) and

                 A148: (h . x) = ((k + 1) + 1) by FUNCT_1:def 3;

                reconsider nx = x as Element of NAT by A147;

                

                 A149: x in ( Seg ( len h)) by A147, FINSEQ_1:def 3;

                then

                 A150: nx <= ( len h) by FINSEQ_1: 1;

                1 <= nx by A149, FINSEQ_1: 1;

                hence contradiction by A1, A145, A148, A150, Th6;

              end;

              1 <= ((k + 1) + 1) by NAT_1: 11;

              then ((k + 1) + 1) in ( Seg ( len g)) by A144, FINSEQ_1: 1;

              then

               A151: ((k + 1) + 1) in ( dom g) by FINSEQ_1:def 3;

              (k + 1) < ((k + 1) + 1) by XREAL_1: 29;

              then

               A152: (k + 1) < ( len g) by A144, XXREAL_0: 2;

              then

               A153: (g4 . ((k + 1) + 1)) = ((g4 /. (k + 1)) + (g /. ((k + 1) + 1))) by A34, NAT_1: 11;

              1 <= (k + 1) by NAT_1: 11;

              then

               A154: (g4 /. (k + 1)) = (g2 . ( len g2)) by A32, A142, A145, A152, FINSEQ_4: 15, NAT_1: 13;

              1 < ((k + 1) + 1) by XREAL_1: 29;

              

              then (g /. ((k + 1) + 1)) = (g . ((k + 1) + 1)) by A144, FINSEQ_4: 15

              .= ( 0* n) by A4, A146, A151;

              hence (g4 . ((k + 1) + 1)) = (g2 . ( len g2)) by A154, A153, EUCLID_4: 1;

            end;

              suppose

               A155: (h . ( len h)) = ((k + 1) + 1);

              

               A156: (( len h) -' 1) = (( len h) - 1) by A19, XREAL_1: 233;

              1 <= ((( len h) -' 1) + 1) & ((( len h) -' 1) + 1) <= ( len g2) implies (g4 . (h . ((( len h) -' 1) + 1))) = (g2 . ((( len h) -' 1) + 1)) by A140;

              hence (g4 . ((k + 1) + 1)) = (g2 . ( len g2)) by A36, A18, A21, A155, A156, FINSEQ_1: 1, FINSEQ_1:def 3;

            end;

          end;

          hence R[(k + 1)];

        end;

        

         A157: 1 <= (h . ( len h)) by A20, FINSEQ_1: 1;

        (h . ( len h)) <= 1 & 1 <= ( len g) implies (g4 . ( 0 + 1)) = (g2 . ( len g2))

        proof

          assume that

           A158: (h . ( len h)) <= 1 and 1 <= ( len g);

          (h . ( len h)) = 1 by A157, A158, XXREAL_0: 1;

          then ( len h) <= 1 by A1, A26, Th7;

          then

           A159: ( len h) = 1 by A19, XXREAL_0: 1;

          (g2 . 1) = (g . (h . 1)) by A3, A5, A37, A17, FUNCT_1: 13

          .= (g . 1) by A157, A158, A159, XXREAL_0: 1;

          hence (g4 . ( 0 + 1)) = (g2 . ( len g2)) by A6, A36, A33, A159, FINSEQ_1:def 3;

        end;

        then

         A160: R[ 0 ];

        for k be Nat holds R[k] from NAT_1:sch 2( A160, A141);

        hence ( Sum g) = ( Sum F) by A36, A39, A35, A29, A30;

      end;

        suppose

         A161: ( len F) <= 0 ;

        then

         A162: ( Sum F) = ( 0* n) by Def11;

        

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

        ( Seg ( len F)) = {} by A161;

        then ( dom F) = {} by FINSEQ_1:def 3;

        then

         A164: ( rng h) = {} by A3, A5, RELAT_1: 42;

         A165:

        now

          let z be object;

          assume

           A166: z in ( dom g);

          

          hence (g . z) = ( 0* n) by A4, A164

          .= ((( len g) |-> ( 0* n)) . z) by A163, A166, FINSEQ_2: 57;

        end;

        ( Seg ( len g)) = ( dom (( len g) |-> ( 0* n))) by FUNCOP_1: 13;

        then g = (( len g) |-> ( 0* n)) by A163, A165, FUNCT_1: 2;

        hence ( Sum g) = ( Sum F) by A162, Th21;

      end;

    end;

    theorem :: EUCLID_7:24

    

     Th23: for g be FinSequence of ( REAL n), h be FinSequence of NAT , F be FinSequence of ( REAL n) st h is one-to-one & ( rng h) c= ( dom g) & F = (g * h) & (for i be Element of NAT st i in ( dom g) & not i in ( rng h) holds (g . i) = ( 0* n)) holds ( Sum g) = ( Sum F)

    proof

      let g be FinSequence of ( REAL n), h be FinSequence of NAT , F be FinSequence of ( REAL n);

      assume that

       A1: h is one-to-one and

       A2: ( rng h) c= ( dom g) and

       A3: F = (g * h) and

       A4: for i be Element of NAT st i in ( dom g) & not i in ( rng h) holds (g . i) = ( 0* n);

      consider h3 be Permutation of ( dom h), h2 be FinSequence of NAT such that

       A5: h2 = (h * h3) and

       A6: h2 is increasing and

       A7: ( dom h) = ( dom h2) and

       A8: ( rng h) = ( rng h2) by A1, Th13;

      ( dom (g * h)) = ( dom h) by A2, RELAT_1: 27;

      then

      reconsider h33 = h3 as Permutation of ( dom F) by A3;

      reconsider F22 = (g * h2) as Function;

      ( dom F22) = ( dom h) by A2, A7, A8, RELAT_1: 27

      .= ( Seg ( len h)) by FINSEQ_1:def 3;

      then

      reconsider F23 = F22 as FinSequence by FINSEQ_1:def 2;

      ( rng F22) c= ( rng g) by RELAT_1: 26;

      then ( rng F23) c= ( REAL n) by XBOOLE_1: 1;

      then

      reconsider F2 = F23 as FinSequence of ( REAL n) by FINSEQ_1:def 4;

      F2 = (F (*) h33) by A3, A5, RELAT_1: 36;

      then ( Sum F) = ( Sum F2) by Th20;

      hence ( Sum g) = ( Sum F) by A2, A4, A6, A8, Th22;

    end;

    begin

    definition

      let n,i be Nat;

      :: original: Base_FinSeq

      redefine

      func Base_FinSeq (n,i) -> Element of ( REAL n) ;

      coherence

      proof

        ( len ( Base_FinSeq (n,i))) = n by MATRIXR2: 74;

        hence thesis by FINSEQ_2: 92;

      end;

    end

    theorem :: EUCLID_7:25

    

     Th24: for i1,i2 be Nat st 1 <= i1 & i1 <= n & ( Base_FinSeq (n,i1)) = ( Base_FinSeq (n,i2)) holds i1 = i2

    proof

      let i1,i2 be Nat;

      assume that

       A1: 1 <= i1 and

       A2: i1 <= n and

       A3: ( Base_FinSeq (n,i1)) = ( Base_FinSeq (n,i2));

      (( Base_FinSeq (n,i1)) . i1) = 1 by A1, A2, MATRIXR2: 75;

      hence thesis by A1, A2, A3, MATRIXR2: 76;

    end;

    theorem :: EUCLID_7:26

    

     Th25: ( sqr ( Base_FinSeq (n,i))) = ( Base_FinSeq (n,i))

    proof

      

       A1: ( dom ( sqrreal * ( Base_FinSeq (n,i)))) = (( Base_FinSeq (n,i)) " ( dom sqrreal )) by RELAT_1: 147;

      

       A2: ( rng ( Base_FinSeq (n,i))) c= REAL ;

      

       A3: for x be object st x in ( dom ( Base_FinSeq (n,i))) holds (( sqrreal * ( Base_FinSeq (n,i)) qua Function) . x) = (( Base_FinSeq (n,i)) . x)

      proof

        let x be object;

        assume

         A4: x in ( dom ( Base_FinSeq (n,i)));

        then

        reconsider nx = x as Element of NAT ;

        

         A5: (( sqrreal * ( Base_FinSeq (n,i)) qua Function) . x) = ( sqrreal . (( Base_FinSeq (n,i)) . x)) by A4, FUNCT_1: 13;

        

         A6: x in ( Seg ( len ( Base_FinSeq (n,i)))) by A4, FINSEQ_1:def 3;

        then

         A7: 1 <= nx by FINSEQ_1: 1;

        ( len ( Base_FinSeq (n,i))) = n by MATRIXR2: 74;

        then

         A8: nx <= n by A6, FINSEQ_1: 1;

        per cases ;

          suppose

           A9: nx = i;

          

          hence (( sqrreal * ( Base_FinSeq (n,i)) qua Function) . x) = ( sqrreal . 1) by A7, A8, A5, MATRIXR2: 75

          .= (1 ^2 ) by RVSUM_1:def 2

          .= (( Base_FinSeq (n,i)) . x) by A7, A8, A9, MATRIXR2: 75;

        end;

          suppose

           A10: nx <> i;

          

          hence (( sqrreal * ( Base_FinSeq (n,i)) qua Function) . x) = ( sqrreal . 0 ) by A7, A8, A5, MATRIXR2: 76

          .= ( 0 ^2 ) by RVSUM_1:def 2

          .= (( Base_FinSeq (n,i)) . x) by A7, A8, A10, MATRIXR2: 76;

        end;

      end;

      (( Base_FinSeq (n,i)) " ( dom sqrreal )) = (( Base_FinSeq (n,i)) " REAL ) by FUNCT_2:def 1

      .= ( dom ( Base_FinSeq (n,i))) by A2, Th1;

      hence thesis by A1, A3, FUNCT_1: 2;

    end;

    

     Lm3: 0 in REAL by XREAL_0:def 1;

    theorem :: EUCLID_7:27

    

     Th26: 1 <= i & i <= n implies ( Sum ( Base_FinSeq (n,i))) = 1

    proof

      assume that

       A1: 1 <= i and

       A2: i <= n;

      defpred P[ object, object] means ( not ($1 in i) implies $2 = 1) & ($1 in i implies $2 = 0 );

      set F = ( Base_FinSeq (n,i));

      

       A3: for x be object st x in NAT holds ex y be object st y in REAL & P[x, y]

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider nx = x as Element of NAT ;

        per cases ;

          suppose nx >= i;

          then

           A4: not nx in ( Segm i) by NAT_1: 44;

          take y = 1;

          thus y in REAL by XREAL_0:def 1;

          thus P[x, y] by A4;

        end;

          suppose nx < i;

          then nx in ( Segm i) by NAT_1: 44;

          hence ex y be object st y in REAL & P[x, y] by Lm3;

        end;

      end;

      consider f0 be sequence of REAL such that

       A5: for x be object st x in NAT holds P[x, (f0 . x)] from FUNCT_2:sch 1( A3);

      

       A6: ( len ( Base_FinSeq (n,i))) = n by MATRIXR2: 74;

      

       A7: for n2 be Nat st 0 <> n2 & n2 < ( len F) holds (f0 . (n2 + 1)) = ( addreal . ((f0 . n2),(F . (n2 + 1))))

      proof

        let n2 be Nat;

        assume that 0 <> n2 and

         A8: n2 < ( len F);

        

         A9: (n2 + 1) <= n by A6, A8, NAT_1: 13;

        

         A10: n2 in NAT by ORDINAL1:def 12;

        per cases ;

          suppose

           A11: (n2 + 1) < i;

          then n2 < i by NAT_1: 13;

          then n2 in ( Segm i) by NAT_1: 44;

          then

           A12: (f0 . n2) = 0 by A5, A10;

          

           A13: 1 <= (n2 + 1) by NAT_1: 11;

          

           A14: (n2 + 1) in ( Segm i) by A11, NAT_1: 44;

          (n2 + 1) <= ( len F) by A8, NAT_1: 13;

          

          then ( addreal . ((f0 . n2),(F . (n2 + 1)))) = ( addreal . ( 0 , 0 )) by A6, A11, A12, A13, MATRIXR2: 76

          .= ( 0 + 0 ) by BINOP_2:def 9;

          hence (f0 . (n2 + 1)) = ( addreal . ((f0 . n2),(F . (n2 + 1)))) by A5, A14;

        end;

          suppose

           A15: i <= (n2 + 1);

          per cases by A15, XXREAL_0: 1;

            suppose

             A16: i < (n2 + 1);

            then i <= n2 by NAT_1: 13;

            then

             A17: not n2 in ( Segm i) by NAT_1: 44;

            

             A18: not (n2 + 1) in ( Segm i) by A16, NAT_1: 44;

            1 <= (n2 + 1) by A1, A16, XXREAL_0: 2;

            then (F . (n2 + 1)) = 0 by A9, A16, MATRIXR2: 76;

            

            then ( addreal . ((f0 . n2),(F . (n2 + 1)))) = ( addreal . (1, 0 )) by A5, A17, A10

            .= (1 + 0 ) by BINOP_2:def 9;

            hence (f0 . (n2 + 1)) = ( addreal . ((f0 . n2),(F . (n2 + 1)))) by A5, A18;

          end;

            suppose

             A19: i = (n2 + 1);

            n2 < (n2 + 1) by XREAL_1: 29;

            then n2 in ( Segm i) by A19, NAT_1: 44;

            then (f0 . n2) = 0 by A5, A10;

            

            then

             A20: ( addreal . ((f0 . n2),(F . (n2 + 1)))) = ( addreal . ( 0 ,1)) by A1, A2, A19, MATRIXR2: 75

            .= ( 0 + 1) by BINOP_2:def 9;

             not (n2 + 1) in i by A19;

            hence (f0 . (n2 + 1)) = ( addreal . ((f0 . n2),(F . (n2 + 1)))) by A5, A20;

          end;

        end;

      end;

      

       A21: (f0 . 1) = (F . 1)

      proof

        per cases ;

          suppose

           A22: 1 < i;

          then 1 in ( Segm i) by NAT_1: 44;

          then

           A23: (f0 . 1) = 0 by A5;

          1 <= n by A1, A2, XXREAL_0: 2;

          hence (f0 . 1) = (F . 1) by A22, A23, MATRIXR2: 76;

        end;

          suppose

           A24: 1 >= i;

          then not 1 in ( Segm i) by NAT_1: 44;

          then

           A25: (f0 . 1) = 1 by A5;

          1 = i by A1, A24, XXREAL_0: 1;

          hence (f0 . 1) = (F . 1) by A2, A25, MATRIXR2: 75;

        end;

      end;

      

       A26: (f0 . ( len F)) = 1

      proof

        per cases ;

          suppose ( len F) < i;

          hence (f0 . ( len F)) = 1 by A2, MATRIXR2: 74;

        end;

          suppose ( len F) >= i;

          then not ( len F) in ( Segm i) by NAT_1: 44;

          hence (f0 . ( len F)) = 1 by A5;

        end;

      end;

      ( len ( Base_FinSeq (n,i))) >= 1 by A1, A2, A6, XXREAL_0: 2;

      hence thesis by A21, A26, A7, FINSOP_1:def 1;

    end;

    theorem :: EUCLID_7:28

    

     Th27: 1 <= i & i <= n implies |.( Base_FinSeq (n,i)).| = 1

    proof

      assume that

       A1: 1 <= i and

       A2: i <= n;

      ( sqrt ( Sum ( Base_FinSeq (n,i)))) = 1 by A1, A2, Th26, SQUARE_1: 18;

      hence thesis by Th25;

    end;

    theorem :: EUCLID_7:29

    

     Th28: 1 <= i & i <= n & i <> j implies |(( Base_FinSeq (n,i)), ( Base_FinSeq (n,j)))| = 0

    proof

      assume that

       A1: 1 <= i and

       A2: i <= n and

       A3: i <> j;

      set x1 = ( Base_FinSeq (n,i)), x2 = ( Base_FinSeq (n,j));

      

       A4: ( dom ( 0* n)) = ( Seg ( len (n |-> 0 qua Real))) by FINSEQ_1:def 3

      .= ( Seg n) by CARD_1:def 7;

      

       A5: ( dom x2) = ( Seg ( len x2)) by FINSEQ_1:def 3

      .= ( Seg n) by MATRIXR2: 74;

      

       A6: ( dom x1) = ( Seg ( len x1)) by FINSEQ_1:def 3

      .= ( Seg n) by MATRIXR2: 74;

      

       A7: ( dom <:x1, x2:>) = (( dom x1) /\ ( dom x2)) by FUNCT_3:def 7;

      ( dom multreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

      

      then

       A8: ( dom ( multreal * <:x1, x2:>)) = ( <:x1, x2:> " [: REAL , REAL :]) by RELAT_1: 147

      .= ( Seg n) by A7, A6, A5, RELSET_1: 22;

      for x be object st x in ( dom ( 0* n)) holds (( multreal * <:x1, x2:>) . x) = (( 0* n) . x)

      proof

        let x be object;

        assume

         A9: x in ( dom ( 0* n));

        then

        reconsider nx = x as Element of NAT ;

        

         A10: (( multreal * <:x1, x2:>) . x) = ( multreal . ( <:x1, x2:> . x)) by A4, A8, A9, FUNCT_1: 12

        .= ( multreal . [(x1 . nx), (x2 . nx)]) by A4, A7, A6, A5, A9, FUNCT_3:def 7;

        

         A11: nx <= n by A4, A9, FINSEQ_1: 1;

        

         A12: 1 <= nx by A4, A9, FINSEQ_1: 1;

        per cases ;

          suppose

           A13: nx = i;

          then

           A14: (x1 . nx) = 1 by A1, A2, MATRIXR2: 75;

          

           A15: (x2 . nx) = 0 by A1, A2, A3, A13, MATRIXR2: 76;

          ( multreal . [(x1 . nx), (x2 . nx)]) = ( multreal . ((x1 . nx),(x2 . nx)))

          .= (1 * 0 ) by A15, A14, BINOP_2:def 11

          .= 0 ;

          hence (( multreal * <:x1, x2:>) . x) = (( 0* n) . x) by A10;

        end;

          suppose

           A16: nx <> i;

          reconsider r = (x2 . nx) as Element of REAL by XREAL_0:def 1;

          

           A17: (x1 . nx) = 0 by A12, A11, A16, MATRIXR2: 76;

          ( multreal . [(x1 . nx), (x2 . nx)]) = ( multreal . ((x1 . nx),(x2 . nx)))

          .= ( 0 * r) by A17, BINOP_2:def 11

          .= 0 ;

          hence (( multreal * <:x1, x2:>) . x) = (( 0* n) . x) by A10;

        end;

      end;

      then ( multreal * <:x1, x2:>) = ( 0* n) by A4, A8, FUNCT_1: 2;

      then ( multreal .: (x1,x2)) = ( 0* n) by FUNCOP_1:def 3;

      hence |(( Base_FinSeq (n,i)), ( Base_FinSeq (n,j)))| = 0 by RVSUM_1: 81;

    end;

    theorem :: EUCLID_7:30

    

     Th29: for x be Element of ( REAL n) st 1 <= i & i <= n holds |(x, ( Base_FinSeq (n,i)))| = (x . i)

    proof

      let x be Element of ( REAL n);

      assume that

       A1: 1 <= i and

       A2: i <= n;

      set x2 = ( Base_FinSeq (n,i));

      

       A3: ( len x) = n by CARD_1:def 7;

      

       A4: ( len x2) = n by MATRIXR2: 74;

      then

       A5: ( len ( mlt (x,x2))) = n by A3, MATRPROB: 30;

      

       A6: for j be Nat st 1 <= j & j <= n holds (( mlt (x,x2)) . j) = (((x /. i) * ( Base_FinSeq (n,i))) . j)

      proof

        let j be Nat;

        assume that

         A7: 1 <= j and

         A8: j <= n;

        reconsider j0 = j as Element of NAT by ORDINAL1:def 12;

         A9:

        now

          per cases ;

            case i = j;

            hence (((x /. i) * ( Base_FinSeq (n,i))) . j) = ((x /. j) * (( Base_FinSeq (n,i)) . j)) by RVSUM_1: 44;

          end;

            case i <> j;

            then

             A10: (( Base_FinSeq (n,i)) . j0) = 0 by A7, A8, MATRIXR2: 76;

            (((x /. i) * ( Base_FinSeq (n,i))) . j) = ((x /. i) * (( Base_FinSeq (n,i)) . j)) by RVSUM_1: 44

            .= ((x /. j) * (( Base_FinSeq (n,i)) . j)) by A10;

            hence (((x /. i) * ( Base_FinSeq (n,i))) . j) = ((x /. j) * (( Base_FinSeq (n,i)) . j));

          end;

        end;

        (( mlt (x,x2)) . j) = ((x . j) * (x2 . j)) by RVSUM_1: 59;

        hence (( mlt (x,x2)) . j) = (((x /. i) * ( Base_FinSeq (n,i))) . j) by A3, A7, A8, A9, FINSEQ_4: 15;

      end;

      ( len ((x /. i) * ( Base_FinSeq (n,i)))) = n by A4, RVSUM_1: 117;

      then ( mlt (x,x2)) = ((x /. i) * ( Base_FinSeq (n,i))) by A5, A6, FINSEQ_1: 14;

      

      then ( Sum ( mlt (x,x2))) = ((x /. i) * ( Sum ( Base_FinSeq (n,i)))) by RVSUM_1: 87

      .= ((x /. i) * 1) by A1, A2, Th26

      .= (x . i) by A1, A2, A3, FINSEQ_4: 15;

      hence |(x, ( Base_FinSeq (n,i)))| = (x . i);

    end;

    definition

      let n be Nat;

      let x0 be Element of ( REAL n);

      :: EUCLID_7:def12

      func ProjFinSeq x0 -> FinSequence of ( REAL n) means

      : Def12: ( len it ) = n & for i be Nat st 1 <= i & i <= n holds (it . i) = ( |(x0, ( Base_FinSeq (n,i)))| * ( Base_FinSeq (n,i)));

      existence

      proof

        defpred P[ set, set] means for i be Nat st i = $1 & 1 <= i & i <= n holds $2 = ( |(x0, ( Base_FinSeq (n,i)))| * ( Base_FinSeq (n,i)));

        

         A1: for k be Nat st k in ( Seg n) holds ex x be Element of ( REAL n) st P[k, x]

        proof

          reconsider n0 = n as Element of NAT by ORDINAL1:def 12;

          let k be Nat;

          assume k in ( Seg n);

          reconsider k0 = k as Element of NAT by ORDINAL1:def 12;

          reconsider x00 = ( |(x0, ( Base_FinSeq (n0,k0)))| * ( Base_FinSeq (n0,k0))) as Element of ( REAL n);

          for i be Nat st i = k & 1 <= i & i <= n holds x00 = ( |(x0, ( Base_FinSeq (n,i)))| * ( Base_FinSeq (n,i)));

          hence ex x be Element of ( REAL n) st P[k, x];

        end;

        consider p be FinSequence of ( REAL n) such that

         A2: ( dom p) = ( Seg n) & for k be Nat st k in ( Seg n) holds P[k, (p . k)] from FINSEQ_1:sch 5( A1);

        

         A3: for i be Nat st 1 <= i & i <= n holds (p . i) = ( |(x0, ( Base_FinSeq (n,i)))| * ( Base_FinSeq (n,i))) by FINSEQ_1: 1, A2;

        ( Seg n) = ( Seg ( len p)) by A2, FINSEQ_1:def 3;

        hence thesis by A3, FINSEQ_1: 6;

      end;

      uniqueness

      proof

        let r1,r2 be FinSequence of ( REAL n);

        assume that

         A4: ( len r1) = n and

         A5: for i be Nat st 1 <= i & i <= n holds (r1 . i) = ( |(x0, ( Base_FinSeq (n,i)))| * ( Base_FinSeq (n,i))) and

         A6: ( len r2) = n and

         A7: for i be Nat st 1 <= i & i <= n holds (r2 . i) = ( |(x0, ( Base_FinSeq (n,i)))| * ( Base_FinSeq (n,i)));

        for k be Nat st 1 <= k & k <= n holds (r1 . k) = (r2 . k)

        proof

          reconsider n22 = n as Element of NAT by ORDINAL1:def 12;

          let k be Nat;

          assume that

           A8: 1 <= k and

           A9: k <= n;

          reconsider k0 = k as Element of NAT by ORDINAL1:def 12;

          (r1 . k0) = ( |(x0, ( Base_FinSeq (n22,k0)))| * ( Base_FinSeq (n22,k0))) by A5, A8, A9;

          hence (r1 . k) = (r2 . k) by A7, A8, A9;

        end;

        hence r1 = r2 by A4, A6, FINSEQ_1: 14;

      end;

    end

    theorem :: EUCLID_7:31

    

     Th30: for x0 be Element of ( REAL n) holds x0 = ( Sum ( ProjFinSeq x0))

    proof

      let x0 be Element of ( REAL n);

      set f = ( ProjFinSeq x0);

      reconsider n2 = n as Element of NAT by ORDINAL1:def 12;

      now

        per cases ;

          case

           A1: ( len f) > 0 ;

          set g2 = ( accum f);

          

           A2: ( len f) = ( len g2) by Def10;

          

           A3: (f . 1) = (g2 . 1) by Def10;

          defpred P[ Nat] means for i be Nat st 1 <= i & i <= ( len f) & 1 <= $1 & $1 <= ( len f) holds (i <= $1 implies ((g2 /. $1) . i) = (x0 . i)) & (i > $1 implies ((g2 /. $1) . i) = 0 );

          

           A4: ( len f) = n by Def12;

          

           A5: ( 0 + 1) <= ( len f) by A1, NAT_1: 13;

          

           A6: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            reconsider k2 = k as Element of NAT by ORDINAL1:def 12;

            assume

             A7: P[k];

            for i be Nat st 1 <= i & i <= ( len f) & 1 <= (k + 1) & (k + 1) <= ( len f) holds (i <= (k + 1) implies ((g2 /. (k + 1)) . i) = (x0 . i)) & (i > (k + 1) implies ((g2 /. (k + 1)) . i) = 0 )

            proof

              let i be Nat;

              assume that

               A8: 1 <= i and

               A9: i <= ( len f) and

               A10: 1 <= (k + 1) and

               A11: (k + 1) <= ( len f);

              (g2 /. (k + 1)) is Element of ( REAL n);

              then

              reconsider r = (g2 . (k + 1)) as Element of ( REAL n) by A2, A10, A11, FINSEQ_4: 15;

              reconsider i2 = i as Element of NAT by ORDINAL1:def 12;

              

               A12: (g2 /. (k + 1)) = (g2 . (k + 1)) by A2, A10, A11, FINSEQ_4: 15;

              now

                per cases ;

                  case

                   A13: 1 <= k;

                  reconsider r3 = (f /. (k + 1)) as Element of ( REAL n);

                  reconsider r2 = (g2 /. k) as Element of ( REAL n);

                  

                   A14: (( ProjFinSeq x0) /. (k + 1)) = (( ProjFinSeq x0) . (k + 1)) by A10, A11, FINSEQ_4: 15

                  .= ( |(x0, ( Base_FinSeq (n2,(k + 1))))| * ( Base_FinSeq (n2,(k + 1)))) by A4, A10, A11, Def12;

                  

                   A15: k < (k + 1) by XREAL_1: 29;

                  then

                   A16: k < ( len f) by A11, XXREAL_0: 2;

                  then r = ((g2 /. k) + (f /. (k + 1))) by Def10, A13;

                  then

                   A17: (r . i) = ((r2 . i) + (r3 . i)) by RVSUM_1: 11;

                   A18:

                  now

                    assume

                     A19: i <= (k + 1);

                    per cases by A19, XXREAL_0: 1;

                      suppose

                       A20: i < (k + 1);

                      then

                       A21: i <= k by NAT_1: 13;

                      ((f /. (k + 1)) . i) = ( |(x0, ( Base_FinSeq (n2,(k + 1))))| * (( Base_FinSeq (n2,(k2 + 1))) . i2)) by A14, RVSUM_1: 44

                      .= ( |(x0, ( Base_FinSeq (n2,(k + 1))))| * 0 ) by A4, A8, A9, A20, MATRIXR2: 76;

                      hence ((g2 /. (k + 1)) . i) = (x0 . i) by A7, A8, A9, A12, A13, A16, A17, A21;

                    end;

                      suppose

                       A22: i = (k + 1);

                      then

                       A23: ((g2 /. k) . i) = 0 by A7, A8, A9, A13, A15, A16;

                      ((f /. (k + 1)) . i) = ( |(x0, ( Base_FinSeq (n2,(k + 1))))| * (( Base_FinSeq (n2,(k2 + 1))) . i2)) by A14, RVSUM_1: 44

                      .= ( |(x0, ( Base_FinSeq (n2,(k + 1))))| * 1) by A4, A8, A9, A22, MATRIXR2: 75

                      .= (x0 . (k + 1)) by A4, A10, A11, Th29;

                      hence ((g2 /. (k + 1)) . i) = (x0 . i) by A2, A8, A9, A17, A22, A23, FINSEQ_4: 15;

                    end;

                  end;

                  now

                    assume

                     A24: i > (k + 1);

                    then

                     A25: i > k by A15, XXREAL_0: 2;

                    ((f /. (k + 1)) . i) = ( |(x0, ( Base_FinSeq (n2,(k + 1))))| * (( Base_FinSeq (n2,(k2 + 1))) . i2)) by A14, RVSUM_1: 44

                    .= ( |(x0, ( Base_FinSeq (n2,(k + 1))))| * 0 ) by A4, A8, A9, A24, MATRIXR2: 76

                    .= 0 ;

                    hence ((g2 /. (k + 1)) . i) = 0 by A7, A8, A9, A12, A13, A16, A17, A25;

                  end;

                  hence (i <= (k + 1) implies ((g2 /. (k + 1)) . i) = (x0 . i)) & (i > (k + 1) implies ((g2 /. (k + 1)) . i) = 0 ) by A18;

                end;

                  case k < 1;

                  then

                   A26: (k + 1) <= ( 0 + 1) by NAT_1: 13;

                  then

                   A27: k = 0 by XREAL_1: 6;

                   A28:

                  now

                    assume

                     A29: i > ( 0 + 1);

                    (g2 /. 1) = (f . 1) by A5, A2, A3, FINSEQ_4: 15;

                    

                    then ((g2 /. 1) . i) = (( |(x0, ( Base_FinSeq (n2,1)))| * ( Base_FinSeq (n2,1))) . i) by A5, A4, Def12

                    .= ( |(x0, ( Base_FinSeq (n2,1)))| * (( Base_FinSeq (n2,1)) . i2)) by RVSUM_1: 44

                    .= ( |(x0, ( Base_FinSeq (n2,1)))| * 0 ) by A4, A9, A29, MATRIXR2: 76

                    .= 0 ;

                    hence ((g2 /. (k + 1)) . i) = 0 by A27;

                  end;

                   A30:

                  now

                    assume i <= ( 0 + 1);

                    then

                     A31: i = 1 by A8, XXREAL_0: 1;

                    (g2 /. 1) = (f . 1) by A5, A2, A3, FINSEQ_4: 15;

                    

                    then ((g2 /. 1) . 1) = (( |(x0, ( Base_FinSeq (n2,1)))| * ( Base_FinSeq (n2,1))) . 1) by A5, A4, Def12

                    .= ( |(x0, ( Base_FinSeq (n2,1)))| * (( Base_FinSeq (n2,1)) . 1)) by RVSUM_1: 44

                    .= ( |(x0, ( Base_FinSeq (n2,1)))| * 1) by A5, A4, MATRIXR2: 75

                    .= (x0 . 1) by A5, A4, Th29;

                    hence ((g2 /. ( 0 + 1)) . i) = (x0 . i) by A31;

                  end;

                  k <= 0 by A26, XREAL_1: 6;

                  hence (i <= (k + 1) implies ((g2 /. (k + 1)) . i) = (x0 . i)) & (i > (k + 1) implies ((g2 /. (k + 1)) . i) = 0 ) by A30, A28;

                end;

              end;

              hence thesis;

            end;

            hence P[(k + 1)];

          end;

          reconsider r4 = (g2 /. ( len f)) as Element of ( REAL n);

          

           A32: ( len x0) = n by CARD_1:def 7;

          then

           A33: ( len x0) = ( len r4) by CARD_1:def 7;

          

           A34: P[ 0 ];

          

           A35: for k be Nat holds P[k] from NAT_1:sch 2( A34, A6);

          for i be Nat st 1 <= i & i <= ( len r4) holds ((g2 /. ( len f)) . i) = (x0 . i)

          proof

            let i be Nat;

            assume that

             A36: 1 <= i and

             A37: i <= ( len r4);

            

             A38: i <= ( len f) by A4, A37, CARD_1:def 7;

            1 <= ( len f) by A4, A32, A33, A36, A37, XXREAL_0: 2;

            hence ((g2 /. ( len f)) . i) = (x0 . i) by A35, A36, A38;

          end;

          then x0 = (g2 /. ( len f)) by A33, FINSEQ_1: 14;

          hence x0 = (g2 . ( len f)) by A5, A2, FINSEQ_4: 15;

        end;

          case ( len f) <= 0 ;

          then

           A39: n = 0 by Def12;

          then x0 = ( <*> REAL );

          hence x0 = ( 0* n) by A39;

        end;

      end;

      hence x0 = ( Sum ( ProjFinSeq x0)) by Def11;

    end;

    definition

      let n be Nat;

      :: EUCLID_7:def13

      func RN_Base n -> Subset of ( REAL n) equals { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= n };

      coherence

      proof

        { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= n } c= ( REAL n)

        proof

          let x be object;

          assume x in { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= n };

          then ex i be Element of NAT st x = ( Base_FinSeq (n,i)) & 1 <= i & i <= n;

          hence x in ( REAL n);

        end;

        hence thesis;

      end;

    end

    theorem :: EUCLID_7:32

    

     Th31: for n be non zero Nat holds ( RN_Base n) <> {}

    proof

      let n be non zero Nat;

      ( 0 + 1) <= n by NAT_1: 13;

      then ( Base_FinSeq (n,1)) in { ( Base_FinSeq (n,i)) where i be Element of NAT : 1 <= i & i <= n };

      hence thesis;

    end;

    registration

      cluster ( RN_Base 0 ) -> empty;

      coherence

      proof

        assume not thesis;

        then

        consider x be object such that

         A1: x in ( RN_Base 0 ) by XBOOLE_0:def 1;

        ex i be Element of NAT st x = ( Base_FinSeq ( 0 ,i)) & 1 <= i & i <= 0 by A1;

        hence thesis;

      end;

    end

    registration

      let n be non zero Nat;

      cluster ( RN_Base n) -> non empty;

      coherence by Th31;

    end

    registration

      let n;

      cluster ( RN_Base n) -> orthogonal_basis;

      coherence

      proof

        set B = ( RN_Base n);

        

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

        proof

          let y be object;

          assume y in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) };

          then ex x be Element of ( REAL n) st y = x & ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i));

          hence y in B;

        end;

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

        proof

          let y be object;

          assume y in B;

          then ex i2 be Element of NAT st y = ( Base_FinSeq (n,i2)) & 1 <= i2 & i2 <= n;

          hence y in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) };

        end;

        then

         A2: B = { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) } by A1, XBOOLE_0:def 10;

        thus B is R-orthogonal

        proof

          let x,y be real-valued FinSequence;

          assume that

           A3: x in B and

           A4: y in B and

           A5: x <> y;

          

           A6: ex y0 be Element of ( REAL n) st y = y0 & ex i be Element of NAT st 1 <= i & i <= n & y0 = ( Base_FinSeq (n,i)) by A2, A4;

          ex x0 be Element of ( REAL n) st x = x0 & ex i be Element of NAT st 1 <= i & i <= n & x0 = ( Base_FinSeq (n,i)) by A2, A3;

          hence |(x, y)| = 0 by A5, A6, Th28;

        end;

        thus B is R-normal

        proof

          let x be real-valued FinSequence;

          assume x in B;

          then ex x0 be Element of ( REAL n) st x = x0 & ex i be Element of NAT st 1 <= i & i <= n & x0 = ( Base_FinSeq (n,i)) by A2;

          hence |.x.| = 1 by Th27;

        end;

        let B2 be R-orthonormal Subset of ( REAL n);

        assume

         A7: B c= B2;

        now

          assume not B2 c= B;

          then

          consider x be object such that

           A8: x in B2 and

           A9: not x in B;

          reconsider rx = x as Element of ( REAL n) by A8;

           A10:

          now

            assume rx <> ( 0* n);

            then

            consider i be 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 B by A11, A12;

            then |(rx, ( Base_FinSeq (n,i)))| = 0 by A7, A8, A9, Def3;

            hence contradiction by A11, A12, A13, Th29;

          end;

           |.( 0* n).| = 0 by EUCLID: 7;

          hence contradiction by A8, A10, Def4;

        end;

        hence thesis by A7, XBOOLE_0:def 10;

      end;

    end

    registration

      let n;

      cluster orthogonal_basis for Subset of ( REAL n);

      existence

      proof

        take ( RN_Base n);

        thus thesis;

      end;

    end

    definition

      let n;

      mode Orthogonal_Basis of n is orthogonal_basis Subset of ( REAL n);

    end

    registration

      let n be non zero Nat;

      cluster -> non empty for Orthogonal_Basis of n;

      coherence

      proof

        let B be Orthogonal_Basis of n;

        assume

         A1: B is empty;

        then B c= ( RN_Base n);

        hence contradiction by A1, Def6;

      end;

    end

    begin

    registration

      let n be Element of NAT ;

      cluster ( REAL-US n) -> constituted-FinSeqs;

      coherence

      proof

        let a be Element of ( REAL-US n);

        reconsider a as Element of ( REAL n) by REAL_NS1:def 6;

        a is FinSequence of REAL ;

        hence thesis;

      end;

    end

    registration

      let n be Element of NAT ;

      cluster -> real-valued for Element of ( REAL-US n);

      coherence

      proof

        let a be Element of ( REAL-US n);

        reconsider a as Element of ( REAL n) by REAL_NS1:def 6;

        a is FinSequence of REAL ;

        hence thesis;

      end;

    end

    registration

      let n be Element of NAT ;

      let x,y be VECTOR of ( REAL-US n), a,b be real-valued Function;

      identify a + b with x + y when x = a, y = b;

      compatibility

      proof

        assume that

         A1: x = a and

         A2: y = b;

        reconsider a1 = a, b1 = b as Element of ( REAL n) by A1, A2, REAL_NS1:def 6;

        

        thus (x + y) = (( Euclid_add n) . (a1,b1)) by A1, A2, REAL_NS1:def 6

        .= (a + b) by REAL_NS1:def 1;

      end;

    end

    registration

      let n be Element of NAT , x be VECTOR of ( REAL-US n), y be real-valued Function, a,b be Element of REAL ;

      identify b (#) y with a * x when x = y, a = b;

      compatibility

      proof

        assume that

         A1: x = y and

         A2: a = b;

        reconsider y1 = y as Element of ( REAL n) by A1, REAL_NS1:def 6;

        

        thus (a * x) = (( Euclid_mult n) . (b,y1)) by A1, A2, REAL_NS1:def 6

        .= (b (#) y) by REAL_NS1:def 2;

      end;

    end

    registration

      let n be Element of NAT ;

      let x be VECTOR of ( REAL-US n), a be real-valued Function;

      identify - a with - x when x = a;

      compatibility

      proof

        x is Element of ( REAL n) by REAL_NS1:def 6;

        then

        reconsider xn = x as Element of ( REAL-NS n) by REAL_NS1:def 4;

        assume

         A1: x = a;

        then

        reconsider a1 = a as Element of ( REAL n) by REAL_NS1:def 6;

        

        thus ( - x) = ( - xn) by REAL_NS1: 13

        .= ( - a1) by A1, REAL_NS1: 4

        .= ( - a);

      end;

    end

    registration

      let n be Element of NAT ;

      let x,y be VECTOR of ( REAL-US n), a,b be real-valued Function;

      identify a - b with x - y when x = a, y = b;

      compatibility ;

    end

    theorem :: EUCLID_7:33

    

     Th32: for n,j be Element of NAT , F be FinSequence of the carrier of ( REAL-US n), Bn be Subset of ( REAL-US n), v0 be Element of ( REAL-US n), l be Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & ( rng F) = ( Carrier l) & v0 in Bn & j in ( dom (l (#) F)) & v0 = (F . j) holds (( Euclid_scalar n) . (v0,( Sum (l (#) F)))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0)))

    proof

      let n,j be Element of NAT , F be FinSequence of the carrier of ( REAL-US n), Bn be Subset of ( REAL-US n), v0 be Element of ( REAL-US n), l be Linear_Combination of Bn;

      assume that

       A1: F is one-to-one and

       A2: Bn is R-orthogonal and

       A3: ( rng F) = ( Carrier l) and

       A4: v0 in Bn and

       A5: j in ( dom (l (#) F)) and

       A6: v0 = (F . j);

      

       A7: ( len (l (#) F)) = ( len F) by RLVECT_2:def 7;

      

      then

       A8: ( dom (l (#) F)) = ( Seg ( len F)) by FINSEQ_1:def 3

      .= ( dom F) by FINSEQ_1:def 3;

      reconsider F2 = (l (#) F) as FinSequence of the carrier of ( REAL-US n);

      reconsider rv0 = v0 as Element of ( REAL n) by REAL_NS1:def 6;

      

       A9: ( Carrier l) c= Bn by RLVECT_2:def 6;

      

       A10: ( dom (l (#) F)) = ( Seg ( len (l (#) F))) by FINSEQ_1:def 3;

      then

       A11: j <= ( len F) by A5, A7, FINSEQ_1: 1;

      consider f be sequence of the carrier of ( REAL-US n) such that

       A12: ( Sum F2) = (f . ( len F2)) and

       A13: (f . 0 ) = ( 0. ( REAL-US n)) and

       A14: for j2 be Nat holds for v be Element of ( REAL-US n) st j2 < ( len F2) & v = (F2 . (j2 + 1)) holds (f . (j2 + 1)) = ((f . j2) + v) by RLVECT_1:def 12;

      defpred Q[ Nat] means $1 >= j & $1 <= ( len F) implies (( Euclid_scalar n) . (v0,(f . $1))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0)));

      defpred P[ Nat] means $1 < j implies (( Euclid_scalar n) . (v0,(f . $1))) = 0 ;

      ( 0. ( REAL-US n)) = ( 0* n) by REAL_NS1:def 6;

      

      then (( Euclid_scalar n) . (v0,(f . 0 ))) = |(rv0, ( 0* n))| by A13, REAL_NS1:def 5

      .= 0 by EUCLID_4: 18;

      then

       A15: P[ 0 ];

      

       A16: j in ( Seg ( len F)) by A5, A7, FINSEQ_1:def 3;

      then

       A17: j <= ( len F2) by A7, FINSEQ_1: 1;

      

       A18: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A19: P[k];

        now

          per cases ;

            case

             A20: k < ( len F2);

            

             A21: 1 <= (k + 1) by NAT_1: 11;

            (k + 1) <= ( len F2) by A20, NAT_1: 13;

            then (k + 1) in ( Seg ( len F2)) by A21, FINSEQ_1: 1;

            then (k + 1) in ( dom F2) by FINSEQ_1:def 3;

            then (F2 . (k + 1)) in ( rng F2) by FUNCT_1:def 3;

            then

            reconsider v = (F2 . (k + 1)) as Element of ( REAL-US n);

            

             A22: (f . (k + 1)) = ((f . k) + v) by A14, A20;

            reconsider rv = v as Element of ( REAL n) by REAL_NS1:def 6;

            reconsider fk = (f . k) as Element of ( REAL n) by REAL_NS1:def 6;

            per cases ;

              suppose

               A23: (k + 1) < j;

              

               A24: 1 <= (k + 1) by NAT_1: 11;

              (k + 1) < ( len F) by A11, A23, XXREAL_0: 2;

              then (k + 1) in ( Seg ( len F)) by A24, FINSEQ_1: 1;

              then

               A25: (k + 1) in ( dom F) by FINSEQ_1:def 3;

              then

               A26: (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

              then

               A27: rv0 <> (F /. (k + 1)) by A1, A5, A6, A8, A23, A25, FUNCT_1:def 4;

              reconsider fk1 = (F /. (k + 1)) as Element of ( REAL n) by REAL_NS1:def 6;

              

               A28: k < (k + 1) by XREAL_1: 29;

              

               A29: |(rv0, (fk + rv))| = ( |(rv0, fk)| + |(rv0, rv)|) by EUCLID_4: 28;

              

               A30: (F /. (k + 1)) in ( rng F) by A25, A26, FUNCT_1:def 3;

              v = ((l . (F /. (k + 1))) * (F /. (k + 1))) by A8, A25, RLVECT_2:def 7;

              

              then |(rv0, rv)| = ((l . (F /. (k + 1))) * |(rv0, fk1)|) by EUCLID_4: 22

              .= ((l . (F /. (k + 1))) * 0 ) by A2, A3, A4, A9, A30, A27

              .= 0 ;

              then |(rv0, (fk + rv))| = 0 by A19, A23, A28, A29, REAL_NS1:def 5, XXREAL_0: 2;

              hence P[(k + 1)] by A22, REAL_NS1:def 5;

            end;

              suppose (k + 1) >= j;

              hence P[(k + 1)];

            end;

          end;

            case

             A31: k >= ( len F2);

            (k + 1) > k by XREAL_1: 29;

            then (k + 1) > ( len F2) by A31, XXREAL_0: 2;

            hence P[(k + 1)] by A17, XXREAL_0: 2;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A32: for i be Nat holds P[i] from NAT_1:sch 2( A15, A18);

      

       A33: for i be Nat st i < j holds (( Euclid_scalar n) . (v0,(f . i))) = 0 by A32;

      

       A34: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        assume

         A35: Q[k];

        per cases ;

          suppose (k + 1) < j;

          hence Q[(k + 1)];

        end;

          suppose

           A36: (k + 1) >= j;

          per cases by A36, XXREAL_0: 1;

            suppose

             A37: (k + 1) > j;

            per cases ;

              suppose

               A38: (k + 1) <= ( len F2);

              1 <= (k + 1) by NAT_1: 11;

              then

               A39: (k + 1) in ( Seg ( len F2)) by A38, FINSEQ_1: 1;

              then

               A40: (k + 1) in ( dom F) by A7, FINSEQ_1:def 3;

              then

               A41: (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

              then

               A42: (F /. (k + 1)) in ( rng F) by A40, FUNCT_1:def 3;

              (k + 1) in ( dom F2) by A39, FINSEQ_1:def 3;

              then (F2 . (k + 1)) in ( rng F2) by FUNCT_1:def 3;

              then

              reconsider v = (F2 . (k + 1)) as Element of ( REAL-US n);

              reconsider fk1 = (F /. (k + 1)) as Element of ( REAL n) by REAL_NS1:def 6;

              reconsider fk = (f . k) as Element of ( REAL n) by REAL_NS1:def 6;

              k < (k + 1) by XREAL_1: 29;

              then

               A43: k < ( len F2) by A38, XXREAL_0: 2;

              then

               A44: (f . (k + 1)) = ((f . k) + v) by A14;

              

               A45: rv0 <> (F /. (k + 1)) by A1, A5, A6, A8, A37, A40, A41, FUNCT_1:def 4;

              reconsider rv = v as Element of ( REAL n) by REAL_NS1:def 6;

              v = ((l . (F /. (k + 1))) * (F /. (k + 1))) by A8, A40, RLVECT_2:def 7;

              

              then

               A46: |(rv0, rv)| = ((l . (F /. (k + 1))) * |(rv0, fk1)|) by EUCLID_4: 22

              .= ((l . (F /. (k + 1))) * 0 ) by A2, A3, A4, A9, A42, A45

              .= 0 ;

               |(rv0, (fk + rv))| = ( |(rv0, fk)| + |(rv0, rv)|) by EUCLID_4: 28;

              then |(rv0, (fk + rv))| = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by A35, A37, A43, A46, NAT_1: 13, REAL_NS1:def 5, RLVECT_2:def 7;

              hence Q[(k + 1)] by A44, REAL_NS1:def 5;

            end;

              suppose (k + 1) > ( len F2);

              hence Q[(k + 1)] by RLVECT_2:def 7;

            end;

          end;

            suppose

             A47: (k + 1) = j;

            then (F2 . (k + 1)) in ( rng F2) by A5, FUNCT_1:def 3;

            then

            reconsider v = (F2 . (k + 1)) as Element of ( REAL-US n);

            reconsider rv = v as Element of ( REAL n) by REAL_NS1:def 6;

            

             A48: v = ((l . (F /. (k + 1))) * (F /. (k + 1))) by A5, A47, RLVECT_2:def 7;

            (k + 1) in ( dom F) by A5, A10, A7, A47, FINSEQ_1:def 3;

            

            then

             A49: |(rv0, rv)| = |(rv0, ((l . (F /. j)) * rv0))| by A6, A47, A48, PARTFUN1:def 6

            .= (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by REAL_NS1:def 5;

            k < (k + 1) by XREAL_1: 29;

            then k < ( len F2) by A7, A11, A47, XXREAL_0: 2;

            then

             A50: (f . (k + 1)) = ((f . k) + v) by A14;

            reconsider fk = (f . k) as Element of ( REAL n) by REAL_NS1:def 6;

            (( Euclid_scalar n) . (v0,(f . k))) = 0 by A33, A47, XREAL_1: 29;

            then

             A51: |(rv0, fk)| = 0 by REAL_NS1:def 5;

             |(rv0, (fk + rv))| = ( |(rv0, fk)| + |(rv0, rv)|) by EUCLID_4: 28;

            hence Q[(k + 1)] by A50, A51, A49, REAL_NS1:def 5;

          end;

        end;

      end;

      

       A52: Q[ 0 ] by A16, FINSEQ_1: 1;

      

       A53: for i be Nat holds Q[i] from NAT_1:sch 2( A52, A34);

      for i be Nat st i >= j & i <= ( len F) holds (( Euclid_scalar n) . (v0,(f . i))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by A53;

      hence thesis by A12, A7, A11;

    end;

    theorem :: EUCLID_7:34

    

     Th33: for n be Element of NAT , f be FinSequence of ( REAL n), g be FinSequence of the carrier of ( REAL-US n) st f = g holds ( Sum f) = ( Sum g)

    proof

      let n be Element of NAT , f be FinSequence of ( REAL n), g be FinSequence of the carrier of ( REAL-US n);

      set V = ( REAL-US n);

      assume

       A1: f = g;

      now

        per cases ;

          case

           A2: ( len f) > 0 ;

          set g2 = ( accum f);

          

           A3: ( len f) = ( len g2) by Def10;

          

           A4: (f . 1) = (g2 . 1) by Def10;

          

           A5: ( Sum f) = (g2 . ( len f)) by A2, Def11;

          deffunc F( set) = ( IFIN ($1,(( len f) + 1),( IFEQ ($1, 0 ,( 0. V),(g2 /. $1))),( 0. V)));

          

           A6: for x be set st x in NAT holds F(x) in the carrier of V

          proof

            let x be set;

            assume x in NAT ;

            then

            reconsider nx = x as Element of NAT ;

            per cases ;

              suppose nx in (( len f) + 1);

              then

               A7: F(x) = ( IFEQ (x, 0 ,( 0. V),(g2 /. nx))) by MATRIX_7:def 1;

              per cases ;

                suppose x = 0 ;

                then F(x) = ( 0. V) by A7, FUNCOP_1:def 8;

                hence F(x) in the carrier of V;

              end;

                suppose

                 A8: x <> 0 ;

                

                 A9: the carrier of V = ( REAL n) by REAL_NS1:def 6;

                 F(x) = (g2 /. nx) by A7, A8, FUNCOP_1:def 8;

                hence F(x) in the carrier of V by A9;

              end;

            end;

              suppose not nx in (( len f) + 1);

              then F(x) = ( 0. V) by MATRIX_7:def 1;

              hence F(x) in the carrier of V;

            end;

          end;

          consider f3 be sequence of the carrier of V such that

           A10: for x be set st x in NAT holds (f3 . x) = F(x) from FUNCT_2:sch 11( A6);

          

           A11: for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f3 . (j + 1)) = ((f3 . j) + v)

          proof

            let j be Nat;

            

             A12: j in NAT by ORDINAL1:def 12;

            let v be Element of V;

            assume that

             A13: j < ( len g) and

             A14: v = (g . (j + 1));

            

             A15: (j + 1) <= ( len f) by A1, A13, NAT_1: 13;

            per cases ;

              suppose

               A16: j = 0 ;

              then (j + 1) < (( len f) + 1) by A2, XREAL_1: 6;

              then

               A17: (j + 1) in ( Segm (( len f) + 1)) by NAT_1: 44;

              

               A18: 0 in ( Segm (( len f) + 1)) by NAT_1: 44;

              

               A19: (f3 . j) = ( IFIN (j,(( len f) + 1),( IFEQ (j, 0 ,( 0. V),(g2 /. j))),( 0. V))) by A10, A12

              .= ( IFEQ (j, 0 ,( 0. V),(g2 /. j))) by A16, A18, MATRIX_7:def 1

              .= ( 0. V) by A16, FUNCOP_1:def 8;

              

              thus (f3 . (j + 1)) = ( IFIN ((j + 1),(( len f) + 1),( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))),( 0. V))) by A10

              .= ( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))) by A17, MATRIX_7:def 1

              .= (g2 /. 1) by A16, FUNCOP_1:def 8

              .= (g . (j + 1)) by A1, A3, A4, A15, A16, FINSEQ_4: 15

              .= ((f3 . j) + v) by A14, A19, RLVECT_1: 4;

            end;

              suppose

               A20: j <> 0 ;

              ( len f) < (( len f) + 1) by XREAL_1: 29;

              then j < (( len f) + 1) by A1, A13, XXREAL_0: 2;

              then

               A21: j in ( Segm (( len f) + 1)) by NAT_1: 44;

              

               A22: (f3 . j) = ( IFIN (j,(( len f) + 1),( IFEQ (j, 0 ,( 0. V),(g2 /. j))),( 0. V))) by A10, A12

              .= ( IFEQ (j, 0 ,( 0. V),(g2 /. j))) by A21, MATRIX_7:def 1

              .= (g2 /. j) by A20, FUNCOP_1:def 8;

              

               A23: ( 0 + 1) <= (j + 1) by NAT_1: 13;

              

               A24: ( 0 + 1) <= j by A20, NAT_1: 13;

              (j + 1) < (( len f) + 1) by A1, A13, XREAL_1: 6;

              then

               A25: (j + 1) in ( Segm (( len f) + 1)) by NAT_1: 44;

              

              thus (f3 . (j + 1)) = ( IFIN ((j + 1),(( len f) + 1),( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))),( 0. V))) by A10

              .= ( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))) by A25, MATRIX_7:def 1

              .= (g2 /. (j + 1)) by FUNCOP_1:def 8

              .= (g2 . (j + 1)) by A3, A15, A23, FINSEQ_4: 15

              .= ((g2 /. j) + (f /. (j + 1))) by A1, Def10, A13, A24

              .= ((f3 . j) + v) by A1, A14, A15, A23, A22, FINSEQ_4: 15;

            end;

          end;

          ( len f) < (( len f) + 1) by XREAL_1: 29;

          then

           A26: ( len f) in ( Segm (( len f) + 1)) by NAT_1: 44;

          

           A27: ( 0 + 1) <= ( len f) by A2, NAT_1: 13;

          

           A28: 0 in ( Segm (( len f) + 1)) by NAT_1: 44;

          

           A29: (f3 . 0 ) = ( IFIN ( 0 ,(( len f) + 1),( IFEQ ( 0 , 0 ,( 0. V),(g2 /. 0 ))),( 0. V))) by A10

          .= ( IFEQ ( 0 , 0 ,( 0. V),(g2 /. 0 ))) by A28, MATRIX_7:def 1

          .= ( 0. V) by FUNCOP_1:def 8;

          (f3 . ( len g)) = F(len) by A1, A10

          .= ( IFEQ (( len f), 0 ,( 0. V),(g2 /. ( len f)))) by A26, MATRIX_7:def 1

          .= (g2 /. ( len f)) by A2, FUNCOP_1:def 8

          .= ( Sum f) by A3, A5, A27, FINSEQ_4: 15;

          hence ex f2 be sequence of the carrier of V st ( Sum f) = (f2 . ( len g)) & (f2 . 0 ) = ( 0. V) & for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f2 . (j + 1)) = ((f2 . j) + v) by A29, A11;

        end;

          case

           A30: ( len f) <= 0 ;

          set f3 = ( NAT --> ( 0. V));

          

           A31: for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f3 . (j + 1)) = ((f3 . j) + v) by A1, A30;

          

           A32: (f3 . ( len g)) = ( 0. V) by FUNCOP_1: 7

          .= ( 0* n) by REAL_NS1:def 6;

          

           A33: (f3 . 0 ) = ( 0. V) by FUNCOP_1: 7;

          ( Sum f) = ( 0* n) by A30, Def11;

          hence ex f2 be sequence of the carrier of V st ( Sum f) = (f2 . ( len g)) & (f2 . 0 ) = ( 0. V) & for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f2 . (j + 1)) = ((f2 . j) + v) by A32, A33, A31;

        end;

      end;

      hence ( Sum f) = ( Sum g) by RLVECT_1:def 12;

    end;

    registration

      let A be set;

      cluster ( RealVectSpace A) -> constituted-Functions;

      coherence ;

    end

    registration

      let n;

      cluster ( RealVectSpace ( Seg n)) -> constituted-FinSeqs;

      coherence

      proof

        let a be Element of ( RealVectSpace ( Seg n));

        a is Element of ( REAL n) by FINSEQ_2: 93;

        hence thesis;

      end;

    end

    registration

      let A be set;

      cluster -> real-valued for Element of ( RealVectSpace A);

      coherence

      proof

        let a be Element of ( RealVectSpace A);

        a is Function of A, REAL or a is empty by FUNCT_2: 66;

        hence thesis;

      end;

    end

    registration

      let A be set;

      let x,y be VECTOR of ( RealVectSpace A), a,b be real-valued Function;

      identify a + b with x + y when x = a, y = b;

      compatibility

      proof

        

         A1: ( dom y) = A by FUNCT_2: 92;

        assume that

         A2: x = a and

         A3: y = b;

        ( dom (x + y)) = A by FUNCT_2: 92;

        then

         A4: for c be object st c in ( dom (x + y)) holds ((x + y) . c) = ((a . c) + (b . c)) by A2, A3, FUNCSDOM: 1;

        ( dom x) = A by FUNCT_2: 92;

        then ( dom (x + y)) = (( dom a) /\ ( dom b)) by A2, A3, A1, FUNCT_2: 92;

        hence thesis by A4, VALUED_1:def 1;

      end;

    end

    registration

      let A be set;

      let x be VECTOR of ( RealVectSpace A), y be real-valued Function, a,b be Element of REAL ;

      identify b (#) y with a * x when x = y, a = b;

      compatibility

      proof

        

         A1: ( dom x) = A by FUNCT_2: 92;

        assume that

         A2: x = y and

         A3: a = b;

        

         A4: ( dom (a * x)) = A by FUNCT_2: 92;

        then for c be object st c in ( dom (a * x)) holds ((a * x) . c) = (b * (y . c)) by A2, A3, FUNCSDOM: 4;

        hence thesis by A2, A4, A1, VALUED_1:def 5;

      end;

    end

    registration

      let A be set;

      let x be VECTOR of ( RealVectSpace A), a be real-valued Function;

      identify - a with - x when x = a;

      compatibility

      proof

        assume

         A1: x = a;

         A2:

        now

          let c be object;

          assume c in ( dom a);

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

          

          thus (( - x) . c) = ((( - jj) * x) . c) by RLVECT_1: 16

          .= (( - jj) * (a . c)) by A1, VALUED_1: 6

          .= ( - (a . c));

        end;

        ( dom ( - x)) = A by FUNCT_2: 92;

        hence thesis by A1, A2, FUNCT_2: 92, VALUED_1: 9;

      end;

    end

    registration

      let A be set;

      let x,y be VECTOR of ( RealVectSpace A), a,b be real-valued Function;

      identify a - b with x - y when x = a, y = b;

      compatibility ;

    end

    theorem :: EUCLID_7:35

    

     Th34: for X be Subspace of ( RealVectSpace ( Seg n)), x be Element of ( REAL n), a be Real st x in the carrier of X holds (a * x) in the carrier of X

    proof

      let X be Subspace of ( RealVectSpace ( Seg n)), x be Element of ( REAL n), a be Real;

      reconsider x1 = x as Element of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

      assume x in the carrier of X;

      then

       A1: x in X;

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

      (aa * x) = (aa * x1);

      then (a * x) in X by A1, RLSUB_1: 21;

      hence (a * x) in the carrier of X;

    end;

    theorem :: EUCLID_7:36

    

     Th35: for X be Subspace of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n) st x in the carrier of X & y in the carrier of X holds (x + y) in the carrier of X

    proof

      let X be Subspace of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n);

      assume that

       A1: x in the carrier of X and

       A2: y in the carrier of X;

      

       A3: y in X by A2;

      reconsider x1 = x, y1 = y as Element of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

      

       A4: (x1 + y1) = (x + y);

      x in X by A1;

      then (x + y) in X by A3, A4, RLSUB_1: 20;

      hence (x + y) in the carrier of X;

    end;

    theorem :: EUCLID_7:37

    for X be Subspace of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n), a,b be Real st x in the carrier of X & y in the carrier of X holds ((a * x) + (b * y)) in the carrier of X

    proof

      let X be Subspace of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n), a,b be Real;

      assume that

       A1: x in the carrier of X and

       A2: y in the carrier of X;

      

       A3: (b * y) in the carrier of X by A2, Th34;

      (a * x) in the carrier of X by A1, Th34;

      hence ((a * x) + (b * y)) in the carrier of X by A3, Th35;

    end;

    

     Lm4: for X be Subspace of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n), a be Real st x in the carrier of X & y in the carrier of X holds ((a * x) + y) in the carrier of X

    proof

      let X be Subspace of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n), a be Real;

      assume that

       A1: x in the carrier of X and

       A2: y in the carrier of X;

      (a * x) in the carrier of X by A1, Th34;

      hence ((a * x) + y) in the carrier of X by A2, Th35;

    end;

    theorem :: EUCLID_7:38

    for u,v be Element of ( REAL n) holds (( Euclid_scalar n) . (u,v)) = |(u, v)| by REAL_NS1:def 5;

    theorem :: EUCLID_7:39

    

     Th38: for F be FinSequence of the carrier of ( RealVectSpace ( Seg n)), Bn be Subset of ( RealVectSpace ( Seg n)), v0 be Element of ( RealVectSpace ( Seg n)), l be Linear_Combination of Bn st F is one-to-one & Bn is R-orthogonal & ( rng F) = ( Carrier l) & v0 in Bn & j in ( dom (l (#) F)) & v0 = (F . j) holds (( Euclid_scalar n) . (v0,( Sum (l (#) F)))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0)))

    proof

      let F be FinSequence of the carrier of ( RealVectSpace ( Seg n)), Bn be Subset of ( RealVectSpace ( Seg n)), v0 be Element of ( RealVectSpace ( Seg n)), l be Linear_Combination of Bn;

      assume that

       A1: F is one-to-one and

       A2: Bn is R-orthogonal and

       A3: ( rng F) = ( Carrier l) and

       A4: v0 in Bn and

       A5: j in ( dom (l (#) F)) and

       A6: v0 = (F . j);

      

       A7: ( len (l (#) F)) = ( len F) by RLVECT_2:def 7;

      

      then

       A8: ( dom (l (#) F)) = ( Seg ( len F)) by FINSEQ_1:def 3

      .= ( dom F) by FINSEQ_1:def 3;

      reconsider F2 = (l (#) F) as FinSequence of the carrier of ( RealVectSpace ( Seg n));

      reconsider rv0 = v0 as Element of ( REAL n) by FINSEQ_2: 93;

      consider f be sequence of the carrier of ( RealVectSpace ( Seg n)) such that

       A9: ( Sum F2) = (f . ( len F2)) and

       A10: (f . 0 ) = ( 0. ( RealVectSpace ( Seg n))) and

       A11: for j2 be Nat holds for v be Element of ( RealVectSpace ( Seg n)) st j2 < ( len F2) & v = (F2 . (j2 + 1)) holds (f . (j2 + 1)) = ((f . j2) + v) by RLVECT_1:def 12;

      defpred Q[ Nat] means $1 >= j & $1 <= ( len F) implies (( Euclid_scalar n) . (v0,(f . $1))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0)));

      defpred P[ Nat] means $1 < j implies (( Euclid_scalar n) . (v0,(f . $1))) = 0 ;

      (( Euclid_scalar n) . (v0,(f . 0 ))) = |(rv0, ( 0* n))| by A10, REAL_NS1:def 5

      .= 0 by EUCLID_4: 18;

      then

       A12: P[ 0 ];

      

       A13: ( dom (l (#) F)) = ( Seg ( len (l (#) F))) by FINSEQ_1:def 3;

      then

       A14: j <= ( len F) by A5, A7, FINSEQ_1: 1;

      

       A15: ( Carrier l) c= Bn by RLVECT_2:def 6;

      

       A16: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A17: P[k];

        now

          per cases ;

            case

             A18: k < ( len F2);

            

             A19: 1 <= (k + 1) by NAT_1: 11;

            (k + 1) <= ( len F2) by A18, NAT_1: 13;

            then (k + 1) in ( Seg ( len F2)) by A19, FINSEQ_1: 1;

            then (k + 1) in ( dom F2) by FINSEQ_1:def 3;

            then (F2 . (k + 1)) in ( rng F2) by FUNCT_1:def 3;

            then

            reconsider v = (F2 . (k + 1)) as Element of ( RealVectSpace ( Seg n));

            reconsider rv = v as Element of ( REAL n) by FINSEQ_2: 93;

            reconsider fk = (f . k) as Element of ( REAL n) by FINSEQ_2: 93;

            per cases ;

              suppose

               A20: (k + 1) < j;

              

               A21: 1 <= (k + 1) by NAT_1: 11;

              (k + 1) < ( len F) by A14, A20, XXREAL_0: 2;

              then (k + 1) in ( Seg ( len F)) by A21, FINSEQ_1: 1;

              then

               A22: (k + 1) in ( dom F) by FINSEQ_1:def 3;

              then

               A23: (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

              then

               A24: rv0 <> (F /. (k + 1)) by A1, A5, A6, A8, A20, A22, FUNCT_1:def 4;

              k < (k + 1) by XREAL_1: 29;

              then

               A25: |(rv0, fk)| = 0 by A17, A20, REAL_NS1:def 5, XXREAL_0: 2;

              reconsider fk1 = (F /. (k + 1)) as Element of ( REAL n) by FINSEQ_2: 93;

              

               A26: |(rv0, (fk + rv))| = ( |(rv0, fk)| + |(rv0, rv)|) by EUCLID_4: 28;

              

               A27: (F /. (k + 1)) in ( rng F) by A22, A23, FUNCT_1:def 3;

              v = ((l . (F /. (k + 1))) * (F /. (k + 1))) by A8, A22, RLVECT_2:def 7;

              

              then |(rv0, rv)| = ((l . (F /. (k + 1))) * |(rv0, fk1)|) by EUCLID_4: 22

              .= ((l . (F /. (k + 1))) * 0 ) by A2, A3, A4, A15, A27, A24

              .= 0 ;

              then (( Euclid_scalar n) . (v0,((f . k) + v))) = 0 by A25, A26, REAL_NS1:def 5;

              hence P[(k + 1)] by A11, A18;

            end;

              suppose (k + 1) >= j;

              hence P[(k + 1)];

            end;

          end;

            case

             A28: k >= ( len F2);

            (k + 1) > k by XREAL_1: 29;

            then (k + 1) > ( len F2) by A28, XXREAL_0: 2;

            hence P[(k + 1)] by A7, A14, XXREAL_0: 2;

          end;

        end;

        hence P[(k + 1)];

      end;

      

       A29: for i be Nat holds P[i] from NAT_1:sch 2( A12, A16);

      

       A30: for i be Nat st i < j holds (( Euclid_scalar n) . (v0,(f . i))) = 0 by A29;

      

       A31: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        assume

         A32: Q[k];

        per cases ;

          suppose (k + 1) < j;

          hence Q[(k + 1)];

        end;

          suppose

           A33: (k + 1) >= j;

          per cases by A33, XXREAL_0: 1;

            suppose

             A34: (k + 1) > j;

            per cases ;

              suppose

               A35: (k + 1) <= ( len F2);

              1 <= (k + 1) by NAT_1: 11;

              then

               A36: (k + 1) in ( Seg ( len F2)) by A35, FINSEQ_1: 1;

              then

               A37: (k + 1) in ( dom F) by A7, FINSEQ_1:def 3;

              then

               A38: (F /. (k + 1)) = (F . (k + 1)) by PARTFUN1:def 6;

              then

               A39: (F /. (k + 1)) in ( rng F) by A37, FUNCT_1:def 3;

              (k + 1) in ( dom F2) by A36, FINSEQ_1:def 3;

              then (F2 . (k + 1)) in ( rng F2) by FUNCT_1:def 3;

              then

              reconsider v = (F2 . (k + 1)) as Element of ( RealVectSpace ( Seg n));

              reconsider rv = v as Element of ( REAL n) by FINSEQ_2: 93;

              reconsider fk1 = (F /. (k + 1)) as Element of ( REAL n) by FINSEQ_2: 93;

              reconsider fk = (f . k) as Element of ( REAL n) by FINSEQ_2: 93;

              

               A40: |(rv0, (fk + rv))| = ( |(rv0, fk)| + |(rv0, rv)|) by EUCLID_4: 28;

              

               A41: rv0 <> (F /. (k + 1)) by A1, A5, A6, A8, A34, A37, A38, FUNCT_1:def 4;

              v = ((l . (F /. (k + 1))) * (F /. (k + 1))) by A8, A37, RLVECT_2:def 7;

              

              then

               A42: |(rv0, rv)| = ((l . (F /. (k + 1))) * |(rv0, fk1)|) by EUCLID_4: 22

              .= ((l . (F /. (k + 1))) * 0 ) by A2, A3, A4, A15, A39, A41

              .= 0 ;

              k < (k + 1) by XREAL_1: 29;

              then

               A43: k < ( len F2) by A35, XXREAL_0: 2;

              then |(rv0, fk)| = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by A32, A34, NAT_1: 13, REAL_NS1:def 5, RLVECT_2:def 7;

              then (( Euclid_scalar n) . (v0,((f . k) + v))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by A40, A42, REAL_NS1:def 5;

              hence Q[(k + 1)] by A11, A43;

            end;

              suppose (k + 1) > ( len F2);

              hence Q[(k + 1)] by RLVECT_2:def 7;

            end;

          end;

            suppose

             A44: (k + 1) = j;

            then (F2 . (k + 1)) in ( rng F2) by A5, FUNCT_1:def 3;

            then

            reconsider v = (F2 . (k + 1)) as Element of ( RealVectSpace ( Seg n));

            

             A45: v = ((l . (F /. (k + 1))) * (F /. (k + 1))) by A5, A44, RLVECT_2:def 7;

            reconsider rv = v as Element of ( REAL n) by FINSEQ_2: 93;

            (k + 1) in ( dom F) by A5, A13, A7, A44, FINSEQ_1:def 3;

            

            then

             A46: |(rv0, rv)| = |(rv0, ((l . (F /. j)) * rv0))| by A6, A44, A45, PARTFUN1:def 6

            .= (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by REAL_NS1:def 5;

            reconsider fk = (f . k) as Element of ( REAL n) by FINSEQ_2: 93;

            (( Euclid_scalar n) . (v0,(f . k))) = 0 by A30, A44, XREAL_1: 29;

            then

             A47: |(rv0, fk)| = 0 by REAL_NS1:def 5;

            k < (k + 1) by XREAL_1: 29;

            then

             A48: k < ( len F2) by A7, A14, A44, XXREAL_0: 2;

             |(rv0, (fk + rv))| = ( |(rv0, fk)| + |(rv0, rv)|) by EUCLID_4: 28;

            then (( Euclid_scalar n) . (v0,((f . k) + v))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by A47, A46, REAL_NS1:def 5;

            hence Q[(k + 1)] by A11, A48;

          end;

        end;

      end;

      

       A49: Q[ 0 ] by A5, A13, FINSEQ_1: 1;

      

       A50: for i be Nat holds Q[i] from NAT_1:sch 2( A49, A31);

      for i be Nat st i >= j & i <= ( len F) holds (( Euclid_scalar n) . (v0,(f . i))) = (( Euclid_scalar n) . (v0,((l . (F /. j)) * v0))) by A50;

      hence thesis by A9, A7, A14;

    end;

    registration

      let n;

      cluster R-orthonormal -> linearly-independent for Subset of ( RealVectSpace ( Seg n));

      coherence

      proof

        let Bn be Subset of ( RealVectSpace ( Seg n));

        assume

         A1: Bn is R-orthonormal;

        let l be Linear_Combination of Bn;

        assume

         A2: ( Sum l) = ( 0. ( RealVectSpace ( Seg n)));

        set v0 = the Element of ( Carrier l);

        consider F be FinSequence of the carrier of ( RealVectSpace ( Seg n)) such that

         A3: F is one-to-one and

         A4: ( rng F) = ( Carrier l) and

         A5: ( Sum l) = ( Sum (l (#) F)) by RLVECT_2:def 8;

        assume

         A6: ( Carrier l) <> {} ;

        then

         A7: v0 in ( Carrier l);

        then v0 in { v2 where v2 be Element of ( RealVectSpace ( Seg n)) : (l . v2) <> 0 } by RLVECT_2:def 4;

        then

        consider v be Element of ( RealVectSpace ( Seg n)) such that

         A8: v0 = v and (l . v) <> 0 ;

        reconsider xv = v as Element of ( REAL n) by FINSEQ_2: 93;

        

         A9: (( Euclid_scalar n) . (v,( Sum (l (#) F)))) = |(xv, ( 0* n))| by A2, A5, REAL_NS1:def 5

        .= 0 by EUCLID_4: 18;

        consider x0 be object such that

         A10: x0 in ( dom F) and

         A11: v0 = (F . x0) by A6, A4, FUNCT_1:def 3;

        reconsider nx0 = x0 as Element of NAT by A10;

        (F . x0) = (F /. x0) by A10, PARTFUN1:def 6;

        then (F /. nx0) in ( rng F) by A10, FUNCT_1:def 3;

        then (F /. nx0) in { v3 where v3 be Element of ( RealVectSpace ( Seg n)) : (l . v3) <> 0 } by A4, RLVECT_2:def 4;

        then

         A12: ex v3 be Element of ( RealVectSpace ( Seg n)) st v3 = (F /. nx0) & (l . v3) <> 0 ;

        

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

        

         A14: ( Carrier l) c= Bn by RLVECT_2:def 6;

        ( len (l (#) F)) = ( len F) by RLVECT_2:def 7;

        then nx0 in ( dom (l (#) F)) by A10, A13, FINSEQ_1:def 3;

        

        then (( Euclid_scalar n) . (v,( Sum (l (#) F)))) = (( Euclid_scalar n) . (v,((l . (F /. nx0)) * v))) by A1, A14, A7, A8, A3, A4, A11, Th38

        .= |(xv, ((l . (F /. nx0)) * xv))| by REAL_NS1:def 5

        .= ((l . (F /. nx0)) * |(xv, xv)|) by EUCLID_4: 22

        .= ((l . (F /. nx0)) * ( |.xv.| ^2 )) by EUCLID_2: 4

        .= ((l . (F /. nx0)) * (1 ^2 )) by A1, A14, A7, A8, Def4

        .= (l . (F /. nx0));

        hence contradiction by A12, A9;

      end;

    end

    registration

      let n be Element of NAT ;

      cluster R-orthonormal -> linearly-independent for Subset of ( REAL-US n);

      coherence

      proof

        let Bn be Subset of ( REAL-US n);

        assume

         A1: Bn is R-orthonormal;

        let l be Linear_Combination of Bn;

        assume

         A2: ( Sum l) = ( 0. ( REAL-US n));

        set v0 = the Element of ( Carrier l);

        consider F be FinSequence of the carrier of ( REAL-US n) such that

         A3: F is one-to-one and

         A4: ( rng F) = ( Carrier l) and

         A5: ( Sum l) = ( Sum (l (#) F)) by RLVECT_2:def 8;

        assume

         A6: ( Carrier l) <> {} ;

        then

         A7: v0 in ( Carrier l);

        then v0 in { v2 where v2 be Element of ( REAL-US n) : (l . v2) <> 0 } by RLVECT_2:def 4;

        then

        consider v be Element of ( REAL-US n) such that

         A8: v0 = v and (l . v) <> 0 ;

        reconsider xv = v as Element of ( REAL n) by REAL_NS1:def 6;

        ( 0. ( REAL-US n)) = ( 0* n) by REAL_NS1:def 6;

        

        then

         A9: (( Euclid_scalar n) . (v,( Sum (l (#) F)))) = |(xv, ( 0* n))| by A2, A5, REAL_NS1:def 5

        .= 0 by EUCLID_4: 18;

        consider x0 be object such that

         A10: x0 in ( dom F) and

         A11: v0 = (F . x0) by A6, A4, FUNCT_1:def 3;

        reconsider nx0 = x0 as Element of NAT by A10;

        (F . x0) = (F /. x0) by A10, PARTFUN1:def 6;

        then (F /. nx0) in ( rng F) by A10, FUNCT_1:def 3;

        then (F /. nx0) in { v3 where v3 be Element of ( REAL-US n) : (l . v3) <> 0 } by A4, RLVECT_2:def 4;

        then

         A12: ex v3 be Element of ( REAL-US n) st v3 = (F /. nx0) & (l . v3) <> 0 ;

        

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

        

         A14: ( Carrier l) c= Bn by RLVECT_2:def 6;

        ( len (l (#) F)) = ( len F) by RLVECT_2:def 7;

        then nx0 in ( dom (l (#) F)) by A10, A13, FINSEQ_1:def 3;

        

        then (( Euclid_scalar n) . (v,( Sum (l (#) F)))) = (( Euclid_scalar n) . (v,((l . (F /. nx0)) * v))) by A1, A14, A7, A8, A3, A4, A11, Th32

        .= |(xv, ((l . (F /. nx0)) * xv))| by REAL_NS1:def 5

        .= ((l . (F /. nx0)) * |(xv, xv)|) by EUCLID_4: 22

        .= ((l . (F /. nx0)) * ( |.xv.| ^2 )) by EUCLID_2: 4

        .= ((l . (F /. nx0)) * (1 ^2 )) by A1, A14, A7, A8, Def4

        .= (l . (F /. nx0));

        hence contradiction by A12, A9;

      end;

    end

    theorem :: EUCLID_7:40

    

     Th39: for Bn be Subset of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n), a be Real st Bn is linearly-independent & x in Bn & y in Bn & y = (a * x) holds x = y

    proof

      let Bn be Subset of ( RealVectSpace ( Seg n)), x,y be Element of ( REAL n), a be Real;

      assume that

       A1: Bn is linearly-independent and

       A2: x in Bn and

       A3: y in Bn and

       A4: y = (a * x);

      reconsider x0 = x, y0 = y as Element of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

      reconsider A = {y0, x0} as Subset of ( RealVectSpace ( Seg n));

      A c= Bn by A2, A3, TARSKI:def 2;

      then

       A5: A is linearly-independent by A1, RLVECT_3: 5;

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

      y0 = (aa * x0) by A4;

      hence x = y by A5, RLVECT_3: 12;

    end;

     Lm5:

    now

      let n;

      thus ( RN_Base n) is finite & ( card ( RN_Base n)) = n

      proof

        per cases ;

          suppose n is zero;

          hence thesis;

        end;

          suppose n is non zero;

          then

          reconsider n as non zero Nat;

          defpred P[ object, object] means for i be Element of NAT st i = $1 holds $2 = ( Base_FinSeq (n,i));

          

           A1: for x be object st x in ( Seg n) holds ex y be object st P[x, y]

          proof

            let x be object;

            assume x in ( Seg n);

            then

            reconsider j = x as Element of NAT ;

            for i be Element of NAT st i = j holds ( Base_FinSeq (n,j)) = ( Base_FinSeq (n,i));

            hence ex y be object st P[x, y];

          end;

          consider f be Function such that

           A2: ( dom f) = ( Seg n) & for x2 be object st x2 in ( Seg n) holds P[x2, (f . x2)] from CLASSES1:sch 1( A1);

          

           A3: ( rng f) c= ( RN_Base n)

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

             A4: x in ( dom f) and

             A5: y = (f . x) by FUNCT_1:def 3;

            reconsider nx = x as Element of NAT by A2, A4;

            

             A6: nx <= n by A2, A4, FINSEQ_1: 1;

            

             A7: (f . x) = ( Base_FinSeq (n,nx)) by A2, A4;

            1 <= nx by A2, A4, FINSEQ_1: 1;

            hence y in ( RN_Base n) by A5, A6, A7;

          end;

          then

          reconsider f2 = f as Function of ( Seg n), ( RN_Base n) by A2, FUNCT_2: 2;

          for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume that

             A8: x1 in ( dom f) and

             A9: x2 in ( dom f) and

             A10: (f . x1) = (f . x2);

            reconsider nx1 = x1, nx2 = x2 as Element of NAT by A2, A8, A9;

            

             A11: nx1 <= n by A2, A8, FINSEQ_1: 1;

            

             A12: (f . x2) = ( Base_FinSeq (n,nx2)) by A2, A9;

            

             A13: (f . x1) = ( Base_FinSeq (n,nx1)) by A2, A8;

            1 <= nx1 by A2, A8, FINSEQ_1: 1;

            hence x1 = x2 by A10, A11, A13, A12, Th24;

          end;

          then

           A14: f2 is one-to-one by FUNCT_1:def 4;

          ( RN_Base n) c= ( rng f)

          proof

            let y be object;

            assume y in ( RN_Base n);

            then

            consider i be Element of NAT such that

             A15: y = ( Base_FinSeq (n,i)) and

             A16: 1 <= i and

             A17: i <= n;

            

             A18: i in ( Seg n) by A16, A17, FINSEQ_1: 1;

            then (f . i) = ( Base_FinSeq (n,i)) by A2;

            hence y in ( rng f) by A2, A15, A18, FUNCT_1:def 3;

          end;

          then ( rng f) = ( RN_Base n) by A3, XBOOLE_0:def 10;

          then f2 is onto by FUNCT_2:def 3;

          then ( card ( Seg n)) = ( card ( RN_Base n)) by A14, Lm1;

          hence thesis by FINSEQ_1: 57;

        end;

      end;

    end;

    begin

    registration

      let n;

      cluster ( RN_Base n) -> finite;

      coherence by Lm5;

    end

    theorem :: EUCLID_7:41

    ( card ( RN_Base n)) = n by Lm5;

    theorem :: EUCLID_7:42

    

     Th41: for f be FinSequence of ( REAL n), g be FinSequence of the carrier of ( RealVectSpace ( Seg n)) st f = g holds ( Sum f) = ( Sum g)

    proof

      let f be FinSequence of ( REAL n), g be FinSequence of the carrier of ( RealVectSpace ( Seg n));

      assume

       A1: f = g;

      set V = ( RealVectSpace ( Seg n));

      

       A2: ( REAL n) = the carrier of V by FINSEQ_2: 93;

      now

        per cases ;

          case

           A3: ( len f) > 0 ;

          set g2 = ( accum f);

          

           A4: ( len f) = ( len g2) by Def10;

          

           A5: (f . 1) = (g2 . 1) by Def10;

          

           A6: ( Sum f) = (g2 . ( len f)) by Def11, A3;

          deffunc F( set) = ( IFIN ($1,(( len f) + 1),( IFEQ ($1, 0 ,( 0. V),(g2 /. $1))),( 0. V)));

          

           A7: for x be set st x in NAT holds F(x) in the carrier of V

          proof

            let x be set;

            assume x in NAT ;

            then

            reconsider nx = x as Element of NAT ;

            per cases ;

              suppose nx in (( len f) + 1);

              then

               A8: F(x) = ( IFEQ (x, 0 ,( 0. V),(g2 /. nx))) by MATRIX_7:def 1;

              per cases ;

                suppose x = 0 ;

                then F(x) = ( 0. V) by A8, FUNCOP_1:def 8;

                hence F(x) in the carrier of V;

              end;

                suppose x <> 0 ;

                then F(x) = (g2 /. nx) by A8, FUNCOP_1:def 8;

                hence F(x) in the carrier of V by A2;

              end;

            end;

              suppose not nx in (( len f) + 1);

              then F(x) = ( 0. V) by MATRIX_7:def 1;

              hence F(x) in the carrier of V;

            end;

          end;

          consider f3 be sequence of the carrier of V such that

           A9: for x be set st x in NAT holds (f3 . x) = F(x) from FUNCT_2:sch 11( A7);

          

           A10: for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f3 . (j + 1)) = ((f3 . j) + v)

          proof

            let j be Nat;

            

             A11: j in NAT by ORDINAL1:def 12;

            let v be Element of V;

            assume that

             A12: j < ( len g) and

             A13: v = (g . (j + 1));

            

             A14: (j + 1) <= ( len f) by A1, A12, NAT_1: 13;

            per cases ;

              suppose

               A15: j = 0 ;

              then (j + 1) < (( len f) + 1) by A3, XREAL_1: 6;

              then

               A16: (j + 1) in ( Segm (( len f) + 1)) by NAT_1: 44;

              

               A17: 0 in ( Segm (( len f) + 1)) by NAT_1: 44;

              

               A18: (f3 . j) = ( IFIN (j,(( len f) + 1),( IFEQ (j, 0 ,( 0. V),(g2 /. j))),( 0. V))) by A9, A11

              .= ( IFEQ (j, 0 ,( 0. V),(g2 /. j))) by A15, A17, MATRIX_7:def 1

              .= ( 0. V) by A15, FUNCOP_1:def 8;

              

              thus (f3 . (j + 1)) = ( IFIN ((j + 1),(( len f) + 1),( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))),( 0. V))) by A9

              .= ( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))) by A16, MATRIX_7:def 1

              .= (g2 /. 1) by A15, FUNCOP_1:def 8

              .= (g . (j + 1)) by A1, A4, A5, A14, A15, FINSEQ_4: 15

              .= ((f3 . j) + v) by A13, A18, RLVECT_1: 4;

            end;

              suppose

               A19: j <> 0 ;

              ( len f) < (( len f) + 1) by XREAL_1: 29;

              then j < (( len f) + 1) by A1, A12, XXREAL_0: 2;

              then

               A20: j in ( Segm (( len f) + 1)) by NAT_1: 44;

              

               A21: (f3 . j) = ( IFIN (j,(( len f) + 1),( IFEQ (j, 0 ,( 0. V),(g2 /. j))),( 0. V))) by A9, A11

              .= ( IFEQ (j, 0 ,( 0. V),(g2 /. j))) by A20, MATRIX_7:def 1

              .= (g2 /. j) by A19, FUNCOP_1:def 8;

              

               A22: ( 0 + 1) <= (j + 1) by NAT_1: 13;

              

               A23: ( 0 + 1) <= j by A19, NAT_1: 13;

              (j + 1) < (( len f) + 1) by A1, A12, XREAL_1: 6;

              then

               A24: (j + 1) in ( Segm (( len f) + 1)) by NAT_1: 44;

              

              thus (f3 . (j + 1)) = ( IFIN ((j + 1),(( len f) + 1),( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))),( 0. V))) by A9

              .= ( IFEQ ((j + 1), 0 ,( 0. V),(g2 /. (j + 1)))) by A24, MATRIX_7:def 1

              .= (g2 /. (j + 1)) by FUNCOP_1:def 8

              .= (g2 . (j + 1)) by A4, A14, A22, FINSEQ_4: 15

              .= ((g2 /. j) + (f /. (j + 1))) by A1, Def10, A12, A23

              .= ((f3 . j) + v) by A1, A13, A14, A22, A21, FINSEQ_4: 15;

            end;

          end;

          ( len f) < (( len f) + 1) by XREAL_1: 29;

          then

           A25: ( len f) in ( Segm (( len f) + 1)) by NAT_1: 44;

          

           A26: ( 0 + 1) <= ( len f) by A3, NAT_1: 13;

          

           A27: 0 in ( Segm (( len f) + 1)) by NAT_1: 44;

          

           A28: (f3 . 0 ) = ( IFIN ( 0 ,(( len f) + 1),( IFEQ ( 0 , 0 ,( 0. V),(g2 /. 0 ))),( 0. V))) by A9

          .= ( IFEQ ( 0 , 0 ,( 0. V),(g2 /. 0 ))) by A27, MATRIX_7:def 1

          .= ( 0. V) by FUNCOP_1:def 8;

          (f3 . ( len g)) = F(len) by A1, A9

          .= ( IFEQ (( len f), 0 ,( 0. V),(g2 /. ( len f)))) by A25, MATRIX_7:def 1

          .= (g2 /. ( len f)) by A3, FUNCOP_1:def 8

          .= ( Sum f) by A4, A6, A26, FINSEQ_4: 15;

          hence ex f2 be sequence of the carrier of V st ( Sum f) = (f2 . ( len g)) & (f2 . 0 ) = ( 0. V) & for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f2 . (j + 1)) = ((f2 . j) + v) by A28, A10;

        end;

          case

           A29: ( len f) <= 0 ;

          set f3 = ( NAT --> ( 0. V));

          

           A30: for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f3 . (j + 1)) = ((f3 . j) + v) by A1, A29;

          

           A31: (f3 . ( len g)) = ( 0* n) by FUNCOP_1: 7;

          

           A32: (f3 . 0 ) = ( 0. V) by FUNCOP_1: 7;

          ( Sum f) = ( 0* n) by A29, Def11;

          hence ex f2 be sequence of the carrier of V st ( Sum f) = (f2 . ( len g)) & (f2 . 0 ) = ( 0. V) & for j be Nat holds for v be Element of V st j < ( len g) & v = (g . (j + 1)) holds (f2 . (j + 1)) = ((f2 . j) + v) by A31, A32, A30;

        end;

      end;

      hence ( Sum f) = ( Sum g) by RLVECT_1:def 12;

    end;

    theorem :: EUCLID_7:43

    

     Th42: for x0 be Element of ( RealVectSpace ( Seg n)), B be Subset of ( RealVectSpace ( Seg n)) st B = ( RN_Base n) holds ex l be Linear_Combination of B st x0 = ( Sum l)

    proof

      let x0 be Element of ( RealVectSpace ( Seg n)), B be Subset of ( RealVectSpace ( Seg n));

      reconsider x1 = x0 as Element of ( REAL n) by FINSEQ_2: 93;

      

       A1: ( REAL n) = the carrier of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

      assume

       A2: B = ( RN_Base n);

      

       A3: { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) } c= B

      proof

        let y be object;

        assume y in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) };

        then ex x be Element of ( REAL n) st y = x & ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i));

        hence y in B by A2;

      end;

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

      proof

        let y be object;

        assume y in B;

        then ex i2 be Element of NAT st y = ( Base_FinSeq (n,i2)) & 1 <= i2 & i2 <= n by A2;

        hence y in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) };

      end;

      then

       A4: B = { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) } by A3, XBOOLE_0:def 10;

      

       A5: { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 } c= B

      proof

        let x2 be object;

        assume x2 in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 };

        then ex x be Element of ( REAL n) st x = x2 & ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 ;

        hence x2 in B by A4;

      end;

      then

      reconsider B0 = { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 } as Subset of ( RealVectSpace ( Seg n)) by XBOOLE_1: 1;

      

       A6: ( dom ( ProjFinSeq x1)) = ( Seg ( len ( ProjFinSeq x1))) by FINSEQ_1:def 3

      .= ( Seg n) by Def12;

      defpred R[ object, object] means $1 in B0 implies ex i be Element of NAT st $2 = i & 1 <= i & i <= n & $1 = ( Base_FinSeq (n,i));

      

       A7: for x be object st x in B0 holds ex y be object st y in ( Seg n) & R[x, y]

      proof

        let x be object;

        assume x in B0;

        then

        consider x2 be Element of ( REAL n) such that

         A8: x = x2 and

         A9: ex i be Element of NAT st 1 <= i & i <= n & x2 = ( Base_FinSeq (n,i)) & |(x1, x2)| <> 0 ;

        consider i0 be Element of NAT such that

         A10: 1 <= i0 and

         A11: i0 <= n and

         A12: x2 = ( Base_FinSeq (n,i0)) and |(x1, x2)| <> 0 by A9;

        i0 in ( Seg n) by A10, A11, FINSEQ_1: 1;

        hence ex y be object st y in ( Seg n) & R[x, y] by A8, A10, A11, A12;

      end;

      consider f be Function of B0, ( Seg n) such that

       A13: for x be object st x in B0 holds R[x, (f . x)] from FUNCT_2:sch 1( A7);

      defpred Q[ object, object] means ($1 in B0 implies (for i be Element of NAT st 1 <= i & i <= n & $1 = ( Base_FinSeq (n,i)) holds $2 = |(x1, ( Base_FinSeq (n,i)))|)) & ( not $1 in B0 implies $2 = 0 );

      

       A14: for x be object st x in the carrier of ( RealVectSpace ( Seg n)) holds ex y be object st y in REAL & Q[x, y]

      proof

        let x be object;

        assume x in the carrier of ( RealVectSpace ( Seg n));

        per cases ;

          suppose

           A15: x in B0;

          then

          consider x2 be Element of ( REAL n) such that

           A16: x2 = x and ex i be Element of NAT st 1 <= i & i <= n & x2 = ( Base_FinSeq (n,i)) & |(x1, x2)| <> 0 ;

          reconsider y0 = |(x1, x2)| as Element of REAL ;

          for i2 be Element of NAT st 1 <= i2 & i2 <= n & x = ( Base_FinSeq (n,i2)) holds y0 = |(x1, ( Base_FinSeq (n,i2)))| by A16;

          hence ex y be object st y in REAL & Q[x, y] by A15;

        end;

          suppose not x in B0;

          hence ex y be object st y in REAL & Q[x, y] by Lm3;

        end;

      end;

      consider l2 be Function of the carrier of ( RealVectSpace ( Seg n)), REAL such that

       A17: for x be object st x in the carrier of ( RealVectSpace ( Seg n)) holds Q[x, (l2 . x)] from FUNCT_2:sch 1( A14);

      

       A18: l2 is Element of ( Funcs (the carrier of ( RealVectSpace ( Seg n)), REAL )) by FUNCT_2: 8;

      for v be Element of ( RealVectSpace ( Seg n)) st not v in B0 holds (l2 . v) = 0 by A17;

      then

      reconsider l3 = l2 as Linear_Combination of ( RealVectSpace ( Seg n)) by A2, A5, A18, RLVECT_2:def 3;

      ( Carrier l3) c= B0

      proof

        let x be object;

        assume x in ( Carrier l3);

        then x in { v where v be Element of ( RealVectSpace ( Seg n)) : (l3 . v) <> 0 } by RLVECT_2:def 4;

        then ex v be Element of ( RealVectSpace ( Seg n)) st x = v & (l3 . v) <> 0 ;

        hence x in B0 by A17;

      end;

      then

      reconsider l0 = l3 as Linear_Combination of B0 by RLVECT_2:def 6;

      

       A19: ( Carrier l0) c= B0 by RLVECT_2:def 6;

      then ( Carrier l0) c= B by A5;

      then

      reconsider l2 = l0 as Linear_Combination of B by RLVECT_2:def 6;

      

       A20: B0 c= ( Carrier l0)

      proof

        let x be object;

        assume

         A21: x in B0;

        then

        consider x6 be Element of ( REAL n) such that

         A22: x = x6 and

         A23: ex i be Element of NAT st 1 <= i & i <= n & x6 = ( Base_FinSeq (n,i)) & |(x1, x6)| <> 0 ;

        reconsider x66 = x6 as Element of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

        consider i8 be Element of NAT such that 1 <= i8 and i8 <= n and

         A24: x6 = ( Base_FinSeq (n,i8)) and |(x1, x6)| <> 0 by A23;

        (l0 . x66) = |(x1, ( Base_FinSeq (n,i8)))| by A17, A21, A22, A23, A24;

        then x in { v where v be Element of ( RealVectSpace ( Seg n)) : (l0 . v) <> 0 } by A22, A23, A24;

        hence x in ( Carrier l0) by RLVECT_2:def 4;

      end;

      for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A25: x1 in ( dom f) and

         A26: x2 in ( dom f) and

         A27: (f . x1) = (f . x2);

        

         A28: ex i2 be Element of NAT st (f . x2) = i2 & 1 <= i2 & i2 <= n & x2 = ( Base_FinSeq (n,i2)) by A13, A26;

        ex i1 be Element of NAT st (f . x1) = i1 & 1 <= i1 & i1 <= n & x1 = ( Base_FinSeq (n,i1)) by A13, A25;

        hence x1 = x2 by A27, A28;

      end;

      then

       A29: f is one-to-one by FUNCT_1:def 4;

      

       A30: ( Seg n) = {} implies B0 = {}

      proof

        assume

         A31: ( Seg n) = {} ;

        now

          set y = the Element of B0;

          assume B0 <> {} ;

          then y in B0;

          then ex x be Element of ( REAL n) st x = y & ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 ;

          hence contradiction by A31;

        end;

        hence B0 = {} ;

      end;

      

       A32: for i3 be Element of NAT st i3 in ( dom ( ProjFinSeq x1)) & not i3 in ( rng ( Sgm ( rng f))) holds (( ProjFinSeq x1) . i3) = ( 0* n)

      proof

        let i3 be Element of NAT ;

        assume that

         A33: i3 in ( dom ( ProjFinSeq x1)) and

         A34: not i3 in ( rng ( Sgm ( rng f)));

        

         A35: i3 in ( Seg ( len ( ProjFinSeq x1))) by A33, FINSEQ_1:def 3;

        then

         A36: 1 <= i3 by FINSEQ_1: 1;

        ( len ( ProjFinSeq x1)) = n by Def12;

        then

         A37: i3 <= n by A35, FINSEQ_1: 1;

        

         A38: not i3 in ( rng f) by A34, FINSEQ_1:def 13;

         A39:

        now

          assume |(x1, ( Base_FinSeq (n,i3)))| <> 0 ;

          then

           A40: ( Base_FinSeq (n,i3)) in B0 by A36, A37;

          then

          consider i5 be Element of NAT such that

           A41: (f . ( Base_FinSeq (n,i3))) = i5 and 1 <= i5 and i5 <= n and

           A42: ( Base_FinSeq (n,i3)) = ( Base_FinSeq (n,i5)) by A13;

          

           A43: ( Base_FinSeq (n,i3)) in ( dom f) by A30, A40, FUNCT_2:def 1;

          i3 = i5 by A36, A37, A42, Th24;

          hence contradiction by A38, A41, A43, FUNCT_1:def 3;

        end;

        (( ProjFinSeq x1) . i3) = ( |(x1, ( Base_FinSeq (n,i3)))| * ( Base_FinSeq (n,i3))) by A36, A37, Def12;

        hence (( ProjFinSeq x1) . i3) = ( 0* n) by A39, EUCLID_4: 3;

      end;

      

       A44: ( dom ( Sgm ( rng f)) qua Function) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      

       A45: ( rng (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function)) c= ( REAL n);

      

       A46: ( rng ( Sgm ( rng f))) = ( rng f) by FINSEQ_1:def 13;

      ( dom (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function)) = (( Sgm ( rng f)) qua Function " ( dom ( ProjFinSeq x1))) by RELAT_1: 147

      .= ( dom ( Sgm ( rng f))) by A46, A6, Th1;

      then (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function) is FinSequence by A44, FINSEQ_1:def 2;

      then

      reconsider F2 = (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function) as FinSequence of the carrier of ( RealVectSpace ( Seg n)) by A1, A45, FINSEQ_1:def 4;

      ( dom F2) = (( Sgm ( rng f)) qua Function " ( Seg n)) by A6, RELAT_1: 147

      .= ( dom ( Sgm ( rng f))) by A46, Th1;

      then

       A47: ( dom F2) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      then

       A48: ( Seg ( len F2)) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      reconsider F3 = F2 as FinSequence of ( REAL n) by FINSEQ_2: 93;

      

       A49: x0 = ( Sum ( ProjFinSeq x1)) by Th30

      .= ( Sum F3) by A46, A6, A32, Th23, FINSEQ_3: 92

      .= ( Sum F2) by Th41;

      

       A50: ( rng ((f qua Function " ) * ( Sgm ( rng f)) qua Function)) c= ( rng (f qua Function " ) qua Function) by RELAT_1: 26;

      

       A51: ( dom ( Sgm ( rng f)) qua Function) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      

       A52: ( len F2) = ( len ( Sgm ( rng f))) by A47, FINSEQ_1:def 3;

      

       A53: ( dom f) = B0 by A30, FUNCT_2:def 1;

      then ( rng (f qua Function " )) = B0 by A29, FUNCT_1: 33;

      then

       A54: ( rng ((f qua Function " ) * ( Sgm ( rng f)) qua Function)) c= the carrier of ( RealVectSpace ( Seg n)) by A50, XBOOLE_1: 1;

      ( dom ((f qua Function " ) qua Function * ( Sgm ( rng f)) qua Function)) = (( Sgm ( rng f)) qua Function " ( dom (f qua Function " ))) by RELAT_1: 147

      .= (( Sgm ( rng f)) qua Function " ( rng f)) by A29, FUNCT_1: 33

      .= ( dom ( Sgm ( rng f))) by A46, Th1;

      then ((f qua Function " ) qua Function * ( Sgm ( rng f)) qua Function) is FinSequence by A51, FINSEQ_1:def 2;

      then

      reconsider F0 = ((f qua Function " ) * ( Sgm ( rng f)) qua Function) as FinSequence of the carrier of ( RealVectSpace ( Seg n)) by A54, FINSEQ_1:def 4;

      ( dom F0) = (( Sgm ( rng f)) qua Function " ( dom (f qua Function " ))) by RELAT_1: 147

      .= (( Sgm ( rng f)) qua Function " ( rng f)) by A29, FUNCT_1: 33

      .= ( dom ( Sgm ( rng f)) qua Function) by A46, Th1;

      then

       A55: ( dom F0) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      ( dom (f qua Function " )) = ( rng f) by A29, FUNCT_1: 33;

      

      then ( rng F0) = ( rng (f qua Function " )) by A46, RELAT_1: 28

      .= ( dom f) by A29, FUNCT_1: 33;

      then

       A56: ( rng F0) = ( Carrier l0) by A53, A19, A20, XBOOLE_0:def 10;

      

       A57: for i be Nat st i in ( dom F2) holds (F2 . i) = ((l0 . (F0 /. i)) * (F0 /. i))

      proof

        let i be Nat;

        

         A58: ( Sgm ( rng f)) is one-to-one by FINSEQ_3: 92;

        assume i in ( dom F2);

        then

         A59: i in ( Seg ( len F2)) by FINSEQ_1:def 3;

        then

         A60: i in ( dom ( Sgm ( rng f))) by A52, FINSEQ_1:def 3;

        then (( Sgm ( rng f)) . i) in ( rng ( Sgm ( rng f))) by FUNCT_1:def 3;

        then

        reconsider i2 = (( Sgm ( rng f)) . i) as Element of NAT ;

        reconsider r = ( Base_FinSeq (n,i2)) as Element of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

        i2 in ( rng ( Sgm ( rng f))) by A60, FUNCT_1:def 3;

        then

        consider x2 be object such that

         A61: x2 in ( dom f) and

         A62: (f . x2) = i2 by A46, FUNCT_1:def 3;

        ( dom f) = B0 by A30, FUNCT_2:def 1;

        then

        reconsider r2 = x2 as Element of ( RealVectSpace ( Seg n)) by A61;

        

         A63: ex i22 be Element of NAT st (f . r2) = i22 & 1 <= i22 & i22 <= n & r2 = ( Base_FinSeq (n,i22)) by A13, A61;

        then

        consider i4 be Element of NAT such that

         A64: (f . r) = i4 and 1 <= i4 and i4 <= n and

         A65: r = ( Base_FinSeq (n,i4)) by A62;

        

         A66: ( dom f) = B0 by A30, FUNCT_2:def 1;

        (F0 . i) = ((f qua Function " ) . (( Sgm ( rng f)) qua Function . i)) by A60, FUNCT_1: 13

        .= ( Base_FinSeq (n,i2)) by A29, A61, A62, A63, FUNCT_1: 32;

        then ( Base_FinSeq (n,i2)) in ( rng F0) by A55, A48, A59, FUNCT_1:def 3;

        then ( Base_FinSeq (n,i2)) in { v where v be Element of ( RealVectSpace ( Seg n)) : (l0 . v) <> 0 } by A56, RLVECT_2:def 4;

        then

         A67: ex v0 be Element of ( RealVectSpace ( Seg n)) st ( Base_FinSeq (n,i2)) = v0 & (l0 . v0) <> 0 ;

        then ( Base_FinSeq (n,i2)) in B0 by A17;

        then

         A68: ((f qua Function " ) . (f . ( Base_FinSeq (n,i2)))) = ( Base_FinSeq (n,i2)) by A29, A66, FUNCT_1: 34;

        then

         A69: (((f qua Function " ) * ( Sgm ( rng f))) . i) = ( Base_FinSeq (n,i2)) by A60, A62, A63, FUNCT_1: 13;

        

         A70: i2 in ( rng f) by A46, A60, FUNCT_1:def 3;

        then

         A71: 1 <= i2 by FINSEQ_1: 1;

        

         A72: i2 <= n by A70, FINSEQ_1: 1;

        then i4 = i2 by A71, A65, Th24;

        then

         A73: ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))) = i by A60, A64, A58, FUNCT_1: 32;

        

         A74: (f . ( Base_FinSeq (n,i2))) in ( rng ( Sgm ( rng f))) by A46, A61, A62, A63, FUNCT_1:def 3;

        then

         A75: ((f qua Function " ) . (( Sgm ( rng f)) . ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))))) = ( Base_FinSeq (n,i2)) by A58, A68, FUNCT_1: 35;

        ( dom (( Sgm ( rng f)) qua Function " )) = ( rng ( Sgm ( rng f))) by A58, FUNCT_1: 33;

        then ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))) in ( rng (( Sgm ( rng f)) qua Function " )) by A74, FUNCT_1:def 3;

        then

         A76: ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))) in ( dom ( Sgm ( rng f))) by A58, FUNCT_1: 33;

        (l0 . (F0 /. i)) = (l0 . (((f qua Function " ) * ( Sgm ( rng f))) . i)) by A55, A52, A59, PARTFUN1:def 6

        .= (l0 . ( Base_FinSeq (n,i2))) by A73, A76, A75, FUNCT_1: 13

        .= |(x1, ( Base_FinSeq (n,i2)))| by A17, A71, A72, A67;

        

        then ((l0 . (F0 /. i)) * (F0 /. i)) = ( |(x1, ( Base_FinSeq (n,i2)))| * ( Base_FinSeq (n,i2))) by A55, A52, A59, A69, PARTFUN1:def 6

        .= (( ProjFinSeq x1) . (( Sgm ( rng f)) . i)) by A71, A72, Def12

        .= ((( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function) . i) by A60, FUNCT_1: 13;

        hence (F2 . i) = ((l0 . (F0 /. i)) * (F0 /. i));

      end;

      

       A77: ( Sgm ( rng f)) qua Function is one-to-one by FINSEQ_3: 92;

      ( len F2) = ( len F0) by A55, A48, FINSEQ_1:def 3;

      then x1 = ( Sum (l0 (#) F0)) by A49, A57, RLVECT_2:def 7;

      then x1 = ( Sum l2) by A29, A77, A56, RLVECT_2:def 8;

      hence ex l be Linear_Combination of B st x0 = ( Sum l);

    end;

    theorem :: EUCLID_7:44

    

     Th43: for n be Element of NAT , x0 be Element of ( REAL-US n), B be Subset of ( REAL-US n) st B = ( RN_Base n) holds ex l be Linear_Combination of B st x0 = ( Sum l)

    proof

      let n be Element of NAT , x0 be Element of ( REAL-US n), B be Subset of ( REAL-US n);

      reconsider x1 = x0 as Element of ( REAL n) by REAL_NS1:def 6;

      

       A1: ( REAL n) = the carrier of ( REAL-US n) by REAL_NS1:def 6;

      assume

       A2: B = ( RN_Base n);

      

       A3: { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) } c= B

      proof

        let y be object;

        assume y in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) };

        then ex x be Element of ( REAL n) st y = x & ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i));

        hence y in B by A2;

      end;

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

      proof

        let y be object;

        assume y in B;

        then ex i2 be Element of NAT st y = ( Base_FinSeq (n,i2)) & 1 <= i2 & i2 <= n by A2;

        hence y in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) };

      end;

      then

       A4: B = { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) } by A3, XBOOLE_0:def 10;

      

       A5: { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 } c= B

      proof

        let x2 be object;

        assume x2 in { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 };

        then ex x be Element of ( REAL n) st x = x2 & ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 ;

        hence x2 in B by A4;

      end;

      then

      reconsider B0 = { x where x be Element of ( REAL n) : ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 } as Subset of ( REAL-US n) by XBOOLE_1: 1;

      defpred R[ object, object] means $1 in B0 implies ex i be Element of NAT st $2 = i & 1 <= i & i <= n & $1 = ( Base_FinSeq (n,i));

      

       A6: for x be object st x in B0 holds ex y be object st y in ( Seg n) & R[x, y]

      proof

        let x be object;

        assume x in B0;

        then

        consider x2 be Element of ( REAL n) such that

         A7: x = x2 and

         A8: ex i be Element of NAT st 1 <= i & i <= n & x2 = ( Base_FinSeq (n,i)) & |(x1, x2)| <> 0 ;

        consider i0 be Element of NAT such that

         A9: 1 <= i0 and

         A10: i0 <= n and

         A11: x2 = ( Base_FinSeq (n,i0)) and |(x1, x2)| <> 0 by A8;

        i0 in ( Seg n) by A9, A10, FINSEQ_1: 1;

        hence ex y be object st y in ( Seg n) & R[x, y] by A7, A9, A10, A11;

      end;

      consider f be Function of B0, ( Seg n) such that

       A12: for x be object st x in B0 holds R[x, (f . x)] from FUNCT_2:sch 1( A6);

      defpred Q[ object, object] means ($1 in B0 implies (for i be Element of NAT st 1 <= i & i <= n & $1 = ( Base_FinSeq (n,i)) holds $2 = |(x1, ( Base_FinSeq (n,i)))|)) & ( not $1 in B0 implies $2 = 0 );

      

       A13: for x be object st x in the carrier of ( REAL-US n) holds ex y be object st y in REAL & Q[x, y]

      proof

        let x be object;

        assume x in the carrier of ( REAL-US n);

        per cases ;

          suppose

           A14: x in B0;

          then

          consider x2 be Element of ( REAL n) such that

           A15: x2 = x and ex i be Element of NAT st 1 <= i & i <= n & x2 = ( Base_FinSeq (n,i)) & |(x1, x2)| <> 0 ;

          reconsider y0 = |(x1, x2)| as Element of REAL ;

          for i2 be Element of NAT st 1 <= i2 & i2 <= n & x = ( Base_FinSeq (n,i2)) holds y0 = |(x1, ( Base_FinSeq (n,i2)))| by A15;

          hence ex y be object st y in REAL & Q[x, y] by A14;

        end;

          suppose not x in B0;

          hence ex y be object st y in REAL & Q[x, y] by Lm3;

        end;

      end;

      consider l2 be Function of the carrier of ( REAL-US n), REAL such that

       A16: for x be object st x in the carrier of ( REAL-US n) holds Q[x, (l2 . x)] from FUNCT_2:sch 1( A13);

      

       A17: l2 is Element of ( Funcs (the carrier of ( REAL-US n), REAL )) by FUNCT_2: 8;

      for v be Element of ( REAL-US n) st not v in B0 holds (l2 . v) = 0 by A16;

      then

      reconsider l3 = l2 as Linear_Combination of ( REAL-US n) by A2, A5, A17, RLVECT_2:def 3;

      ( Carrier l3) c= B0

      proof

        let x be object;

        assume x in ( Carrier l3);

        then x in { v where v be Element of ( REAL-US n) : (l3 . v) <> 0 } by RLVECT_2:def 4;

        then ex v be Element of ( REAL-US n) st x = v & (l3 . v) <> 0 ;

        hence x in B0 by A16;

      end;

      then

      reconsider l0 = l3 as Linear_Combination of B0 by RLVECT_2:def 6;

      

       A18: ( Carrier l0) c= B0 by RLVECT_2:def 6;

      then ( Carrier l0) c= B by A5;

      then

      reconsider l2 = l0 as Linear_Combination of B by RLVECT_2:def 6;

      

       A19: B0 c= ( Carrier l0)

      proof

        let x be object;

        assume

         A20: x in B0;

        then

        consider x6 be Element of ( REAL n) such that

         A21: x = x6 and

         A22: ex i be Element of NAT st 1 <= i & i <= n & x6 = ( Base_FinSeq (n,i)) & |(x1, x6)| <> 0 ;

        reconsider x66 = x6 as Element of ( REAL-US n) by REAL_NS1:def 6;

        consider i8 be Element of NAT such that 1 <= i8 and i8 <= n and

         A23: x6 = ( Base_FinSeq (n,i8)) and |(x1, x6)| <> 0 by A22;

        (l0 . x66) = |(x1, ( Base_FinSeq (n,i8)))| by A16, A20, A21, A22, A23;

        then x in { v where v be Element of ( REAL-US n) : (l0 . v) <> 0 } by A21, A22, A23;

        hence x in ( Carrier l0) by RLVECT_2:def 4;

      end;

      

       A24: ( dom ( Sgm ( rng f)) qua Function) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      

       A25: ( rng ((f qua Function " ) * ( Sgm ( rng f)) qua Function)) c= ( rng (f qua Function " ) qua Function) by RELAT_1: 26;

      

       A26: ( dom ( Sgm ( rng f)) qua Function) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A27: x1 in ( dom f) and

         A28: x2 in ( dom f) and

         A29: (f . x1) = (f . x2);

        

         A30: ex i2 be Element of NAT st (f . x2) = i2 & 1 <= i2 & i2 <= n & x2 = ( Base_FinSeq (n,i2)) by A12, A28;

        ex i1 be Element of NAT st (f . x1) = i1 & 1 <= i1 & i1 <= n & x1 = ( Base_FinSeq (n,i1)) by A12, A27;

        hence x1 = x2 by A29, A30;

      end;

      then

       A31: f is one-to-one by FUNCT_1:def 4;

      

       A32: ( Seg n) = {} implies B0 = {}

      proof

        set y = the Element of B0;

        assume

         A33: ( Seg n) = {} ;

        assume B0 <> {} ;

        then y in B0;

        then ex x be Element of ( REAL n) st x = y & ex i be Element of NAT st 1 <= i & i <= n & x = ( Base_FinSeq (n,i)) & |(x1, x)| <> 0 ;

        hence contradiction by A33;

      end;

      

       A34: for i3 be Element of NAT st i3 in ( dom ( ProjFinSeq x1)) & not i3 in ( rng ( Sgm ( rng f))) holds (( ProjFinSeq x1) . i3) = ( 0* n)

      proof

        let i3 be Element of NAT ;

        assume that

         A35: i3 in ( dom ( ProjFinSeq x1)) and

         A36: not i3 in ( rng ( Sgm ( rng f)));

        

         A37: i3 in ( Seg ( len ( ProjFinSeq x1))) by A35, FINSEQ_1:def 3;

        then

         A38: 1 <= i3 by FINSEQ_1: 1;

        ( len ( ProjFinSeq x1)) = n by Def12;

        then

         A39: i3 <= n by A37, FINSEQ_1: 1;

        

         A40: not i3 in ( rng f) by A36, FINSEQ_1:def 13;

         A41:

        now

          assume |(x1, ( Base_FinSeq (n,i3)))| <> 0 ;

          then

           A42: ( Base_FinSeq (n,i3)) in B0 by A38, A39;

          then

          consider i5 be Element of NAT such that

           A43: (f . ( Base_FinSeq (n,i3))) = i5 and 1 <= i5 and i5 <= n and

           A44: ( Base_FinSeq (n,i3)) = ( Base_FinSeq (n,i5)) by A12;

          

           A45: ( Base_FinSeq (n,i3)) in ( dom f) by A32, A42, FUNCT_2:def 1;

          i3 = i5 by A38, A39, A44, Th24;

          hence contradiction by A40, A43, A45, FUNCT_1:def 3;

        end;

        (( ProjFinSeq x1) . i3) = ( |(x1, ( Base_FinSeq (n,i3)))| * ( Base_FinSeq (n,i3))) by A38, A39, Def12;

        hence (( ProjFinSeq x1) . i3) = ( 0* n) by A41, EUCLID_4: 3;

      end;

      

       A46: ( rng (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function)) c= ( REAL n);

      

       A47: ( rng ( Sgm ( rng f))) = ( rng f) by FINSEQ_1:def 13;

      

       A48: ( dom f) = B0 by A32, FUNCT_2:def 1;

      then ( rng (f qua Function " )) = B0 by A31, FUNCT_1: 33;

      then

       A49: ( rng ((f qua Function " ) * ( Sgm ( rng f)) qua Function)) c= the carrier of ( REAL-US n) by A25, XBOOLE_1: 1;

      ( dom ((f qua Function " ) qua Function * ( Sgm ( rng f)) qua Function)) = (( Sgm ( rng f)) qua Function " ( dom (f qua Function " ))) by RELAT_1: 147

      .= (( Sgm ( rng f)) qua Function " ( rng f)) by A31, FUNCT_1: 33

      .= ( dom ( Sgm ( rng f))) by A47, Th1;

      then ((f qua Function " ) qua Function * ( Sgm ( rng f)) qua Function) is FinSequence by A26, FINSEQ_1:def 2;

      then

      reconsider F0 = ((f qua Function " ) * ( Sgm ( rng f)) qua Function) as FinSequence of the carrier of ( REAL-US n) by A49, FINSEQ_1:def 4;

      ( dom F0) = (( Sgm ( rng f)) qua Function " ( dom (f qua Function " ))) by RELAT_1: 147

      .= (( Sgm ( rng f)) qua Function " ( rng f)) by A31, FUNCT_1: 33

      .= ( dom ( Sgm ( rng f)) qua Function) by A47, Th1;

      then

       A50: ( dom F0) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      

       A51: ( dom ( ProjFinSeq x1)) = ( Seg ( len ( ProjFinSeq x1))) by FINSEQ_1:def 3

      .= ( Seg n) by Def12;

      

      then ( dom (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function)) = (( Sgm ( rng f)) qua Function " ( Seg n)) by RELAT_1: 147

      .= ( dom ( Sgm ( rng f))) by A47, Th1;

      then (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function) is FinSequence by A24, FINSEQ_1:def 2;

      then

      reconsider F2 = (( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function) as FinSequence of the carrier of ( REAL-US n) by A1, A46, FINSEQ_1:def 4;

      ( dom F2) = (( Sgm ( rng f)) qua Function " ( Seg n)) by A51, RELAT_1: 147

      .= ( dom ( Sgm ( rng f))) by A47, Th1;

      then

       A52: ( dom F2) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      then

       A53: ( Seg ( len F2)) = ( Seg ( len ( Sgm ( rng f)))) by FINSEQ_1:def 3;

      

       A54: ( len F2) = ( len ( Sgm ( rng f))) by A52, FINSEQ_1:def 3;

      ( dom (f qua Function " )) = ( rng f) by A31, FUNCT_1: 33;

      

      then ( rng F0) = ( rng (f qua Function " )) by A47, RELAT_1: 28

      .= ( dom f) by A31, FUNCT_1: 33;

      then

       A55: ( rng F0) = ( Carrier l0) by A48, A18, A19, XBOOLE_0:def 10;

      

       A56: for i be Nat st i in ( dom F2) holds (F2 . i) = ((l0 . (F0 /. i)) * (F0 /. i))

      proof

        let i be Nat;

        

         A57: ( Sgm ( rng f)) is one-to-one by FINSEQ_3: 92;

        assume i in ( dom F2);

        then

         A58: i in ( Seg ( len F2)) by FINSEQ_1:def 3;

        then

         A59: i in ( dom ( Sgm ( rng f))) by A54, FINSEQ_1:def 3;

        then (( Sgm ( rng f)) . i) in ( rng ( Sgm ( rng f))) by FUNCT_1:def 3;

        then

        reconsider i2 = (( Sgm ( rng f)) . i) as Element of NAT ;

        reconsider r = ( Base_FinSeq (n,i2)) as Element of ( REAL-US n) by REAL_NS1:def 6;

        i2 in ( rng ( Sgm ( rng f))) by A59, FUNCT_1:def 3;

        then

        consider x2 be object such that

         A60: x2 in ( dom f) and

         A61: (f . x2) = i2 by A47, FUNCT_1:def 3;

        ( dom f) = B0 by A32, FUNCT_2:def 1;

        then

        reconsider r2 = x2 as Element of ( REAL-US n) by A60;

        

         A62: ex i22 be Element of NAT st (f . r2) = i22 & 1 <= i22 & i22 <= n & r2 = ( Base_FinSeq (n,i22)) by A12, A60;

        then

        consider i4 be Element of NAT such that

         A63: (f . r) = i4 and 1 <= i4 and i4 <= n and

         A64: r = ( Base_FinSeq (n,i4)) by A61;

        

         A65: ( dom f) = B0 by A32, FUNCT_2:def 1;

        (F0 . i) = ((f qua Function " ) . (( Sgm ( rng f)) qua Function . i)) by A59, FUNCT_1: 13

        .= ( Base_FinSeq (n,i2)) by A31, A60, A61, A62, FUNCT_1: 32;

        then ( Base_FinSeq (n,i2)) in ( rng F0) by A50, A53, A58, FUNCT_1:def 3;

        then ( Base_FinSeq (n,i2)) in { v where v be Element of ( REAL-US n) : (l0 . v) <> 0 } by A55, RLVECT_2:def 4;

        then

         A66: ex v0 be Element of ( REAL-US n) st ( Base_FinSeq (n,i2)) = v0 & (l0 . v0) <> 0 ;

        then ( Base_FinSeq (n,i2)) in B0 by A16;

        then

         A67: ((f qua Function " ) . (f . ( Base_FinSeq (n,i2)))) = ( Base_FinSeq (n,i2)) by A31, A65, FUNCT_1: 34;

        then

         A68: (((f qua Function " ) * ( Sgm ( rng f))) . i) = ( Base_FinSeq (n,i2)) by A59, A61, A62, FUNCT_1: 13;

        

         A69: i2 in ( rng f) by A47, A59, FUNCT_1:def 3;

        then

         A70: 1 <= i2 by FINSEQ_1: 1;

        

         A71: i2 <= n by A69, FINSEQ_1: 1;

        then i4 = i2 by A70, A64, Th24;

        then

         A72: ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))) = i by A59, A63, A57, FUNCT_1: 32;

        

         A73: (f . ( Base_FinSeq (n,i2))) in ( rng ( Sgm ( rng f))) by A47, A60, A61, A62, FUNCT_1:def 3;

        then

         A74: ((f qua Function " ) . (( Sgm ( rng f)) . ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))))) = ( Base_FinSeq (n,i2)) by A57, A67, FUNCT_1: 35;

        ( dom (( Sgm ( rng f)) qua Function " )) = ( rng ( Sgm ( rng f))) by A57, FUNCT_1: 33;

        then ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))) in ( rng (( Sgm ( rng f)) qua Function " )) by A73, FUNCT_1:def 3;

        then

         A75: ((( Sgm ( rng f)) qua Function " ) . (f . ( Base_FinSeq (n,i2)))) in ( dom ( Sgm ( rng f))) by A57, FUNCT_1: 33;

        (l0 . (F0 /. i)) = (l0 . (((f qua Function " ) * ( Sgm ( rng f))) . i)) by A50, A54, A58, PARTFUN1:def 6

        .= (l0 . ( Base_FinSeq (n,i2))) by A72, A75, A74, FUNCT_1: 13

        .= |(x1, ( Base_FinSeq (n,i2)))| by A16, A70, A71, A66;

        

        then ((l0 . (F0 /. i)) * (F0 /. i)) = ( |(x1, ( Base_FinSeq (n,i2)))| * ( Base_FinSeq (n,i2))) by A50, A54, A58, A68, PARTFUN1:def 6

        .= (( ProjFinSeq x1) . (( Sgm ( rng f)) . i)) by A70, A71, Def12

        .= ((( ProjFinSeq x1) qua Function * ( Sgm ( rng f)) qua Function) . i) by A59, FUNCT_1: 13;

        hence (F2 . i) = ((l0 . (F0 /. i)) * (F0 /. i));

      end;

      

       A76: ( Sgm ( rng f)) qua Function is one-to-one by FINSEQ_3: 92;

      reconsider F3 = F2 as FinSequence of ( REAL n) by REAL_NS1:def 6;

      

       A77: x0 = ( Sum ( ProjFinSeq x1)) by Th30

      .= ( Sum F3) by A47, A51, A34, Th23, FINSEQ_3: 92

      .= ( Sum F2) by Th33;

      ( len F2) = ( len F0) by A50, A53, FINSEQ_1:def 3;

      then x1 = ( Sum (l0 (#) F0)) by A77, A56, RLVECT_2:def 7;

      then x1 = ( Sum l2) by A31, A76, A55, RLVECT_2:def 8;

      hence ex l be Linear_Combination of B st x0 = ( Sum l);

    end;

    theorem :: EUCLID_7:45

    

     Th44: for B be Subset of ( RealVectSpace ( Seg n)) st B = ( RN_Base n) holds B is Basis of ( RealVectSpace ( Seg n))

    proof

      let B be Subset of ( RealVectSpace ( Seg n));

      set V = ( RealVectSpace ( Seg n));

      assume

       A1: B = ( RN_Base n);

      then

      reconsider B1 = B as R-orthonormal Subset of V;

      

       A2: the carrier of ( Lin B) = the set of all ( Sum l) where l be Linear_Combination of B by RLVECT_3:def 2;

       A3:

      now

        assume not the carrier of V c= the carrier of ( Lin B);

        then

        consider x be object such that

         A4: x in the carrier of V and

         A5: not x in the carrier of ( Lin B);

        reconsider x0 = x as Element of V by A4;

        ex l be Linear_Combination of B st x0 = ( Sum l) by A1, Th42;

        hence contradiction by A2, A5;

      end;

      the carrier of ( Lin B) c= the carrier of V

      proof

        let x be object;

        assume x in the carrier of ( Lin B);

        then ex l be Linear_Combination of B st x = ( Sum l) by A2;

        hence x in the carrier of V;

      end;

      then the carrier of ( Lin B) = the carrier of V by A3, XBOOLE_0:def 10;

      then ( Lin B) = V by Th8;

      then B1 is Basis of ( RealVectSpace ( Seg n)) by RLVECT_3:def 3;

      hence thesis;

    end;

    registration

      let n;

      cluster ( RealVectSpace ( Seg n)) -> finite-dimensional;

      coherence

      proof

        reconsider B = ( RN_Base n) as Subset of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

        B is Basis of ( RealVectSpace ( Seg n)) by Th44;

        hence thesis by RLVECT_5:def 1;

      end;

    end

    theorem :: EUCLID_7:46

    ( dim ( RealVectSpace ( Seg n))) = n

    proof

      reconsider B = ( RN_Base n) as Subset of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

      

       A1: for I be Basis of ( RealVectSpace ( Seg n)) holds n = ( card I)

      proof

        let I be Basis of ( RealVectSpace ( Seg n));

        B is Basis of ( RealVectSpace ( Seg n)) by Th44;

        then ( card B) = ( card I) by RLVECT_5: 25;

        hence n = ( card I) by Lm5;

      end;

      n in NAT by ORDINAL1:def 12;

      hence thesis by A1, RLVECT_5:def 2;

    end;

    theorem :: EUCLID_7:47

    

     Th46: for B be Subset of ( RealVectSpace ( Seg n)) st B is Basis of ( RealVectSpace ( Seg n)) holds ( card B) = n

    proof

      let B be Subset of ( RealVectSpace ( Seg n));

      assume

       A1: B is Basis of ( RealVectSpace ( Seg n));

      reconsider Br = ( RN_Base n) as Subset of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

      Br is Basis of ( RealVectSpace ( Seg n)) by Th44;

      then ( card Br) = ( card B) by A1, RLVECT_5: 25;

      hence ( card B) = n by Lm5;

    end;

    theorem :: EUCLID_7:48

    

     Th47: {} is Basis of ( RealVectSpace ( Seg 0 ))

    proof

      consider A be finite Subset of ( RealVectSpace ( Seg 0 )) such that

       A1: A is Basis of ( RealVectSpace ( Seg 0 )) by RLVECT_5:def 1;

      ( card A) = 0 by A1, Th46;

      then A = {} ;

      hence thesis by A1;

    end;

    theorem :: EUCLID_7:49

    

     Th48: for n be Element of NAT holds ( RN_Base n) is Basis of ( REAL-US n)

    proof

      let n be Element of NAT ;

      reconsider B = ( RN_Base n) as Subset of ( REAL-US n) by REAL_NS1:def 6;

      set V = ( REAL-US n);

      

       A1: the carrier of ( Lin B) = the set of all ( Sum l) where l be Linear_Combination of B by RUSUB_3:def 1;

       A2:

      now

        assume not the carrier of V c= the carrier of ( Lin B);

        then

        consider x be object such that

         A3: x in the carrier of V and

         A4: not x in the carrier of ( Lin B);

        reconsider x0 = x as Element of V by A3;

        ex l be Linear_Combination of B st x0 = ( Sum l) by Th43;

        hence contradiction by A1, A4;

      end;

      the carrier of ( Lin B) c= the carrier of V

      proof

        let x be object;

        assume x in the carrier of ( Lin B);

        then ex l be Linear_Combination of B st x = ( Sum l) by A1;

        hence x in the carrier of V;

      end;

      then the carrier of ( Lin B) = the carrier of V by A2, XBOOLE_0:def 10;

      then ( Lin B) = V by RUSUB_1: 26;

      hence thesis by RUSUB_3:def 2;

    end;

    theorem :: EUCLID_7:50

    

     Th49: for D be Orthogonal_Basis of n holds D is Basis of ( RealVectSpace ( Seg n))

    proof

      let D be Orthogonal_Basis of n;

      set V = ( RealVectSpace ( Seg n));

      reconsider B = D as R-orthonormal Subset of V by FINSEQ_2: 93;

      per cases ;

        suppose n = 0 ;

        hence thesis by Th17, Th47;

      end;

        suppose

         A1: n <> 0 ;

        reconsider D0 = D as R-orthonormal Subset of ( REAL n);

        consider I be Basis of V such that

         A2: B c= I by RLVECT_5: 2;

        ( card I) = n by Th46;

        then

         A3: I is finite;

        

         A4: for D2 be R-orthonormal Subset of ( REAL n) st D0 c= D2 holds D2 = D0 by Def6;

         A5:

        now

          assume that B <> I and

           A6: not I c= the carrier of ( Lin B);

          consider x0 be object such that

           A7: x0 in I and

           A8: not x0 in the carrier of ( Lin B) by A6;

          reconsider z0 = x0 as Element of ( REAL n) by A7, FINSEQ_2: 93;

           not x0 in ( Lin B) by A8;

          then

           A9: not x0 in B by RLVECT_3: 15;

          consider p be FinSequence such that

           A10: ( rng p) = B and

           A11: p is one-to-one by A2, A3, FINSEQ_4: 58;

          

           A12: 1 <= (( len p) + 1) by NAT_1: 12;

          reconsider p0 = p as FinSequence of ( REAL n) by A10, FINSEQ_1:def 4;

          defpred P[ Nat] means 1 <= $1 & $1 <= (( len p) + 1) implies ex q be FinSequence of ( REAL n) st ( len q) = $1 & ($1 <= ( len p) implies for d be Real holds not (q . $1) = (d * (p0 /. $1))) & (q . 1) = z0 & for i be Nat, a,b be Element of ( REAL n) st 1 <= i & i < $1 & a = (q /. i) & b = (p0 /. i) holds (q /. (i + 1)) <> ( 0* n) & (q . (i + 1)) = ((q /. i) - ( |(a, b)| * (p0 /. i)));

          

           A13: I is linearly-independent by RLVECT_3:def 3;

          

           A14: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             A15: P[k];

            per cases ;

              suppose

               A16: 1 <= (k + 1) & (k + 1) <= (( len p) + 1);

              k < (k + 1) by XREAL_1: 29;

              then

               A17: k < (( len p) + 1) by A16, XXREAL_0: 2;

              

               A18: k <= ( len p) by A16, XREAL_1: 6;

              per cases ;

                suppose 1 <= k;

                then

                consider q0 be FinSequence of ( REAL n) such that

                 A19: ( len q0) = k and

                 A20: 1 <= k and k <= (( len p) + 1) and

                 A21: k <= ( len p) implies for d be Real holds not (q0 . k) = (d * (p0 /. k)) and

                 A22: (q0 . 1) = z0 and

                 A23: for i be Nat, a,b be Element of ( REAL n) st 1 <= i & i < k & a = (q0 /. i) & b = (p0 /. i) holds (q0 /. (i + 1)) <> ( 0* n) & (q0 . (i + 1)) = ((q0 /. i) - ( |(a, b)| * (p0 /. i))) by A15, A17;

                reconsider a2 = (q0 /. k), b2 = (p0 /. k) as Element of ( REAL n);

                reconsider q3 = <*((q0 /. k) - ( |(a2, b2)| * (p0 /. k)))*> as FinSequence of ( REAL n);

                reconsider q1 = (q0 ^ q3) as FinSequence of ( REAL n);

                1 in ( Seg ( len q0)) by A19, A20, FINSEQ_1: 1;

                then

                 A24: 1 in ( dom q0) by FINSEQ_1:def 3;

                then

                 A25: (q1 . 1) = z0 by A22, FINSEQ_1:def 7;

                

                 A26: 1 <= (k + 1) by NAT_1: 12;

                

                 A27: (k + 1) <= ( len p) implies (p0 /. (k + 1)) in B

                proof

                  assume

                   A28: (k + 1) <= ( len p);

                  then (k + 1) in ( dom p) by A26, FINSEQ_3: 25;

                  then (p . (k + 1)) in ( rng p) by FUNCT_1:def 3;

                  hence (p0 /. (k + 1)) in B by A10, A28, FINSEQ_4: 15, NAT_1: 12;

                end;

                

                 A29: ( len q1) = (( len q0) + ( len q3)) by FINSEQ_1: 22

                .= (k + 1) by A19, FINSEQ_1: 40;

                

                 A30: for i be Nat, a,b be Element of ( REAL n) st 1 <= i & i < (k + 1) & a = (q1 /. i) & b = (p0 /. i) holds (q1 /. (i + 1)) <> ( 0* n) & (q1 . (i + 1)) = ((q1 /. i) - ( |(a, b)| * (p0 /. i)))

                proof

                  let i be Nat, a,b be Element of ( REAL n);

                  assume that

                   A31: 1 <= i and

                   A32: i < (k + 1) and

                   A33: a = (q1 /. i) and

                   A34: b = (p0 /. i);

                  

                   A35: i <= k by A32, NAT_1: 13;

                  

                   A36: (i + 1) <= (k + 1) by A32, NAT_1: 13;

                  

                   A37: 1 <= (i + 1) by NAT_1: 12;

                  per cases by A35, XXREAL_0: 1;

                    suppose

                     A38: i < k;

                    then

                     A39: (i + 1) <= k by NAT_1: 13;

                    then

                     A40: (q1 . (i + 1)) = (q0 . (i + 1)) by A19, FINSEQ_1: 64, NAT_1: 12;

                    

                     A41: (q1 /. (i + 1)) = (q1 . (i + 1)) by A29, A37, A36, FINSEQ_4: 15;

                    

                     A42: (q0 /. (i + 1)) = (q0 . (i + 1)) by A19, A39, FINSEQ_4: 15, NAT_1: 12;

                    (q1 /. i) = (q1 . i) by A29, A31, A32, FINSEQ_4: 15

                    .= (q0 . i) by A19, A31, A35, FINSEQ_1: 64

                    .= (q0 /. i) by A19, A31, A35, FINSEQ_4: 15;

                    hence (q1 /. (i + 1)) <> ( 0* n) & (q1 . (i + 1)) = ((q1 /. i) - ( |(a, b)| * (p0 /. i))) by A23, A31, A33, A34, A38, A40, A41, A42;

                  end;

                    suppose

                     A43: i = k;

                    

                    then

                     A44: (q1 /. (i + 1)) = (q1 . (k + 1)) by A29, A26, FINSEQ_4: 15

                    .= (q3 . ((k + 1) - ( len q0))) by A19, A29, FINSEQ_1: 24, XREAL_1: 29

                    .= ((q0 /. k) - ( |(a2, b2)| * (p0 /. k))) by A19, FINSEQ_1: 40;

                     A45:

                    now

                      assume (q1 /. (i + 1)) = ( 0* n);

                      then (((q0 /. k) - ( |(a2, b2)| * (p0 /. k))) + ( |(a2, b2)| * (p0 /. k))) = ( |(a2, b2)| * (p0 /. k)) by A44, EUCLID_4: 1;

                      then

                       A46: (q0 /. k) = ( |(a2, b2)| * (p0 /. k)) by RVSUM_1: 43;

                      (q0 /. k) = (q0 . k) by A19, A20, FINSEQ_4: 15;

                      hence contradiction by A16, A21, A46, XREAL_1: 6;

                    end;

                    k < (k + 1) by XREAL_1: 29;

                    then

                     A47: (q1 /. k) = (q1 . k) by A20, A29, FINSEQ_4: 15;

                    

                     A48: (q0 /. k) = (q0 . k) by A19, A20, FINSEQ_4: 15;

                    (q1 . k) = (q0 . k) by A19, A20, FINSEQ_1: 64;

                    hence (q1 /. (i + 1)) <> ( 0* n) & (q1 . (i + 1)) = ((q1 /. i) - ( |(a, b)| * (p0 /. i))) by A29, A33, A34, A37, A43, A48, A47, A44, A45, FINSEQ_4: 15;

                  end;

                end;

                

                 A49: for s1 be Element of ( RealVectSpace ( Seg n)), a01 be Real st s1 in B holds (a01 * s1) in the carrier of ( Lin B)

                proof

                  let s1 be Element of ( RealVectSpace ( Seg n)), a01 be Real;

                  assume

                   A50: s1 in B;

                   {s1} c= B by A50, TARSKI:def 1;

                  then ( Lin {s1}) is Subspace of ( Lin B) by RLVECT_3: 20;

                  then

                   A51: the carrier of ( Lin {s1}) c= the carrier of ( Lin B) by RLSUB_1:def 2;

                  (a01 * s1) in ( Lin {s1}) by RLVECT_4: 8;

                  then (a01 * s1) in the carrier of ( Lin {s1});

                  hence (a01 * s1) in the carrier of ( Lin B) by A51;

                end;

                

                 A52: for s1 be Element of ( REAL n), a01 be Real st s1 in B holds (a01 * s1) in the carrier of ( Lin B)

                proof

                  let s1 be Element of ( REAL n), a01 be Real;

                  reconsider s10 = s1 as Element of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

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

                  

                   A53: (aa * s1) = (aa * s10);

                  assume s1 in B;

                  hence (a01 * s1) in the carrier of ( Lin B) by A49, A53;

                end;

                defpred G[ Nat] means ($1 + 1) <= (k + 1) implies not (q1 . ($1 + 1)) in the carrier of ( Lin B);

                

                 A54: for j be Nat st G[j] holds G[(j + 1)]

                proof

                  let j be Nat;

                  assume

                   A55: G[j];

                  ((j + 1) + 1) <= (k + 1) implies not (q1 . ((j + 1) + 1)) in the carrier of ( Lin B)

                  proof

                    

                     A56: B c= the carrier of ( Lin B)

                    proof

                      let z be object;

                      assume z in B;

                      then z in ( Lin B) by RLVECT_3: 15;

                      hence z in the carrier of ( Lin B);

                    end;

                    assume ((j + 1) + 1) <= (k + 1);

                    then

                     A57: (j + 1) <= k by XREAL_1: 6;

                    per cases by A57, XXREAL_0: 1;

                      suppose

                       A58: (j + 1) = k;

                      1 <= (j + 1) by NAT_1: 12;

                      then (j + 1) in ( dom p0) by A18, A58, FINSEQ_3: 25;

                      then

                       A59: (p0 . (j + 1)) in ( rng p) by FUNCT_1:def 3;

                      

                       A60: (p0 /. (j + 1)) = (p0 . (j + 1)) by A18, A58, FINSEQ_4: 15, NAT_1: 12;

                      1 <= ((j + 1) + 1) by NAT_1: 12;

                      then

                       A61: (q1 /. ((j + 1) + 1)) = (q1 . ((j + 1) + 1)) by A29, A58, FINSEQ_4: 15;

                      

                       A62: (q1 . ((j + 1) + 1)) = ((q0 /. k) - ( |(a2, b2)| * (p0 /. k))) by A19, A58, FINSEQ_1: 42;

                      now

                        assume

                         A63: (q1 . ((j + 1) + 1)) in the carrier of ( Lin B);

                        ((q1 /. ((j + 1) + 1)) + ( |(a2, b2)| * (p0 /. (j + 1)))) = (q0 /. (j + 1)) by A58, A62, A61, RVSUM_1: 43;

                        then (q0 /. (j + 1)) in the carrier of ( Lin B) by A10, A56, A61, A59, A60, A63, Lm4;

                        then

                         A64: (q0 /. (j + 1)) in ( Lin B);

                        

                         A65: not (q1 . (j + 1)) in ( Lin B) by A55, A58, XREAL_1: 29;

                        (q1 . (j + 1)) = (q0 . (j + 1)) by A19, A20, A58, FINSEQ_1: 64;

                        hence contradiction by A19, A20, A58, A64, A65, FINSEQ_4: 15;

                      end;

                      hence not (q1 . ((j + 1) + 1)) in the carrier of ( Lin B);

                    end;

                      suppose

                       A66: (j + 1) < k;

                      reconsider a11 = (q0 /. (j + 1)), b11 = (p0 /. (j + 1)) as Element of ( REAL n);

                      

                       A67: ((j + 1) + 1) <= k by A66, NAT_1: 13;

                      then

                       A68: (q0 /. ((j + 1) + 1)) = (q0 . ((j + 1) + 1)) by A19, FINSEQ_4: 15, NAT_1: 12;

                      

                       A69: (j + 1) <= ( len p0) by A18, A66, XXREAL_0: 2;

                      then

                       A70: (p0 /. (j + 1)) = (p0 . (j + 1)) by FINSEQ_4: 15, NAT_1: 12;

                      

                       A71: 1 <= (j + 1) by NAT_1: 12;

                      then (j + 1) in ( dom p0) by A69, FINSEQ_3: 25;

                      then

                       A72: (p0 . (j + 1)) in ( rng p) by FUNCT_1:def 3;

                      

                       A73: (q1 . ((j + 1) + 1)) = (q0 . ((j + 1) + 1)) by A19, A67, FINSEQ_1: 64, NAT_1: 12;

                      

                       A74: (q0 . ((j + 1) + 1)) = ((q0 /. (j + 1)) - ( |(a11, b11)| * (p0 /. (j + 1)))) by A23, A66, A71;

                      now

                        assume

                         A75: (q1 . ((j + 1) + 1)) in the carrier of ( Lin B);

                        ((q0 /. ((j + 1) + 1)) + ( |(a11, b11)| * (p0 /. (j + 1)))) = (q0 /. (j + 1)) by A74, A68, RVSUM_1: 43;

                        then (q0 /. (j + 1)) in the carrier of ( Lin B) by A10, A56, A68, A72, A70, A73, A75, Lm4;

                        then

                         A76: (q0 /. (j + 1)) in ( Lin B);

                        k < (k + 1) by XREAL_1: 29;

                        then

                         A77: not (q1 . (j + 1)) in ( Lin B) by A55, A66, XXREAL_0: 2;

                        (q1 . (j + 1)) = (q0 . (j + 1)) by A19, A66, FINSEQ_1: 64, NAT_1: 12;

                        hence contradiction by A19, A66, A76, A77, FINSEQ_4: 15, NAT_1: 12;

                      end;

                      hence not (q1 . ((j + 1) + 1)) in the carrier of ( Lin B);

                    end;

                  end;

                  hence G[(j + 1)];

                end;

                

                 A78: G[ 0 ] by A8, A22, A24, FINSEQ_1:def 7;

                for j be Nat holds G[j] from NAT_1:sch 2( A78, A54);

                then (k + 1) <= ( len p) implies for d be Real holds not (q1 . (k + 1)) = (d * (p0 /. (k + 1))) by A52, A27;

                hence P[(k + 1)] by A29, A25, A30;

              end;

                suppose

                 A79: 1 > k;

                reconsider q1 = <*z0*> as FinSequence of ( REAL n);

                

                 A80: ( len q1) = 1 by FINSEQ_1: 40;

                

                 A81: (q1 . 1) = z0 by FINSEQ_1: 40;

                

                 A82: 1 <= ( len p) implies for d be Real holds not (q1 . 1) = (d * (p0 /. 1))

                proof

                  assume

                   A83: 1 <= ( len p);

                  thus for d be Real holds not (q1 . 1) = (d * (p0 /. 1))

                  proof

                    let d be Real;

                    

                     A84: (q1 . 1) = z0 by FINSEQ_1: 40;

                    1 in ( dom p0) by A83, FINSEQ_3: 25;

                    then

                     A85: (p0 . 1) in B by A10, FUNCT_1:def 3;

                    (p0 /. 1) = (p0 . 1) by A83, FINSEQ_4: 15;

                    hence not (q1 . 1) = (d * (p0 /. 1)) by A2, A7, A9, A13, A84, A85, Th39;

                  end;

                end;

                

                 A86: for i be Nat, a,b be Element of ( REAL n) st 1 <= i & i < 1 & a = (q1 /. i) & b = (p0 /. i) holds (q1 /. (i + 1)) <> ( 0* n) & (q1 . (i + 1)) = ((q1 /. i) - ( |(a, b)| * (p0 /. i)));

                k = 0 by A79, NAT_1: 14;

                hence P[(k + 1)] by A80, A81, A82, A86;

              end;

            end;

              suppose not (1 <= (k + 1) & (k + 1) <= (( len p) + 1));

              hence P[(k + 1)];

            end;

          end;

          

           A87: P[ 0 ];

          for k be Nat holds P[k] from NAT_1:sch 2( A87, A14);

          then

          consider q be FinSequence of ( REAL n) such that

           A88: ( len q) = (( len p) + 1) and (( len p) + 1) <= ( len p) implies for d be Real holds not (q . (( len p) + 1)) = (d * (p0 /. (( len p) + 1))) and (q . 1) = z0 and

           A89: for i be Nat, a,b be Element of ( REAL n) st 1 <= i & i < (( len p) + 1) & a = (q /. i) & b = (p0 /. i) holds (q /. (i + 1)) <> ( 0* n) & (q . (i + 1)) = ((q /. i) - ( |(a, b)| * (p0 /. i))) by A12;

          reconsider u4 = (q /. ( len q)) as Element of ( REAL n);

          

           A90: ( len p) < (( len p) + 1) by XREAL_1: 29;

          set u0 = ((1 / |.u4.|) * u4);

          reconsider B3 = (B \/ {u0}) as Subset of ( REAL n) by XBOOLE_1: 8;

          

           A91: for i be Nat, s be Element of ( REAL n) st 1 <= i & i <= ( len p) & (p0 /. i) = s holds |(s, u4)| = 0

          proof

            defpred Q[ Nat] means for s2 be Element of ( REAL n), u2 be Element of ( REAL n), k be Nat st u2 = (q /. $1) & 1 <= k & k < $1 & $1 <= (( len p) + 1) & (p0 /. k) = s2 holds |(s2, u2)| = 0 ;

            let i be Nat, s be Element of ( REAL n);

            assume that

             A92: 1 <= i and

             A93: i <= ( len p) and

             A94: (p0 /. i) = s;

            

             A95: for k be Nat st Q[k] holds Q[(k + 1)]

            proof

              let k be Nat;

              assume

               A96: Q[k];

              for s2 be Element of ( REAL n), u2 be Element of ( REAL n), k2 be Nat st u2 = (q /. (k + 1)) & 1 <= k2 & k2 < (k + 1) & (k + 1) <= (( len p) + 1) & (p0 /. k2) = s2 holds |(s2, u2)| = 0

              proof

                

                 A97: k < (k + 1) by XREAL_1: 29;

                let s2 be Element of ( REAL n), u2 be Element of ( REAL n), k2 be Nat;

                assume that

                 A98: u2 = (q /. (k + 1)) and

                 A99: 1 <= k2 and

                 A100: k2 < (k + 1) and

                 A101: (k + 1) <= (( len p) + 1) and

                 A102: (p0 /. k2) = s2;

                

                 A103: k2 <= k by A100, NAT_1: 13;

                per cases ;

                  suppose k = 0 ;

                  hence |(s2, u2)| = 0 by A99, A100;

                end;

                  suppose

                   A104: k <> 0 ;

                  reconsider a = (q /. k), b = (p0 /. k) as Element of ( REAL n);

                  

                   A105: k < (( len p) + 1) by A101, A97, XXREAL_0: 2;

                  then

                   A106: k <= ( len p) by NAT_1: 13;

                  1 <= (k + 1) by A99, A100, XXREAL_0: 2;

                  then

                   A107: u2 = (q . (k + 1)) by A88, A98, A101, FINSEQ_4: 15;

                  

                   A108: ( 0 + 1) <= k by A104, NAT_1: 13;

                  then (q . (k + 1)) = ((q /. k) - ( |(a, b)| * (p0 /. k))) by A89, A105;

                  

                  then

                   A109: |(s2, u2)| = ( |(s2, a)| - |(s2, ( |(a, b)| * b))|) by A107, EUCLID_4: 26

                  .= ( |(s2, a)| - ( |(a, b)| * |(s2, b)|)) by EUCLID_4: 21;

                  per cases by A103, XXREAL_0: 1;

                    suppose

                     A110: k2 < k;

                    then

                     A111: 1 < k by A99, XXREAL_0: 2;

                    then

                     A112: (p0 /. k) = (p0 . k) by A106, FINSEQ_4: 15;

                    k in ( Seg ( len p0)) by A106, A111, FINSEQ_1: 1;

                    then

                     A113: k in ( dom p0) by FINSEQ_1:def 3;

                    then

                     A114: b in D by A10, A112, FUNCT_1:def 3;

                    

                     A115: k < (( len p) + 1) by A101, A97, XXREAL_0: 2;

                    

                     A116: k2 < ( len p) by A106, A110, XXREAL_0: 2;

                    then

                     A117: (p0 /. k2) = (p0 . k2) by A99, FINSEQ_4: 15;

                    k2 in ( Seg ( len p0)) by A99, A116, FINSEQ_1: 1;

                    then

                     A118: k2 in ( dom p0) by FINSEQ_1:def 3;

                    then

                     A119: s2 in ( rng p) by A102, A117, FUNCT_1:def 3;

                    s2 <> b by A11, A102, A110, A117, A118, A112, A113, FUNCT_1:def 4;

                    then |(s2, b)| = 0 by A10, A119, A114, Def3;

                    hence |(s2, u2)| = 0 by A96, A99, A102, A109, A110, A115;

                  end;

                    suppose

                     A120: k2 = k;

                    k in ( Seg ( len p0)) by A108, A106, FINSEQ_1: 1;

                    then

                     A121: k in ( dom p0) by FINSEQ_1:def 3;

                    (p0 /. k) = (p0 . k) by A108, A106, FINSEQ_4: 15;

                    then b in ( rng p0) by A121, FUNCT_1:def 3;

                    then |.b.| = 1 by A10, Def4;

                    then ( |.b.| ^2 ) = 1;

                    

                    hence |(s2, u2)| = ( |(b, a)| - ( |(a, b)| * 1)) by A102, A109, A120, EUCLID_2: 4

                    .= 0 ;

                  end;

                end;

              end;

              hence Q[(k + 1)];

            end;

            

             A122: Q[ 0 ];

            

             A123: for k be Nat holds Q[k] from NAT_1:sch 2( A122, A95);

            ( len p) < (( len p) + 1) by XREAL_1: 29;

            then i < ( len q) by A88, A93, XXREAL_0: 2;

            hence |(s, u4)| = 0 by A88, A92, A94, A123;

          end;

          

           A124: for i be Nat, s be Element of ( REAL n) st 1 <= i & i <= ( len p) & (p0 /. i) = s holds |(s, u0)| = 0

          proof

            let i be Nat, s be Element of ( REAL n);

            assume that

             A125: 1 <= i and

             A126: i <= ( len p) and

             A127: (p0 /. i) = s;

            

             A128: |(s, u0)| = ((1 / |.u4.|) * |(s, u4)|) by EUCLID_4: 22;

             |(s, u4)| = 0 by A91, A125, A126, A127;

            hence |(s, u0)| = 0 by A128;

          end;

          for x,y be real-valued FinSequence st x in B3 & y in B3 & x <> y holds |(x, y)| = 0

          proof

            let x,y be real-valued FinSequence;

            assume that

             A129: x in B3 and

             A130: y in B3 and

             A131: x <> y;

            per cases by A129, A130, XBOOLE_0:def 3;

              suppose x in B & y in B;

              hence |(x, y)| = 0 by A131, Def3;

            end;

              suppose

               A132: x in B & y in {u0};

              then

              consider x3 be object such that

               A133: x3 in ( dom p0) and

               A134: x = (p0 . x3) by A10, FUNCT_1:def 3;

              reconsider j = x3 as Element of NAT by A133;

              

               A135: x3 in ( Seg ( len p0)) by A133, FINSEQ_1:def 3;

              then

               A136: j <= ( len p0) by FINSEQ_1: 1;

              

               A137: y = u0 by A132, TARSKI:def 1;

              

               A138: 1 <= j by A135, FINSEQ_1: 1;

              then (p0 . x3) = (p0 /. j) by A136, FINSEQ_4: 15;

              hence |(x, y)| = 0 by A124, A137, A134, A138, A136;

            end;

              suppose

               A139: x in {u0} & y in B;

              then

              consider y3 be object such that

               A140: y3 in ( dom p0) and

               A141: y = (p0 . y3) by A10, FUNCT_1:def 3;

              reconsider j = y3 as Element of NAT by A140;

              

               A142: y3 in ( Seg ( len p0)) by A140, FINSEQ_1:def 3;

              then

               A143: j <= ( len p0) by FINSEQ_1: 1;

              

               A144: x = u0 by A139, TARSKI:def 1;

              

               A145: 1 <= j by A142, FINSEQ_1: 1;

              then (p0 . y3) = (p0 /. j) by A143, FINSEQ_4: 15;

              hence |(x, y)| = 0 by A124, A144, A141, A145, A143;

            end;

              suppose

               A146: x in {u0} & y in {u0};

              then y = u0 by TARSKI:def 1;

              hence |(x, y)| = 0 by A131, A146, TARSKI:def 1;

            end;

          end;

          then

           A147: B3 is R-orthogonal;

          1 in ( dom p) by A1, A10, FINSEQ_3: 32;

          then

           A148: 1 <= ( len p) by FINSEQ_3: 25;

          set aq = (q /. ( len p)), bq = (p0 /. ( len p));

          

           A149: bq = (p0 /. ( len p));

          aq = (q /. ( len p));

          then

           A150: |.u4.| <> 0 by A148, A88, A89, A149, A90, EUCLID: 8;

          

           A151: |.(1 / |.u4.|).| = (1 / |.u4.|) by ABSVALUE:def 1;

          

           A152: u0 in {u0} by TARSKI:def 1;

          

           A153: |.u0.| = ( |.(1 / |.u4.|).| * |.u4.|) by EUCLID: 11

          .= 1 by A150, A151, XCMPLX_1: 106;

          then B3 is R-normal by Th16;

          then D0 = B3 by A4, A147, XBOOLE_1: 7;

          then u0 in B by A152, XBOOLE_0:def 3;

          then

          consider x3 be object such that

           A154: x3 in ( dom p0) and

           A155: u0 = (p0 . x3) by A10, FUNCT_1:def 3;

          reconsider j = x3 as Element of NAT by A154;

          

           A156: x3 in ( Seg ( len p0)) by A154, FINSEQ_1:def 3;

          then

           A157: j <= ( len p0) by FINSEQ_1: 1;

          

           A158: 1 <= j by A156, FINSEQ_1: 1;

          then (p0 . x3) = (p0 /. j) by A157, FINSEQ_4: 15;

          then |(u0, u0)| = 0 by A124, A155, A158, A157;

          hence B is Basis of ( RealVectSpace ( Seg n)) by A153, EUCLID_4: 16;

        end;

        ( Lin B) is Subspace of ( Lin I) by A2, RLVECT_3: 20;

        then

         A159: the carrier of ( Lin B) c= the carrier of ( Lin I) by RLSUB_1:def 2;

        

         A160: ( Lin I) = V by RLVECT_3:def 3;

        now

          assume I c= the carrier of ( Lin B);

          then ( Lin I) is Subspace of ( Lin B) by RLVECT_5: 19;

          then the carrier of ( Lin I) c= the carrier of ( Lin B) by RLSUB_1:def 2;

          then the carrier of ( Lin I) = the carrier of ( Lin B) by A159, XBOOLE_0:def 10;

          then ( Lin B) = ( Lin I) by RLSUB_1: 30;

          hence B is Basis of ( RealVectSpace ( Seg n)) by A160, RLVECT_3:def 3;

        end;

        hence thesis by A5;

      end;

    end;

    registration

      let n be Element of NAT ;

      cluster ( REAL-US n) -> finite-dimensional;

      coherence

      proof

        reconsider B = ( RN_Base n) as Subset of ( REAL-US n) by REAL_NS1:def 6;

        B is Basis of ( REAL-US n) by Th48;

        hence thesis by RUSUB_4:def 1;

      end;

    end

    theorem :: EUCLID_7:51

    for n be Element of NAT holds ( dim ( REAL-US n)) = n

    proof

      let n be Element of NAT ;

      reconsider B = ( RN_Base n) as Subset of ( REAL-US n) by REAL_NS1:def 6;

      for I be Basis of ( REAL-US n) holds n = ( card I)

      proof

        let I be Basis of ( REAL-US n);

        B is Basis of ( REAL-US n) by Th48;

        then ( card B) = ( card I) by RUSUB_4: 5;

        hence n = ( card I) by Lm5;

      end;

      hence thesis by RUSUB_4:def 2;

    end;

    theorem :: EUCLID_7:52

    for B be Orthogonal_Basis of n holds ( card B) = n

    proof

      let B be Orthogonal_Basis of n;

      reconsider B0 = B as Subset of ( RealVectSpace ( Seg n)) by FINSEQ_2: 93;

      B0 is Basis of ( RealVectSpace ( Seg n)) by Th49;

      hence ( card B) = n by Th46;

    end;