seq_1.miz



    begin

    reserve f for Function;

    reserve n,k,n1 for Nat;

    reserve r,p for Real;

    reserve x,y,z for object;

    definition

      mode Real_Sequence is sequence of REAL ;

    end

    reserve seq,seq1,seq2,seq3,seq9,seq19 for Real_Sequence;

    theorem :: SEQ_1:1

    

     Th1: f is Real_Sequence iff (( dom f) = NAT & for x st x in NAT holds (f . x) is real)

    proof

      thus f is Real_Sequence implies (( dom f) = NAT & for x st x in NAT holds (f . x) is real) by FUNCT_2:def 1;

      assume that

       A1: ( dom f) = NAT and

       A2: for x st x in NAT holds (f . x) is real;

      now

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) and

         A4: y = (f . x) by FUNCT_1:def 3;

        (f . x) is real by A1, A2, A3;

        hence y in REAL by A4, XREAL_0:def 1;

      end;

      then ( rng f) c= REAL by TARSKI:def 3;

      hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: SEQ_1:2

    

     Th2: f is Real_Sequence iff (( dom f) = NAT & for n holds (f . n) is real)

    proof

      thus f is Real_Sequence implies (( dom f) = NAT & for n holds (f . n) is real) by Th1;

      assume that

       A1: ( dom f) = NAT and

       A2: for n holds (f . n) is real;

      for x holds x in NAT implies (f . x) is real by A2;

      hence thesis by A1, Th1;

    end;

    registration

      cluster non-zero for PartFunc of NAT , REAL ;

      existence

      proof

        1 in NAT ;

        then 1 in REAL by NUMBERS: 19;

        then

        reconsider p = ( NAT --> 1) as PartFunc of NAT , REAL by FUNCOP_1: 46;

        take p;

        ( rng p) = {1} by FUNCOP_1: 8;

        hence not 0 in ( rng p) by TARSKI:def 1;

      end;

    end

    theorem :: SEQ_1:3

    for f be non-zero PartFunc of NAT , REAL holds ( rng f) c= ( REAL \ { 0 }) by ORDINAL1:def 15, ZFMISC_1: 34;

    theorem :: SEQ_1:4

    

     Th4: seq is non-zero iff for x st x in NAT holds (seq . x) <> 0

    proof

      thus seq is non-zero implies for x st x in NAT holds (seq . x) <> 0

      proof

        assume

         A1: seq is non-zero;

        let x;

        assume x in NAT ;

        then x in ( dom seq) by Th2;

        then (seq . x) in ( rng seq) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

      assume

       A2: for x st x in NAT holds (seq . x) <> 0 ;

      assume 0 in ( rng seq);

      then ex x be object st x in ( dom seq) & (seq . x) = 0 by FUNCT_1:def 3;

      hence contradiction by A2;

    end;

    theorem :: SEQ_1:5

    

     Th5: seq is non-zero iff for n holds (seq . n) <> 0

    proof

      thus seq is non-zero implies for n holds (seq . n) <> 0 by ORDINAL1:def 12, Th4;

      assume for n holds (seq . n) <> 0 ;

      then for x holds x in NAT implies (seq . x) <> 0 ;

      hence thesis by Th4;

    end;

    theorem :: SEQ_1:6

    for r holds ex seq st ( rng seq) = {r}

    proof

      let r;

      consider f such that

       A1: ( dom f) = NAT and

       A2: ( rng f) = {r} by FUNCT_1: 5;

      for x be object st x in {r} holds x in REAL by XREAL_0:def 1;

      then ( rng f) c= REAL by A2, TARSKI:def 3;

      then

      reconsider f as Real_Sequence by A1, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      thus thesis by A2;

    end;

    scheme :: SEQ_1:sch1

    ExRealSeq { F( object) -> Real } :

ex seq st for n holds (seq . n) = F(n);

      defpred P[ object, object] means ex n st n = $1 & $2 = F(n);

       A1:

      now

        let x be object;

        assume x in NAT ;

        then

        consider n such that

         A2: n = x;

        reconsider r2 = F(n) as object;

        take y = r2;

        thus P[x, y] by A2;

      end;

      consider f such that

       A3: ( dom f) = NAT and

       A4: for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A1);

      now

        let x;

        assume x in NAT ;

        then ex n st n = x & (f . x) = F(n) by A4;

        hence (f . x) is real;

      end;

      then

      reconsider f as Real_Sequence by A3, Th1;

      take seq = f;

      let n;

      n in NAT by ORDINAL1:def 12;

      then ex k st k = n & (seq . n) = F(k) by A4;

      hence thesis;

    end;

    scheme :: SEQ_1:sch2

    PartFuncExD9 { D,C() -> non empty set , P[ object, object] } :

