comseq_1.miz



    begin

    reserve f for Function;

    reserve n,k,n1 for Element of NAT ;

    reserve r,p for Complex;

    reserve x,y for set;

    definition

      mode Complex_Sequence is sequence of COMPLEX ;

    end

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

    theorem :: COMSEQ_1:1

    

     Th1: f is Complex_Sequence iff (( dom f) = NAT & for x st x in NAT holds (f . x) is Element of COMPLEX )

    proof

      thus f is Complex_Sequence implies (( dom f) = NAT & for x st x in NAT holds (f . x) is Element of COMPLEX )

      proof

        assume

         A1: f is Complex_Sequence;

        hence

         A2: ( dom f) = NAT by FUNCT_2:def 1;

        let x;

        assume x in NAT ;

        then

         A3: (f . x) in ( rng f) by A2, FUNCT_1:def 3;

        ( rng f) c= COMPLEX by A1, RELAT_1:def 19;

        hence thesis by A3;

      end;

      assume that

       A4: ( dom f) = NAT and

       A5: for x st x in NAT holds (f . x) is Element of COMPLEX ;

      now

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A6: x in ( dom f) and

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

        (f . x) is Element of COMPLEX by A4, A5, A6;

        hence y in COMPLEX by A7;

      end;

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

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

    end;

    theorem :: COMSEQ_1:2

    

     Th2: f is Complex_Sequence iff (( dom f) = NAT & for n holds (f . n) is Element of COMPLEX )

    proof

      thus f is Complex_Sequence implies (( dom f) = NAT & for n holds (f . n) is Element of COMPLEX ) by Th1;

      assume that

       A1: ( dom f) = NAT and

       A2: for n holds (f . n) is Element of COMPLEX ;

      for x holds x in NAT implies (f . x) is Element of COMPLEX by A2;

      hence thesis by A1, Th1;

    end;

    scheme :: COMSEQ_1:sch1

    ExComplexSeq { F( set) -> Complex } :