ex f be PartFunc of D(), C() st (for d be Element of D() holds d in ( dom f) iff (ex c be Element of C() st P[d, c])) & for d be Element of D() st d in ( dom f) holds P[d, (f . d)];

      defpred X[ object] means ex c be Element of C() st P[$1, c];

      set x = the Element of C();

      defpred X2[ Element of D(), Element of C()] means ((ex c be Element of C() st P[$1, c]) implies P[$1, $2]) & ((for c be Element of C() holds not P[$1, c]) implies $2 = x);

      consider X be set such that

       A1: for x be object holds x in X iff x in D() & X[x] from XBOOLE_0:sch 1;

      for x be object holds x in X implies x in D() by A1;

      then

      reconsider X as Subset of D() by TARSKI:def 3;

      

       A2: for d be Element of D() holds ex z be Element of C() st X2[d, z]

      proof

        let d be Element of D();

        (for c be Element of C() holds not P[d, c]) implies ex z st ((ex c be Element of C() st P[d, c]) implies P[d, z]) & ((for c be Element of C() holds not P[d, c]) implies z = x);

        hence thesis;

      end;

      consider g be Function of D(), C() such that

       A3: for d be Element of D() holds X2[d, (g . d)] from FUNCT_2:sch 3( A2);

      reconsider f = (g | X) as PartFunc of D(), C();

      take f;

      

       A4: ( dom g) = D() by FUNCT_2:def 1;

      thus for d be Element of D() holds d in ( dom f) iff ex c be Element of C() st P[d, c]

      proof

        let d be Element of D();

        ( dom f) c= X by RELAT_1: 58;

        hence d in ( dom f) implies ex c be Element of C() st P[d, c] by A1;

        assume ex c be Element of C() st P[d, c];

        then d in X by A1;

        then d in (( dom g) /\ X) by A4, XBOOLE_0:def 4;

        hence thesis by RELAT_1: 61;

      end;

      let d be Element of D();

      assume

       A5: d in ( dom f);

      ( dom f) c= X by RELAT_1: 58;

      then ex c be Element of C() st P[d, c] by A1, A5;

      then P[d, (g . d)] by A3;

      hence thesis by A5, FUNCT_1: 47;

    end;

    scheme :: SEQ_1:sch3

    LambdaPFD9 { D,C() -> non empty set , F( object) -> Element of C() , P[ object] } :

ex f be PartFunc of D(), C() st (for d be Element of D() holds d in ( dom f) iff P[d]) & for d be Element of D() st d in ( dom f) holds (f . d) = F(d);

      defpred X[ Element of D(), set] means P[$1] & $2 = F($1);

      consider f be PartFunc of D(), C() such that

       A1: for d be Element of D() holds d in ( dom f) iff ex c be Element of C() st X[d, c] and

       A2: for d be Element of D() st d in ( dom f) holds X[d, (f . d)] from PartFuncExD9;

      take f;

      thus for d be Element of D() holds d in ( dom f) iff P[d]

      proof

        let d be Element of D();

        thus d in ( dom f) implies P[d]

        proof

          assume d in ( dom f);

          then ex c be Element of C() st P[d] & c = F(d) by A1;

          hence thesis;

        end;

        assume P[d];

        then ex c be Element of C() st P[d] & c = F(d);

        hence thesis by A1;

      end;

      thus thesis by A2;

    end;

    scheme :: SEQ_1:sch4

    UnPartFuncD9 { C,D,X() -> set , F( object) -> object } :

for f,g be PartFunc of C(), D() st (( dom f) = X() & for c be Element of C() st c in ( dom f) holds (f . c) = F(c)) & (( dom g) = X() & for c be Element of C() st c in ( dom g) holds (g . c) = F(c)) holds f = g;

      let f,g be PartFunc of C(), D();

      assume that

       A1: ( dom f) = X() and

       A2: for c be Element of C() st c in ( dom f) holds (f . c) = F(c) and

       A3: ( dom g) = X() and

       A4: for c be Element of C() st c in ( dom g) holds (g . c) = F(c);

      now

        let c be Element of C();

        assume

         A5: c in ( dom f);

        

        hence (f . c) = F(c) by A2

        .= (g . c) by A1, A3, A4, A5;

      end;

      hence thesis by A1, A3, PARTFUN1: 5;

    end;

    theorem :: SEQ_1:7

    

     Th7: seq = (seq1 + seq2) iff for n holds (seq . n) = ((seq1 . n) + (seq2 . n))

    proof

      thus seq = (seq1 + seq2) implies for n holds (seq . n) = ((seq1 . n) + (seq2 . n))

      proof

        assume

         A1: seq = (seq1 + seq2);

        let n;

        

         A2: n in NAT by ORDINAL1:def 12;

        ( dom seq) = NAT by FUNCT_2:def 1;

        hence thesis by A1, VALUED_1:def 1, A2;

      end;

      assume for n holds (seq . n) = ((seq1 . n) + (seq2 . n));

      then

       A3: for n be object st n in ( dom seq) holds (seq . n) = ((seq1 . n) + (seq2 . n));

      ( dom seq) = ( NAT /\ NAT ) by FUNCT_2:def 1

      .= ( NAT /\ ( dom seq2)) by FUNCT_2:def 1

      .= (( dom seq1) /\ ( dom seq2)) by FUNCT_2:def 1;

      hence thesis by A3, VALUED_1:def 1;

    end;

    theorem :: SEQ_1:8

    

     Th8: seq = (seq1 (#) seq2) iff for n holds (seq . n) = ((seq1 . n) * (seq2 . n))

    proof

      thus seq = (seq1 (#) seq2) implies for n holds (seq . n) = ((seq1 . n) * (seq2 . n))

      proof

        assume

         A1: seq = (seq1 (#) seq2);

        let n;

        

         A2: n in NAT by ORDINAL1:def 12;

        ( dom seq) = NAT by FUNCT_2:def 1;

        hence thesis by A1, VALUED_1:def 4, A2;

      end;

      assume for n holds (seq . n) = ((seq1 . n) * (seq2 . n));

      then

       A3: for n be object st n in ( dom seq) holds (seq . n) = ((seq1 . n) * (seq2 . n));

      ( dom seq) = ( NAT /\ NAT ) by FUNCT_2:def 1

      .= ( NAT /\ ( dom seq2)) by FUNCT_2:def 1

      .= (( dom seq1) /\ ( dom seq2)) by FUNCT_2:def 1;

      hence thesis by A3, VALUED_1:def 4;

    end;

    theorem :: SEQ_1:9

    

     Th9: seq1 = (r (#) seq2) iff for n holds (seq1 . n) = (r * (seq2 . n))

    proof

      thus seq1 = (r (#) seq2) implies for n holds (seq1 . n) = (r * (seq2 . n)) by VALUED_1: 6;

      assume for n holds (seq1 . n) = (r * (seq2 . n));

      then

       A1: for n be object st n in ( dom seq1) holds (seq1 . n) = (r * (seq2 . n));

      ( dom seq1) = NAT by FUNCT_2:def 1

      .= ( dom seq2) by FUNCT_2:def 1;

      hence thesis by A1, VALUED_1:def 5;

    end;

    theorem :: SEQ_1:10

    seq1 = ( - seq2) iff for n holds (seq1 . n) = ( - (seq2 . n))

    proof

      thus seq1 = ( - seq2) implies for n holds (seq1 . n) = ( - (seq2 . n)) by VALUED_1: 8;

      assume for n holds (seq1 . n) = ( - (seq2 . n));

      then

       A1: for n be object st n in ( dom seq1) holds (seq1 . n) = ( - (seq2 . n));

      ( dom seq1) = NAT by FUNCT_2:def 1

      .= ( dom seq2) by FUNCT_2:def 1;

      hence thesis by A1, VALUED_1: 9;

    end;

    theorem :: SEQ_1:11

    (seq1 - seq2) = (seq1 + ( - seq2));

    theorem :: SEQ_1:12

    

     Th12: seq1 = ( abs seq) iff for n holds (seq1 . n) = |.(seq . n).|

    proof

      thus seq1 = ( abs seq) implies for n holds (seq1 . n) = |.(seq . n).| by VALUED_1: 18;

      assume for n holds (seq1 . n) = |.(seq . n).|;

      then

       A1: for n be object st n in ( dom seq1) holds (seq1 . n) = |.(seq . n).|;

      ( dom seq1) = NAT by FUNCT_2:def 1

      .= ( dom seq) by FUNCT_2:def 1;

      hence thesis by A1, VALUED_1:def 11;

    end;

    theorem :: SEQ_1:13

    

     Th13: ((seq1 + seq2) + seq3) = (seq1 + (seq2 + seq3))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq1 + seq2) + seq3) . n) = (((seq1 + seq2) . n) + (seq3 . n)) by Th7

        .= (((seq1 . n) + (seq2 . n)) + (seq3 . n)) by Th7

        .= ((seq1 . n) + ((seq2 . n) + (seq3 . n)))

        .= ((seq1 . n) + ((seq2 + seq3) . n)) by Th7

        .= ((seq1 + (seq2 + seq3)) . n) by Th7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:14

    

     Th14: ((seq1 (#) seq2) (#) seq3) = (seq1 (#) (seq2 (#) seq3))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq1 (#) seq2) (#) seq3) . n) = (((seq1 (#) seq2) . n) * (seq3 . n)) by Th8

        .= (((seq1 . n) * (seq2 . n)) * (seq3 . n)) by Th8

        .= ((seq1 . n) * ((seq2 . n) * (seq3 . n)))

        .= ((seq1 . n) * ((seq2 (#) seq3) . n)) by Th8

        .= ((seq1 (#) (seq2 (#) seq3)) . n) by Th8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:15

    

     Th15: ((seq1 + seq2) (#) seq3) = ((seq1 (#) seq3) + (seq2 (#) seq3))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq1 + seq2) (#) seq3) . n) = (((seq1 + seq2) . n) * (seq3 . n)) by Th8

        .= (((seq1 . n) + (seq2 . n)) * (seq3 . n)) by Th7

        .= (((seq1 . n) * (seq3 . n)) + ((seq2 . n) * (seq3 . n)))

        .= (((seq1 (#) seq3) . n) + ((seq2 . n) * (seq3 . n))) by Th8

        .= (((seq1 (#) seq3) . n) + ((seq2 (#) seq3) . n)) by Th8

        .= (((seq1 (#) seq3) + (seq2 (#) seq3)) . n) by Th7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:16

    (seq3 (#) (seq1 + seq2)) = ((seq3 (#) seq1) + (seq3 (#) seq2)) by Th15;

    theorem :: SEQ_1:17

    ( - seq) = (( - 1) (#) seq);

    theorem :: SEQ_1:18

    

     Th18: (r (#) (seq1 (#) seq2)) = ((r (#) seq1) (#) seq2)

    proof

      now

        let n be Element of NAT ;

        

        thus ((r (#) (seq1 (#) seq2)) . n) = (r * ((seq1 (#) seq2) . n)) by Th9

        .= (r * ((seq1 . n) * (seq2 . n))) by Th8

        .= ((r * (seq1 . n)) * (seq2 . n))

        .= (((r (#) seq1) . n) * (seq2 . n)) by Th9

        .= (((r (#) seq1) (#) seq2) . n) by Th8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:19

    

     Th19: (r (#) (seq1 (#) seq2)) = (seq1 (#) (r (#) seq2))

    proof

      now

        let n be Element of NAT ;

        

        thus ((r (#) (seq1 (#) seq2)) . n) = (r * ((seq1 (#) seq2) . n)) by Th9

        .= (r * ((seq1 . n) * (seq2 . n))) by Th8

        .= ((seq1 . n) * (r * (seq2 . n)))

        .= ((seq1 . n) * ((r (#) seq2) . n)) by Th9

        .= ((seq1 (#) (r (#) seq2)) . n) by Th8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:20

    

     Th20: ((seq1 - seq2) (#) seq3) = ((seq1 (#) seq3) - (seq2 (#) seq3))

    proof

      

      thus ((seq1 - seq2) (#) seq3) = ((seq1 (#) seq3) + (( - seq2) (#) seq3)) by Th15

      .= ((seq1 (#) seq3) - (seq2 (#) seq3)) by Th18;

    end;

    theorem :: SEQ_1:21

    ((seq3 (#) seq1) - (seq3 (#) seq2)) = (seq3 (#) (seq1 - seq2)) by Th20;

    theorem :: SEQ_1:22

    

     Th22: (r (#) (seq1 + seq2)) = ((r (#) seq1) + (r (#) seq2))

    proof

      now

        let n be Element of NAT ;

        

        thus ((r (#) (seq1 + seq2)) . n) = (r * ((seq1 + seq2) . n)) by Th9

        .= (r * ((seq1 . n) + (seq2 . n))) by Th7

        .= ((r * (seq1 . n)) + (r * (seq2 . n)))

        .= (((r (#) seq1) . n) + (r * (seq2 . n))) by Th9

        .= (((r (#) seq1) . n) + ((r (#) seq2) . n)) by Th9

        .= (((r (#) seq1) + (r (#) seq2)) . n) by Th7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:23

    

     Th23: ((r * p) (#) seq) = (r (#) (p (#) seq))

    proof

      now

        let n be Element of NAT ;

        

        thus (((r * p) (#) seq) . n) = ((r * p) * (seq . n)) by Th9

        .= (r * (p * (seq . n)))

        .= (r * ((p (#) seq) . n)) by Th9

        .= ((r (#) (p (#) seq)) . n) by Th9;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:24

    

     Th24: (r (#) (seq1 - seq2)) = ((r (#) seq1) - (r (#) seq2))

    proof

      

      thus (r (#) (seq1 - seq2)) = ((r (#) seq1) + (r (#) ( - seq2))) by Th22

      .= ((r (#) seq1) + ((( - 1) * r) (#) seq2)) by Th23

      .= ((r (#) seq1) - (r (#) seq2)) by Th23;

    end;

    theorem :: SEQ_1:25

    (r (#) (seq1 /" seq)) = ((r (#) seq1) /" seq)

    proof

      

      thus (r (#) (seq1 /" seq)) = (r (#) (seq1 (#) (seq " )))

      .= ((r (#) seq1) /" seq) by Th18;

    end;

    theorem :: SEQ_1:26

    (seq1 - (seq2 + seq3)) = ((seq1 - seq2) - seq3)

    proof

      

      thus (seq1 - (seq2 + seq3)) = (seq1 + (( - seq2) + (( - 1) (#) seq3))) by Th22

      .= ((seq1 - seq2) - seq3) by Th13;

    end;

    theorem :: SEQ_1:27

    (1 (#) seq) = seq

    proof

      now

        let n be Element of NAT ;

        

        thus ((1 (#) seq) . n) = (1 * (seq . n)) by Th9

        .= (seq . n);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    ::$Canceled

    theorem :: SEQ_1:29

    (seq1 - ( - seq2)) = (seq1 + seq2);

    theorem :: SEQ_1:30

    (seq1 - (seq2 - seq3)) = ((seq1 - seq2) + seq3)

    proof

      

      thus (seq1 - (seq2 - seq3)) = (seq1 + (( - seq2) - ( - seq3))) by Th24

      .= ((seq1 - seq2) + seq3) by Th13;

    end;

    theorem :: SEQ_1:31

    (seq1 + (seq2 - seq3)) = ((seq1 + seq2) - seq3)

    proof

      

      thus (seq1 + (seq2 - seq3)) = ((seq1 + seq2) + ( - seq3)) by Th13

      .= ((seq1 + seq2) - seq3);

    end;

    theorem :: SEQ_1:32

    (( - seq1) (#) seq2) = ( - (seq1 (#) seq2)) & (seq1 (#) ( - seq2)) = ( - (seq1 (#) seq2)) by Th18;

    theorem :: SEQ_1:33

    

     Th32: seq is non-zero implies (seq " ) is non-zero

    proof

      assume that

       A1: seq is non-zero and

       A2: not (seq " ) is non-zero;

      consider n1 such that

       A3: ((seq " ) . n1) = 0 by A2, Th5;

      ((seq . n1) " ) = ((seq " ) . n1) by VALUED_1: 10;

      hence contradiction by A1, A3, Th5, XCMPLX_1: 202;

    end;

    ::$Canceled

    theorem :: SEQ_1:35

    

     Th33: seq is non-zero & seq1 is non-zero iff (seq (#) seq1) is non-zero

    proof

      thus seq is non-zero & seq1 is non-zero implies (seq (#) seq1) is non-zero

      proof

        assume

         A1: seq is non-zero & seq1 is non-zero;

        now

          let n;

          

           A2: ((seq (#) seq1) . n) = ((seq . n) * (seq1 . n)) by Th8;

          (seq . n) <> 0 & (seq1 . n) <> 0 by A1, Th5;

          hence ((seq (#) seq1) . n) <> 0 by A2, XCMPLX_1: 6;

        end;

        hence thesis by Th5;

      end;

      assume

       A3: (seq (#) seq1) is non-zero;

      now

        let n;

        ((seq (#) seq1) . n) = ((seq . n) * (seq1 . n)) by Th8;

        hence (seq . n) <> 0 by A3, Th5;

      end;

      hence seq is non-zero by Th5;

      now

        let n;

        ((seq (#) seq1) . n) = ((seq . n) * (seq1 . n)) by Th8;

        hence (seq1 . n) <> 0 by A3, Th5;

      end;

      hence thesis by Th5;

    end;

    theorem :: SEQ_1:36

    

     Th34: ((seq " ) (#) (seq1 " )) = ((seq (#) seq1) " )

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq " ) (#) (seq1 " )) . n) = (((seq " ) . n) * ((seq1 " ) . n)) by Th8

        .= (((seq " ) . n) * ((seq1 . n) " )) by VALUED_1: 10

        .= (((seq . n) " ) * ((seq1 . n) " )) by VALUED_1: 10

        .= (((seq . n) * (seq1 . n)) " ) by XCMPLX_1: 204

        .= (((seq (#) seq1) . n) " ) by Th8

        .= (((seq (#) seq1) " ) . n) by VALUED_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:37

    seq is non-zero implies ((seq1 /" seq) (#) seq) = seq1

    proof

      assume

       A1: seq is non-zero;

      now

        let n be Element of NAT ;

        

         A2: (seq . n) <> 0 by A1, Th5;

        

        thus (((seq1 /" seq) (#) seq) . n) = (((seq1 (#) (seq " )) . n) * (seq . n)) by Th8

        .= (((seq1 . n) * ((seq " ) . n)) * (seq . n)) by Th8

        .= (((seq1 . n) * ((seq . n) " )) * (seq . n)) by VALUED_1: 10

        .= ((seq1 . n) * (((seq . n) " ) * (seq . n)))

        .= ((seq1 . n) * 1) by A2, XCMPLX_0:def 7

        .= (seq1 . n);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:38

    ((seq9 /" seq) (#) (seq19 /" seq1)) = ((seq9 (#) seq19) /" (seq (#) seq1))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq9 /" seq) (#) (seq19 /" seq1)) . n) = (((seq9 (#) (seq " )) . n) * ((seq19 /" seq1) . n)) by Th8

        .= (((seq9 . n) * ((seq " ) . n)) * ((seq19 (#) (seq1 " )) . n)) by Th8

        .= (((seq9 . n) * ((seq " ) . n)) * ((seq19 . n) * ((seq1 " ) . n))) by Th8

        .= ((seq9 . n) * ((seq19 . n) * (((seq " ) . n) * ((seq1 " ) . n))))

        .= ((seq9 . n) * ((seq19 . n) * (((seq " ) (#) (seq1 " )) . n))) by Th8

        .= (((seq9 . n) * (seq19 . n)) * (((seq " ) (#) (seq1 " )) . n))

        .= (((seq9 . n) * (seq19 . n)) * (((seq (#) seq1) " ) . n)) by Th34

        .= (((seq9 (#) seq19) . n) * (((seq (#) seq1) " ) . n)) by Th8

        .= (((seq9 (#) seq19) /" (seq (#) seq1)) . n) by Th8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:39

    seq is non-zero & seq1 is non-zero implies (seq /" seq1) is non-zero

    proof

      assume that

       A1: seq is non-zero and

       A2: seq1 is non-zero;

      (seq1 " ) is non-zero by A2, Th32;

      hence thesis by A1, Th33;

    end;

    theorem :: SEQ_1:40

    

     Th38: ((seq /" seq1) " ) = (seq1 /" seq)

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq /" seq1) " ) . n) = (((seq " ) (#) ((seq1 " ) " )) . n) by Th34

        .= ((seq1 /" seq) . n);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:41

    (seq2 (#) (seq1 /" seq)) = ((seq2 (#) seq1) /" seq)

    proof

      

      thus (seq2 (#) (seq1 /" seq)) = (seq2 (#) (seq1 (#) (seq " )))

      .= ((seq2 (#) seq1) /" seq) by Th14;

    end;

    theorem :: SEQ_1:42

    (seq2 /" (seq /" seq1)) = ((seq2 (#) seq1) /" seq)

    proof

      

      thus (seq2 /" (seq /" seq1)) = (seq2 (#) (seq1 /" seq)) by Th38

      .= (seq2 (#) (seq1 (#) (seq " )))

      .= ((seq2 (#) seq1) /" seq) by Th14;

    end;

    theorem :: SEQ_1:43

    

     Th41: seq1 is non-zero implies (seq2 /" seq) = ((seq2 (#) seq1) /" (seq (#) seq1))

    proof

      assume

       A1: seq1 is non-zero;

      now

        let n be Element of NAT ;

        

         A2: (seq1 . n) <> 0 by A1, Th5;

        

        thus ((seq2 /" seq) . n) = (((seq2 . n) * 1) * ((seq " ) . n)) by Th8

        .= (((seq2 . n) * ((seq1 . n) * ((seq1 . n) " ))) * ((seq " ) . n)) by A2, XCMPLX_0:def 7

        .= (((seq2 . n) * (seq1 . n)) * (((seq1 . n) " ) * ((seq " ) . n)))

        .= (((seq2 (#) seq1) . n) * (((seq1 . n) " ) * ((seq " ) . n))) by Th8

        .= (((seq2 (#) seq1) . n) * (((seq1 " ) . n) * ((seq " ) . n))) by VALUED_1: 10

        .= (((seq2 (#) seq1) . n) * (((seq " ) (#) (seq1 " )) . n)) by Th8

        .= (((seq2 (#) seq1) . n) * (((seq (#) seq1) " ) . n)) by Th34

        .= (((seq2 (#) seq1) /" (seq (#) seq1)) . n) by Th8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:44

    

     Th42: r <> 0 & seq is non-zero implies (r (#) seq) is non-zero

    proof

      assume that

       A1: r <> 0 and

       A2: seq is non-zero and

       A3: not (r (#) seq) is non-zero;

      consider n1 such that

       A4: ((r (#) seq) . n1) = 0 by A3, Th5;

      

       A5: (seq . n1) <> 0 by A2, Th5;

      (r * (seq . n1)) = 0 by A4, Th9;

      hence contradiction by A1, A5, XCMPLX_1: 6;

    end;

    theorem :: SEQ_1:45

    seq is non-zero implies ( - seq) is non-zero by Th42;

    theorem :: SEQ_1:46

    

     Th44: ((r (#) seq) " ) = ((r " ) (#) (seq " ))

    proof

      now

        let n be Element of NAT ;

        

        thus (((r (#) seq) " ) . n) = (((r (#) seq) . n) " ) by VALUED_1: 10

        .= ((r * (seq . n)) " ) by Th9

        .= ((r " ) * ((seq . n) " )) by XCMPLX_1: 204

        .= ((r " ) * ((seq " ) . n)) by VALUED_1: 10

        .= (((r " ) (#) (seq " )) . n) by Th9;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm1: (( - 1) " ) = ( - 1);

    theorem :: SEQ_1:47

    (( - seq) " ) = (( - 1) (#) (seq " )) by Lm1, Th44;

    theorem :: SEQ_1:48

    ( - (seq1 /" seq)) = (( - seq1) /" seq) & (seq1 /" ( - seq)) = ( - (seq1 /" seq))

    proof

      

      thus ( - (seq1 /" seq)) = (( - 1) (#) (seq1 (#) (seq " )))

      .= (( - seq1) /" seq) by Th18;

      

      thus (seq1 /" ( - seq)) = (seq1 (#) (( - 1) (#) (seq " ))) by Lm1, Th44

      .= ( - (seq1 /" seq)) by Th19;

    end;

    theorem :: SEQ_1:49

    ((seq1 /" seq) + (seq19 /" seq)) = ((seq1 + seq19) /" seq) & ((seq1 /" seq) - (seq19 /" seq)) = ((seq1 - seq19) /" seq)

    proof

      

      thus ((seq1 /" seq) + (seq19 /" seq)) = ((seq1 + seq19) (#) (seq " )) by Th15

      .= ((seq1 + seq19) /" seq);

      

      thus ((seq1 /" seq) - (seq19 /" seq)) = ((seq1 - seq19) (#) (seq " )) by Th20

      .= ((seq1 - seq19) /" seq);

    end;

    theorem :: SEQ_1:50

    seq is non-zero & seq9 is non-zero implies ((seq1 /" seq) + (seq19 /" seq9)) = (((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9)) & ((seq1 /" seq) - (seq19 /" seq9)) = (((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9))

    proof

      assume that

       A1: seq is non-zero and

       A2: seq9 is non-zero;

      

      thus ((seq1 /" seq) + (seq19 /" seq9)) = (((seq1 (#) seq9) /" (seq (#) seq9)) + (seq19 /" seq9)) by A2, Th41

      .= (((seq1 (#) seq9) /" (seq (#) seq9)) + ((seq19 (#) seq) /" (seq (#) seq9))) by A1, Th41

      .= (((seq1 (#) seq9) + (seq19 (#) seq)) (#) ((seq (#) seq9) " )) by Th15

      .= (((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9));

      

      thus ((seq1 /" seq) - (seq19 /" seq9)) = (((seq1 (#) seq9) /" (seq (#) seq9)) - (seq19 /" seq9)) by A2, Th41

      .= (((seq1 (#) seq9) /" (seq (#) seq9)) - ((seq19 (#) seq) /" (seq (#) seq9))) by A1, Th41

      .= (((seq1 (#) seq9) - (seq19 (#) seq)) (#) ((seq (#) seq9) " )) by Th20

      .= (((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9));

    end;

    theorem :: SEQ_1:51

    ((seq19 /" seq) /" (seq9 /" seq1)) = ((seq19 (#) seq1) /" (seq (#) seq9))

    proof

      

      thus ((seq19 /" seq) /" (seq9 /" seq1)) = ((seq19 /" seq) (#) ((seq9 " ) (#) ((seq1 " ) " ))) by Th34

      .= (((seq19 (#) (seq " )) (#) seq1) (#) (seq9 " )) by Th14

      .= ((seq19 (#) (seq1 (#) (seq " ))) (#) (seq9 " )) by Th14

      .= (seq19 (#) ((seq1 (#) (seq " )) (#) (seq9 " ))) by Th14

      .= (seq19 (#) (seq1 (#) ((seq " ) (#) (seq9 " )))) by Th14

      .= ((seq19 (#) seq1) (#) ((seq " ) (#) (seq9 " ))) by Th14

      .= ((seq19 (#) seq1) /" (seq (#) seq9)) by Th34;

    end;

    theorem :: SEQ_1:52

    

     Th50: ( abs (seq (#) seq9)) = (( abs seq) (#) ( abs seq9))

    proof

      now

        let n be Element of NAT ;

        

        thus (( abs (seq (#) seq9)) . n) = |.((seq (#) seq9) . n).| by Th12

        .= |.((seq . n) * (seq9 . n)).| by Th8

        .= ( |.(seq . n).| * |.(seq9 . n).|) by COMPLEX1: 65

        .= ((( abs seq) . n) * |.(seq9 . n).|) by Th12

        .= ((( abs seq) . n) * (( abs seq9) . n)) by Th12

        .= ((( abs seq) (#) ( abs seq9)) . n) by Th8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:53

    seq is non-zero implies ( abs seq) is non-zero

    proof

      assume

       A1: seq is non-zero;

      now

        let n;

        (seq . n) <> 0 by A1, Th5;

        then |.(seq . n).| <> 0 by COMPLEX1: 47;

        hence (( abs seq) . n) <> 0 by Th12;

      end;

      hence thesis by Th5;

    end;

    theorem :: SEQ_1:54

    

     Th52: (( abs seq) " ) = ( abs (seq " ))

    proof

      now

        let n be Element of NAT ;

        

        thus (( abs (seq " )) . n) = |.((seq " ) . n).| by Th12

        .= |.((seq . n) " ).| by VALUED_1: 10

        .= |.(1 / (seq . n)).| by XCMPLX_1: 215

        .= (1 / |.(seq . n).|) by ABSVALUE: 7

        .= ( |.(seq . n).| " ) by XCMPLX_1: 215

        .= ((( abs seq) . n) " ) by Th12

        .= ((( abs seq) " ) . n) by VALUED_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQ_1:55

    ( abs (seq9 /" seq)) = (( abs seq9) /" ( abs seq))

    proof

      

      thus ( abs (seq9 /" seq)) = (( abs seq9) (#) ( abs (seq " ))) by Th50

      .= (( abs seq9) /" ( abs seq)) by Th52;

    end;

    theorem :: SEQ_1:56

    ( abs (r (#) seq)) = ( |.r.| (#) ( abs seq))

    proof

      now

        let n be Element of NAT ;

        

        thus (( abs (r (#) seq)) . n) = |.((r (#) seq) . n).| by Th12

        .= |.(r * (seq . n)).| by Th9

        .= ( |.r.| * |.(seq . n).|) by COMPLEX1: 65

        .= ( |.r.| * (( abs seq) . n)) by Th12

        .= (( |.r.| (#) ( abs seq)) . n) by Th9;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let b be Real;

      :: SEQ_1:def1

      func seq_const b -> Real_Sequence equals

      : Def1: ( NAT --> b);

      coherence

      proof

        reconsider b as Element of REAL by XREAL_0:def 1;

        ( NAT --> b) is Real_Sequence;

        hence thesis;

      end;

    end

    registration

      let b be Real;

      cluster ( seq_const b) -> constant;

      coherence ;

    end

    registration

      let b be non zero Real;

      cluster ( seq_const b) -> non-zero;

      coherence

      proof

        ( rng ( seq_const b)) = {b} by FUNCOP_1: 8;

        hence not 0 in ( rng ( seq_const b)) by TARSKI:def 1;

      end;

    end

    registration

      cluster constant for Real_Sequence;

      existence

      proof

        take ( seq_const 0 );

        thus thesis;

      end;

    end

    theorem :: SEQ_1:57

    for a be Real, k be Nat holds (( seq_const a) . k) = a by ORDINAL1:def 12, FUNCOP_1: 7;

    registration

      let k be object;

      reduce (( NAT --> 0 ) . k) to 0 ;

      reducibility

      proof

        

         A1: ( dom ( NAT --> 0 )) = NAT ;

        per cases ;

          suppose k in NAT ;

          hence thesis by FUNCOP_1: 7;

        end;

          suppose not k in NAT ;

          hence thesis by A1, FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let k be object;

      reduce (( seq_const 0 ) . k) to 0 ;

      reducibility ;

    end