ex seq st for n be Nat 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 Element of COMPLEX by XCMPLX_0:def 2;

      end;

      then

      reconsider f as Complex_Sequence by A3, Th1;

      take seq = f;

      let n be Nat;

      n in NAT by ORDINAL1:def 12;

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

      hence thesis;

    end;

    registration

      cluster non-zero for Complex_Sequence;

      existence

      proof

        take s = ( NAT --> 1r );

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

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

      end;

    end

    theorem :: COMSEQ_1:3

    

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

    proof

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

      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) <> 0c ;

      assume 0 in ( rng seq);

      then 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 :: COMSEQ_1:4

    

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

    proof

      thus seq is non-zero implies for n holds (seq . n) <> 0c by Th3;

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

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

      hence thesis by Th3;

    end;

    theorem :: COMSEQ_1:5

    for IT be non-zero Complex_Sequence holds ( rng IT) c= ( COMPLEX \ { 0c }) by ORDINAL1:def 15, ZFMISC_1: 34;

    theorem :: COMSEQ_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 COMPLEX by XCMPLX_0:def 2;

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

      then

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

      take f;

      thus thesis by A2;

    end;

    theorem :: COMSEQ_1:7

    

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

    proof

      now

        let n;

        

        thus (((seq1 + seq2) + seq3) . n) = (((seq1 + seq2) qua Complex_Sequence . n) + (seq3 . n)) by VALUED_1: 1

        .= (((seq1 . n) + (seq2 . n)) + (seq3 . n)) by VALUED_1: 1

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

        .= ((seq1 . n) + ((seq2 + seq3) . n)) by VALUED_1: 1

        .= ((seq1 + (seq2 + seq3)) . n) by VALUED_1: 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:8

    

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

    proof

      now

        let n;

        

        thus (((seq1 (#) seq2) (#) seq3) . n) = (((seq1 (#) seq2) . n) * (seq3 . n)) by VALUED_1: 5

        .= (((seq1 . n) * (seq2 . n)) * (seq3 . n)) by VALUED_1: 5

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

        .= ((seq1 . n) * ((seq2 (#) seq3) . n)) by VALUED_1: 5

        .= ((seq1 (#) (seq2 (#) seq3)) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:9

    

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

    proof

      now

        let n;

        

        thus (((seq1 + seq2) (#) seq3) . n) = (((seq1 + seq2) . n) * (seq3 . n)) by VALUED_1: 5

        .= (((seq1 . n) + (seq2 . n)) * (seq3 . n)) by VALUED_1: 1

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

        .= (((seq1 (#) seq3) . n) + ((seq2 . n) * (seq3 . n))) by VALUED_1: 5

        .= (((seq1 (#) seq3) . n) + ((seq2 (#) seq3) . n)) by VALUED_1: 5

        .= (((seq1 (#) seq3) + (seq2 (#) seq3)) . n) by VALUED_1: 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:10

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

    theorem :: COMSEQ_1:11

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

    theorem :: COMSEQ_1:12

    

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

    proof

      now

        let n;

        

        thus ((r (#) (seq1 (#) seq2)) . n) = (r * ((seq1 (#) seq2) . n)) by VALUED_1: 6

        .= (r * ((seq1 . n) * (seq2 . n))) by VALUED_1: 5

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

        .= (((r (#) seq1) . n) * (seq2 . n)) by VALUED_1: 6

        .= (((r (#) seq1) (#) seq2) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:13

    

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

    proof

      now

        let n;

        

        thus ((r (#) (seq1 (#) seq2)) . n) = (r * ((seq1 (#) seq2) . n)) by VALUED_1: 6

        .= (r * ((seq1 . n) * (seq2 . n))) by VALUED_1: 5

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

        .= ((seq1 . n) * ((r (#) seq2) . n)) by VALUED_1: 6

        .= ((seq1 (#) (r (#) seq2)) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:14

    

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

    proof

      

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

      .= ((seq1 (#) seq3) + ((( - 1r ) (#) seq2) (#) seq3))

      .= ((seq1 (#) seq3) + (( - 1r ) (#) (seq2 (#) seq3))) by Th12

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

    end;

    theorem :: COMSEQ_1:15

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

    theorem :: COMSEQ_1:16

    

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

    proof

      now

        let n;

        

        thus ((r (#) (seq1 + seq2)) . n) = (r * ((seq1 + seq2) . n)) by VALUED_1: 6

        .= (r * ((seq1 . n) + (seq2 . n))) by VALUED_1: 1

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

        .= (((r (#) seq1) . n) + (r * (seq2 . n))) by VALUED_1: 6

        .= (((r (#) seq1) . n) + ((r (#) seq2) . n)) by VALUED_1: 6

        .= (((r (#) seq1) + (r (#) seq2)) . n) by VALUED_1: 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:17

    

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

    proof

      now

        let n;

        

        thus (((r * p) (#) seq) . n) = ((r * p) * (seq . n)) by VALUED_1: 6

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

        .= (r * ((p (#) seq) . n)) by VALUED_1: 6

        .= ((r (#) (p (#) seq)) . n) by VALUED_1: 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:18

    

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

    proof

      

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

      .= ((r (#) seq1) + (r (#) (( - 1r ) (#) seq2)))

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

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

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

    end;

    theorem :: COMSEQ_1:19

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

    proof

      

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

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

    end;

    theorem :: COMSEQ_1:20

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

    proof

      

      thus (seq1 - (seq2 + seq3)) = (seq1 + (( - 1r ) (#) (seq2 + seq3)))

      .= (seq1 + ((( - 1r ) (#) seq2) + (( - 1r ) (#) seq3))) by Th16

      .= (seq1 + (( - seq2) + (( - 1r ) (#) seq3)))

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

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

    end;

    theorem :: COMSEQ_1:21

    ( 1r (#) seq) = seq

    proof

      now

        let n;

        

        thus (( 1r (#) seq) . n) = ( 1r * (seq . n)) by VALUED_1: 6

        .= (seq . n);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:22

    ( - ( - seq)) = seq;

    theorem :: COMSEQ_1:23

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

    theorem :: COMSEQ_1:24

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

    proof

      

      thus (seq1 - (seq2 - seq3)) = (seq1 + (( - 1r ) (#) (seq2 - seq3)))

      .= (seq1 + ((( - 1r ) (#) seq2) - (( - 1r ) (#) seq3))) by Th18

      .= (seq1 + (( - seq2) - (( - 1r ) (#) seq3)))

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

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

    end;

    theorem :: COMSEQ_1:25

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

    proof

      

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

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

    end;

    theorem :: COMSEQ_1:26

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

    theorem :: COMSEQ_1:27

    

     Th27: 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) = 0c by A2, Th4;

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

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

    end;

    ::$Canceled

    theorem :: COMSEQ_1:29

    

     Th28: 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 VALUED_1: 5;

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

          hence ((seq (#) seq1) . n) <> 0c by A2;

        end;

        hence thesis by Th4;

      end;

      assume

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

      now

        let n;

        ((seq (#) seq1) . n) = ((seq . n) * (seq1 . n)) by VALUED_1: 5;

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

      end;

      hence seq is non-zero by Th4;

      now

        let n;

        ((seq (#) seq1) . n) = ((seq . n) * (seq1 . n)) by VALUED_1: 5;

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

      end;

      hence thesis by Th4;

    end;

    theorem :: COMSEQ_1:30

    

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

    proof

      now

        let n;

        

        thus (((seq " ) (#) (seq1 " )) . n) = (((seq " ) . n) * ((seq1 " ) . n)) by VALUED_1: 5

        .= (((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 VALUED_1: 5

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:31

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

    proof

      assume

       A1: seq is non-zero;

      now

        let n;

        

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

        

        thus (((seq1 /" seq) (#) seq) . n) = (((seq1 (#) (seq " )) . n) * (seq . n)) by VALUED_1: 5

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

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

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

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

        .= (seq1 . n);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:32

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

    proof

      now

        let n;

        

        thus (((seq9 /" seq) (#) (seq19 /" seq1)) . n) = (((seq9 (#) (seq " )) . n) * ((seq19 /" seq1) . n)) by VALUED_1: 5

        .= (((seq9 . n) * ((seq " ) . n)) * ((seq19 (#) (seq1 " )) . n)) by VALUED_1: 5

        .= (((seq9 . n) * ((seq " ) . n)) * ((seq19 . n) * ((seq1 " ) . n))) by VALUED_1: 5

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

        .= ((seq9 . n) * ((seq19 . n) * (((seq " ) (#) (seq1 " )) . n))) by VALUED_1: 5

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

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

        .= (((seq9 (#) seq19) . n) * (((seq (#) seq1) " ) . n)) by VALUED_1: 5

        .= (((seq9 (#) seq19) /" (seq (#) seq1)) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:33

    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, Th27;

      hence thesis by A1, Th28;

    end;

    theorem :: COMSEQ_1:34

    

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

    proof

      now

        let n;

        

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:35

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

    proof

      

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

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

    end;

    theorem :: COMSEQ_1:36

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

    proof

      now

        let n;

        

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

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:37

    

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

    proof

      assume

       A1: seq1 is non-zero;

      now

        let n;

        

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

        

        thus ((seq2 /" seq) . n) = (((seq2 . n) * 1r ) * ((seq " ) . n)) by VALUED_1: 5

        .= (((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 VALUED_1: 5

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

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

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

        .= (((seq2 (#) seq1) /" (seq (#) seq1)) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:38

    

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

    proof

      assume that

       A1: r <> 0c and

       A2: seq is non-zero and

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

      consider n1 such that

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

      

       A5: (r * (seq . n1)) = 0c by A4, VALUED_1: 6;

      (seq . n1) <> 0c by A2, Th4;

      hence contradiction by A1, A5;

    end;

    theorem :: COMSEQ_1:39

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

    theorem :: COMSEQ_1:40

    

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

    proof

      now

        let n;

        

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

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

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

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

        .= (((r " ) (#) (seq " )) . n) by VALUED_1: 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:41

    

     Th40: seq is non-zero implies (( - seq) " ) = (( - 1r ) (#) (seq " ))

    proof

      (( - 1) " ) = ( - 1);

      hence thesis by Th39;

    end;

    theorem :: COMSEQ_1:42

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

    proof

      assume

       A1: seq is non-zero;

      

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

      .= ((( - 1r ) (#) seq1) (#) (seq " )) by Th12

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

      

      thus (seq1 /" ( - seq)) = (seq1 (#) (( - 1r ) (#) (seq " ))) by A1, Th40

      .= (( - 1r ) (#) (seq1 (#) (seq " ))) by Th13

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

    end;

    theorem :: COMSEQ_1:43

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

    proof

      

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

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

      

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

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

    end;

    theorem :: COMSEQ_1:44

    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, Th36

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

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

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

      

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

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

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

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

    end;

    theorem :: COMSEQ_1:45

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

    proof

      

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

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

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

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

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

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

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

    end;

    theorem :: COMSEQ_1:46

    

     Th45: |.(seq (#) seq9).| = ( |.seq.| (#) |.seq9.|)

    proof

      now

        let n;

        

        thus ( |.(seq (#) seq9).| . n) = |.((seq (#) seq9) . n).| by VALUED_1: 18

        .= |.((seq . n) * (seq9 . n)).| by VALUED_1: 5

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

        .= (( |.seq.| . n) * |.(seq9 . n).|) by VALUED_1: 18

        .= (( |.seq.| . n) * ( |.seq9.| . n)) by VALUED_1: 18

        .= (( |.seq.| (#) |.seq9.|) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    ::$Canceled

    theorem :: COMSEQ_1:48

    

     Th46: ( |.seq.| " ) = |.(seq " ).|

    proof

      now

        let n;

        

        thus ( |.(seq " ).| . n) = |.((seq " ) . n).| by VALUED_1: 18

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

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

        .= (1 / |.(seq . n).|) by COMPLEX1: 48, COMPLEX1: 67

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

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_1:49

     |.(seq9 /" seq).| = ( |.seq9.| /" |.seq.|)

    proof

      

      thus |.(seq9 /" seq).| = ( |.seq9.| (#) |.(seq " ).|) by Th45

      .= ( |.seq9.| /" |.seq.|) by Th46;

    end;

    theorem :: COMSEQ_1:50

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

    proof

      now

        let n;

        

        thus ( |.(r (#) seq).| . n) = |.((r (#) seq) . n).| by VALUED_1: 18

        .= |.(r * (seq . n)).| by VALUED_1: 6

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

        .= ( |.r.| * ( |.seq.| . n)) by VALUED_1: 18

        .= (( |.r.| (#) |.seq.|) . n) by VALUED_1: 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;