finseq_5.miz



    begin

    reserve i,j,k,n for Nat;

    theorem :: FINSEQ_5:1

    

     Th1: for i,n be Nat holds i <= n implies ((n - i) + 1) is Element of NAT

    proof

      let i,n be Nat;

      assume i <= n;

      then

      reconsider ni = (n - i) as Element of NAT by INT_1: 5;

      (ni + 1) is Element of NAT ;

      hence thesis;

    end;

    theorem :: FINSEQ_5:2

    

     Th2: for i,n be Nat holds i in ( Seg n) implies ((n - i) + 1) in ( Seg n)

    proof

      let i,n be Nat;

      assume

       A1: i in ( Seg n);

      then i <= n by FINSEQ_1: 1;

      then

      reconsider ni = (n - i) as Element of NAT by INT_1: 5;

      reconsider j = (ni + 1) as Element of NAT ;

       A2:

      now

        assume j = (n + 1);

        then ( - 0 ) = ( - i);

        hence contradiction by A1, FINSEQ_1: 1;

      end;

      j <= (n + 1) by XREAL_1: 6, XREAL_1: 43;

      then j < (n + 1) by A2, XXREAL_0: 1;

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

      hence thesis;

    end;

    theorem :: FINSEQ_5:3

    

     Th3: for f be Function, x,y be object st (f " {y}) = {x} holds x in ( dom f) & y in ( rng f) & (f . x) = y

    proof

      let f be Function, x,y be object;

      assume (f " {y}) = {x};

      then

       A1: x in (f " {y}) by TARSKI:def 1;

      hence

       A2: x in ( dom f) by FUNCT_1:def 7;

      (f . x) in {y} by A1, FUNCT_1:def 7;

      then (f . x) = y by TARSKI:def 1;

      hence thesis by A2, FUNCT_1:def 3;

    end;

    theorem :: FINSEQ_5:4

    for f be Function holds f is one-to-one iff for x be set st x in ( dom f) holds (f " {(f . x)}) = {x}

    proof

      let f be Function;

      now

        hereby

          assume

           A1: for x be object st x in ( dom f) holds f is_one-to-one_at x;

          let x be object;

          assume x in ( dom f);

          then f is_one-to-one_at x by A1;

          hence (f " {(f . x)}) = {x} by FINSEQ_4: 2;

        end;

        assume

         A2: for x be object st x in ( dom f) holds (f " {(f . x)}) = {x};

        let x be object;

        assume

         A3: x in ( dom f);

        then (f " {(f . x)}) = {x} by A2;

        hence f is_one-to-one_at x by A3, FINSEQ_4: 2;

      end;

      hence thesis by FINSEQ_4: 4;

    end;

    theorem :: FINSEQ_5:5

    for f be Function, y1,y2 be object st f is one-to-one & y1 in ( rng f) & (f " {y1}) = (f " {y2}) holds y1 = y2

    proof

      let f be Function, y1,y2 be object such that

       A1: f is one-to-one & y1 in ( rng f) and

       A2: (f " {y1}) = (f " {y2});

      consider x1 be object such that

       A3: (f " {y1}) = {x1} by A1, FUNCT_1: 74;

      (f . x1) = y1 by A3, Th3;

      hence thesis by A2, A3, Th3;

    end;

    registration

      let x be object;

      cluster <*x*> -> trivial;

      coherence ;

      let y be object;

      cluster <*x, y*> -> non trivial;

      coherence

      proof

        ( len <*x, y*>) = 2 by FINSEQ_1: 44;

        hence thesis by NAT_D: 60;

      end;

    end

    registration

      cluster one-to-one non empty for FinSequence;

      existence

      proof

        set f = <* {} *>;

        f is one-to-one by FINSEQ_3: 93;

        hence thesis;

      end;

    end

    theorem :: FINSEQ_5:6

    

     Th6: for f be non empty FinSequence holds 1 in ( dom f) & ( len f) in ( dom f)

    proof

      let f be non empty FinSequence;

      

       A1: ( len f) >= 1 by NAT_1: 14;

      hence 1 in ( dom f) by FINSEQ_3: 25;

      thus thesis by A1, FINSEQ_3: 25;

    end;

    theorem :: FINSEQ_5:7

    for f be non empty FinSequence holds ex i be Nat st (i + 1) = ( len f) by NAT_1: 6;

    theorem :: FINSEQ_5:8

    

     Th8: for x be object, f be FinSequence holds ( len ( <*x*> ^ f)) = (1 + ( len f))

    proof

      let x be object, f be FinSequence;

      

      thus ( len ( <*x*> ^ f)) = (( len <*x*>) + ( len f)) by FINSEQ_1: 22

      .= (1 + ( len f)) by FINSEQ_1: 39;

    end;

    theorem :: FINSEQ_5:9

    for f be FinSequence, p,q be set st p in ( rng f) & q in ( rng f) & (p .. f) = (q .. f) holds p = q

    proof

      let f be FinSequence, p,q be set such that

       A1: p in ( rng f) and

       A2: q in ( rng f);

      assume (p .. f) = (q .. f);

      

      hence p = (f . (q .. f)) by A1, FINSEQ_4: 19

      .= q by A2, FINSEQ_4: 19;

    end;

    theorem :: FINSEQ_5:10

    

     Th10: for f,g be FinSequence st (n + 1) in ( dom f) & g = (f | ( Seg n)) holds (f | ( Seg (n + 1))) = (g ^ <*(f . (n + 1))*>)

    proof

      let f,g be FinSequence such that

       A1: (n + 1) in ( dom f) and

       A2: g = (f | ( Seg n));

      reconsider h = (f | ( Seg (n + 1))) as FinSequence by FINSEQ_1: 15;

      (n + 1) <= ( len f) by A1, FINSEQ_3: 25;

      then

       A3: ( len h) = (n + 1) by FINSEQ_1: 17;

      ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5, NAT_1: 11;

      then (h . (n + 1)) = (f . (n + 1)) & g = (h | ( Seg n)) by A2, FINSEQ_1: 4, FUNCT_1: 49, FUNCT_1: 51;

      hence thesis by A3, FINSEQ_3: 55;

    end;

    theorem :: FINSEQ_5:11

    

     Th11: for f be one-to-one FinSequence st i in ( dom f) holds ((f . i) .. f) = i

    proof

      let f be one-to-one FinSequence;

      assume

       A1: i in ( dom f);

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

      then

       A2: f just_once_values (f . i) by FINSEQ_4: 8;

      then (f <- (f . i)) = ((f . i) .. f) by FINSEQ_4: 25;

      hence thesis by A1, A2, FINSEQ_4:def 3;

    end;

    reserve D for non empty set,

p for Element of D,

f,g for FinSequence of D;

    registration

      let D be non empty set;

      cluster one-to-one non empty for FinSequence of D;

      existence

      proof

        set x = the Element of D;

        set f = <*x*>;

        f is one-to-one by FINSEQ_3: 93;

        hence thesis;

      end;

    end

    theorem :: FINSEQ_5:12

    ( dom f) = ( dom g) & (for i st i in ( dom f) holds (f /. i) = (g /. i)) implies f = g

    proof

      assume that

       A1: ( dom f) = ( dom g) and

       A2: for i st i in ( dom f) holds (f /. i) = (g /. i);

      now

        let k be Nat;

        assume

         A3: k in ( dom f);

        

        hence (f . k) = (f /. k) by PARTFUN1:def 6

        .= (g /. k) by A2, A3

        .= (g . k) by A1, A3, PARTFUN1:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_5:13

    ( len f) = ( len g) & (for k st 1 <= k & k <= ( len f) holds (f /. k) = (g /. k)) implies f = g

    proof

      assume that

       A1: ( len f) = ( len g) and

       A2: for k st 1 <= k & k <= ( len f) holds (f /. k) = (g /. k);

      now

        let k be Nat;

        assume

         A3: 1 <= k & k <= ( len f);

        

        hence (f . k) = (f /. k) by FINSEQ_4: 15

        .= (g /. k) by A2, A3

        .= (g . k) by A1, A3, FINSEQ_4: 15;

      end;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_5:14

    

     Th14: for f be FinSequence st ( len f) = 1 holds f = <*(f . 1)*> by FINSEQ_1: 40;

    theorem :: FINSEQ_5:15

    

     Th15: for D be non empty set, p be Element of D, f be FinSequence of D holds (( <*p*> ^ f) /. 1) = p

    proof

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

      ( len ( <*p*> ^ f)) = (1 + ( len f)) by Th8;

      then 1 <= ( len ( <*p*> ^ f)) by NAT_1: 11;

      then 1 in ( dom ( <*p*> ^ f)) by FINSEQ_3: 25;

      then (( <*p*> ^ f) /. 1) = (( <*p*> ^ f) . 1) by PARTFUN1:def 6;

      hence thesis by FINSEQ_1: 41;

    end;

    

     Lm1: i in ( dom f) implies ((f ^ g) . i) = (f . i) by FINSEQ_1:def 7;

    theorem :: FINSEQ_5:16

    

     Th16: for f be FinSequence, i be Nat holds ( len (f | i)) <= ( len f)

    proof

      let f be FinSequence, i be Nat;

      i <= ( len f) implies ( len (f | i)) = i by FINSEQ_1: 59;

      hence thesis by FINSEQ_1: 58;

    end;

    theorem :: FINSEQ_5:17

    

     Th17: for f be FinSequence, i be Nat holds ( len (f | i)) <= i

    proof

      let f be FinSequence, i be Nat;

      i <= ( len f) implies ( len (f | i)) = i by FINSEQ_1: 59;

      hence thesis by FINSEQ_1: 58;

    end;

    theorem :: FINSEQ_5:18

    

     Th18: for f be FinSequence, i be Nat holds ( dom (f | i)) c= ( dom f)

    proof

      let f be FinSequence, i be Nat;

      (f | i) c= f by RELAT_1: 59;

      hence thesis by RELAT_1: 11;

    end;

    theorem :: FINSEQ_5:19

    

     Th19: for f be FinSequence, i be Nat holds ( rng (f | i)) c= ( rng f)

    proof

      let f be FinSequence, i be Nat;

      (f | i) c= f by RELAT_1: 59;

      hence thesis by RELAT_1: 11;

    end;

    theorem :: FINSEQ_5:20

    

     Th20: for f be FinSequence st f is non empty holds (f | 1) = <*(f . 1)*>

    proof

      let f be FinSequence;

      assume f is non empty;

      then 1 in ( dom f) by Th6;

      then 1 <= ( len f) by FINSEQ_3: 25;

      then

       A1: ( len (f | 1)) = 1 by FINSEQ_1: 59;

      ((f | ( Seg 1)) . 1) = (f . 1) by FINSEQ_1: 1, FUNCT_1: 49;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_5:21

    (i + 1) = ( len f) implies f = ((f | i) ^ <*(f /. ( len f))*>)

    proof

      assume

       A1: (i + 1) = ( len f);

      then f is non empty;

      then

       A2: (i + 1) in ( dom f) by A1, Th6;

      ( dom f) = ( Seg (i + 1)) by A1, FINSEQ_1:def 3;

      

      hence f = (f | ( Seg (i + 1)))

      .= ((f | i) ^ <*(f . (i + 1))*>) by A2, Th10

      .= ((f | i) ^ <*(f /. ( len f))*>) by A1, A2, PARTFUN1:def 6;

    end;

    

     Lm2: f is one-to-one implies (f | i) is one-to-one

    proof

      assume

       A1: f is one-to-one;

      now

        

         A2: ( dom (f | i)) c= ( dom f) by Th18;

        let n,m be Element of NAT such that

         A3: n in ( dom (f | i)) and

         A4: m in ( dom (f | i)) and

         A5: ((f | i) /. n) = ((f | i) /. m);

        (f /. n) = ((f | i) /. n) by A3, FINSEQ_4: 70

        .= (f /. m) by A4, A5, FINSEQ_4: 70;

        hence n = m by A1, A3, A4, A2, PARTFUN2: 10;

      end;

      hence thesis by PARTFUN2: 9;

    end;

    registration

      let i, D;

      let f be one-to-one FinSequence of D;

      cluster (f | i) -> one-to-one;

      coherence by Lm2;

    end

    theorem :: FINSEQ_5:22

    

     Th22: for f,g be FinSequence st i <= ( len f) holds ((f ^ g) | i) = (f | i)

    proof

      let f,g be FinSequence;

      assume

       A1: i <= ( len f);

      then

       A2: ( len (f | i)) = i by FINSEQ_1: 59;

      then

       A3: ( dom (f | i)) = ( Seg i) by FINSEQ_1:def 3;

       A4:

      now

        let j be Nat;

        assume

         A5: j in ( dom (f | i));

        then j <= i by A3, FINSEQ_1: 1;

        then

         A6: j <= ( len f) by A1, XXREAL_0: 2;

        j in NAT & 1 <= j by A3, A5, FINSEQ_1: 1;

        then j in ( Seg ( len f)) by A6;

        then

         A7: j in ( dom f) by FINSEQ_1:def 3;

        

        thus (((f ^ g) | i) . j) = ((f ^ g) . j) by A3, A5, FUNCT_1: 49

        .= (f . j) by A7, FINSEQ_1:def 7

        .= ((f | i) . j) by A3, A5, FUNCT_1: 49;

      end;

      i <= (( len f) + ( len g)) by A1, NAT_1: 12;

      then i <= ( len (f ^ g)) by FINSEQ_1: 22;

      then ( len ((f ^ g) | i)) = i by FINSEQ_1: 59;

      hence thesis by A2, A4, FINSEQ_2: 9;

    end;

    theorem :: FINSEQ_5:23

    for f,g be FinSequence holds ((f ^ g) | ( len f)) = f

    proof

      let f,g be FinSequence;

      

      thus f = (f | ( len f)) by FINSEQ_2: 20

      .= ((f ^ g) | ( len f)) by Th22;

    end;

    theorem :: FINSEQ_5:24

    for f be FinSequence of D st p in ( rng f) holds ((f -| p) ^ <*p*>) = (f | (p .. f))

    proof

      let f be FinSequence of D;

      assume

       A1: p in ( rng f);

      then

      consider n be Nat such that

       A2: n = ((p .. f) - 1) and

       A3: (f -| p) = (f | ( Seg n)) by FINSEQ_4:def 5;

      (n + 1) in ( dom f) & (f . (n + 1)) = p by A1, A2, FINSEQ_4: 19, FINSEQ_4: 20;

      hence thesis by A2, A3, Th10;

    end;

    theorem :: FINSEQ_5:25

    for f be FinSequence holds ( len (f /^ i)) <= ( len f)

    proof

      let f be FinSequence;

      per cases ;

        suppose i <= ( len f);

        then ( len (f /^ i)) = (( len f) - i) by RFINSEQ:def 1;

        then (( len (f /^ i)) + i) = ( len f);

        hence thesis by NAT_1: 11;

      end;

        suppose ( len f) < i;

        then (f /^ i) = {} by RFINSEQ:def 1;

        hence thesis;

      end;

    end;

    theorem :: FINSEQ_5:26

    

     Th26: for f be FinSequence st i in ( dom (f /^ n)) holds (n + i) in ( dom f)

    proof

      let f be FinSequence;

      assume

       A1: i in ( dom (f /^ n));

      per cases ;

        suppose

         A2: n <= ( len f);

        i <= ( len (f /^ n)) by A1, FINSEQ_3: 25;

        then i <= (( len f) - n) by A2, RFINSEQ:def 1;

        then

         A3: (n + i) <= ( len f) by XREAL_1: 19;

        1 <= i & i <= (i + n) by A1, FINSEQ_3: 25, NAT_1: 11;

        then 1 <= (i + n) by XXREAL_0: 2;

        hence thesis by A3, FINSEQ_3: 25;

      end;

        suppose n > ( len f);

        then (f /^ n) = {} by RFINSEQ:def 1;

        hence thesis by A1;

      end;

    end;

    theorem :: FINSEQ_5:27

    

     Th27: (for f be FinSequence st i in ( dom (f /^ n)) holds ((f /^ n) . i) = (f . (n + i))) & (i in ( dom (f /^ n)) implies ((f /^ n) /. i) = (f /. (n + i)))

    proof

      thus

       AA: for f be FinSequence st i in ( dom (f /^ n)) holds ((f /^ n) . i) = (f . (n + i))

      proof

        let f be FinSequence;

        assume

         A1: i in ( dom (f /^ n));

        per cases ;

          suppose n <= ( len f);

          hence ((f /^ n) . i) = (f . (n + i)) by A1, RFINSEQ:def 1;

        end;

          suppose n > ( len f);

          then (f /^ n) = {} by RFINSEQ:def 1;

          hence ((f /^ n) . i) = (f . (n + i)) by A1;

        end;

      end;

      assume

       B1: i in ( dom (f /^ n));

      then

       B2: (n + i) in ( dom f) by Th26;

      ((f /^ n) . i) = (f . (n + i)) by AA, B1;

      

      then ((f /^ n) /. i) = (f . (n + i)) by B1, PARTFUN1:def 6

      .= (f /. (n + i)) by PARTFUN1:def 6, B2;

      hence thesis;

    end;

    theorem :: FINSEQ_5:28

    

     Th28: for f be FinSequence holds (f /^ 0 ) = f

    proof

      let f be FinSequence;

      

       A1: 0 <= ( len f);

       A2:

      now

        let i be Nat;

        assume 1 <= i & i <= ( len (f /^ 0 ));

        then i in ( dom (f /^ 0 )) by FINSEQ_3: 25;

        

        hence ((f /^ 0 ) . i) = (f . (i + 0 )) by A1, RFINSEQ:def 1

        .= (f . i);

      end;

      ( len (f /^ 0 )) = (( len f) - 0 ) by RFINSEQ:def 1

      .= ( len f);

      hence thesis by A2;

    end;

    registration

      let f be FinSequence;

      reduce (f /^ 0 ) to f;

      reducibility by Th28;

    end

    reserve D for non empty set,

p for Element of D,

f,g for FinSequence of D;

    theorem :: FINSEQ_5:29

    

     Th29: f is non empty implies f = ( <*(f /. 1)*> ^ (f /^ 1))

    proof

      assume

       A1: f is non empty;

      then

       A2: 1 in ( dom f) by Th6;

      (f | 1) = <*(f . 1)*> by A1, Th20

      .= <*(f /. 1)*> by A2, PARTFUN1:def 6;

      hence thesis by RFINSEQ: 8;

    end;

    theorem :: FINSEQ_5:30

    for f be FinSequence st (i + 1) = ( len f) holds (f /^ i) = <*(f . ( len f))*>

    proof

      let f be FinSequence;

      assume

       A1: (i + 1) = ( len f);

      then i <= ( len f) by NAT_1: 11;

      

      then

       A2: ( len (f /^ i)) = (( len f) - i) by RFINSEQ:def 1

      .= 1 by A1;

      then

       A3: 1 in ( dom (f /^ i)) by FINSEQ_3: 25;

      

      thus (f /^ i) = <*((f /^ i) . 1)*> by A2, Th14

      .= <*(f . ( len f))*> by A1, A3, Th27;

    end;

    theorem :: FINSEQ_5:31

    

     Th31: (j + 1) = i & i in ( dom f) implies ( <*(f /. i)*> ^ (f /^ i)) = (f /^ j)

    proof

      assume that

       A1: (j + 1) = i and

       A2: i in ( dom f);

      set g = ( <*(f /. i)*> ^ (f /^ i));

      

       A3: i <= ( len f) by A2, FINSEQ_3: 25;

      j <= i by A1, NAT_1: 11;

      then

       A4: j <= ( len f) by A3, XXREAL_0: 2;

      

       A5: ( len g) = (( len (f /^ i)) + 1) by Th8;

      

      then

       A6: ( len g) = ((( len f) - i) + 1) by A3, RFINSEQ:def 1

      .= (( len f) - j) by A1

      .= ( len (f /^ j)) by A4, RFINSEQ:def 1;

      now

        let k be Nat;

        assume that

         A7: 1 <= k and

         A8: k <= ( len g);

        

         A9: k in ( dom (f /^ j)) by A6, A7, A8, FINSEQ_3: 25;

        per cases ;

          suppose

           A10: k = 1;

          

          hence (g . k) = (f /. i) by FINSEQ_1: 41

          .= (f . i) by A2, PARTFUN1:def 6

          .= ((f /^ j) . k) by A1, A4, A9, A10, RFINSEQ:def 1;

        end;

          suppose k <> 1;

          then

           A11: 1 < k by A7, XXREAL_0: 1;

          reconsider k9 = (k - 1) as Element of NAT by A7, INT_1: 5;

          

           A12: k9 <= (( len g) - 1) by A8, XREAL_1: 9;

          (k9 + 1) = k;

          then 1 <= k9 by A11, NAT_1: 13;

          then

           A13: k9 in ( dom (f /^ i)) by A5, A12, FINSEQ_3: 25;

          ( len <*(f /. i)*>) = 1 by FINSEQ_1: 39;

          

          hence (g . k) = ((f /^ i) . k9) by A8, A11, FINSEQ_1: 24

          .= (f . (k9 + i)) by A3, A13, RFINSEQ:def 1

          .= (f . (k + j)) by A1

          .= ((f /^ j) . k) by A4, A9, RFINSEQ:def 1;

        end;

      end;

      hence thesis by A6;

    end;

    theorem :: FINSEQ_5:32

    

     Th32: for f be FinSequence st ( len f) <= i holds (f /^ i) is empty

    proof

      let f be FinSequence;

      assume

       A1: ( len f) <= i;

      per cases ;

        suppose ( len f) = i;

        

        then ( len (f /^ i)) = (( len f) - ( len f)) by RFINSEQ:def 1

        .= 0 ;

        hence thesis;

      end;

        suppose ( len f) <> i;

        then ( len f) < i by A1, XXREAL_0: 1;

        hence thesis by RFINSEQ:def 1;

      end;

    end;

    theorem :: FINSEQ_5:33

    

     Th33: for f be FinSequence holds ( rng (f /^ n)) c= ( rng f)

    proof

      let f be FinSequence;

      let p be object;

      assume p in ( rng (f /^ n));

      then

      consider j be object such that

       A1: j in ( dom (f /^ n)) and

       A2: ((f /^ n) . j) = p by FUNCT_1:def 3;

      reconsider jj = j as Nat by A1;

      (jj + n) in ( dom f) by A1, Th26;

      then (f . (jj + n)) in ( rng f) by FUNCT_1:def 3;

      hence thesis by A1, A2, Th27;

    end;

    

     Lm3: f is one-to-one implies (f /^ i) is one-to-one

    proof

      assume

       A1: f is one-to-one;

      now

        let n,m be Element of NAT such that

         A2: n in ( dom (f /^ i)) and

         A3: m in ( dom (f /^ i)) and

         A4: ((f /^ i) . n) = ((f /^ i) . m);

        

         A5: (i + n) in ( dom f) & (i + m) in ( dom f) by A2, A3, Th26;

        (f . (i + n)) = ((f /^ i) . n) by A2, Th27

        .= (f . (i + m)) by A3, A4, Th27;

        then (i + n) = (i + m) by A1, A5;

        hence n = m;

      end;

      hence thesis;

    end;

    registration

      let i, D;

      let f be one-to-one FinSequence of D;

      cluster (f /^ i) -> one-to-one;

      coherence by Lm3;

    end

    theorem :: FINSEQ_5:34

    

     Th34: for f be FinSequence st f is one-to-one holds ( rng (f | n)) misses ( rng (f /^ n))

    proof

      let f be FinSequence;

      assume

       A1: f is one-to-one;

      

       A2: ( dom (f | n)) c= ( dom f) by Th18;

      assume ( rng (f | n)) meets ( rng (f /^ n));

      then

      consider x be object such that

       A3: x in ( rng (f | n)) and

       A4: x in ( rng (f /^ n)) by XBOOLE_0: 3;

      consider i be object such that

       A5: i in ( dom (f | n)) and

       A6: ((f | n) . i) = x by A3, FUNCT_1:def 3;

      consider j be object such that

       A7: j in ( dom (f /^ n)) and

       A8: ((f /^ n) . j) = x by A4, FUNCT_1:def 3;

      reconsider ii = i, jj = j as Nat by A7, A5;

      

       A9: (jj + n) in ( dom f) by A7, Th26;

       A10:

      now

        ii <= ( len (f | n)) & ( len (f | n)) <= n by A5, Th17, FINSEQ_3: 25;

        then

         A11: ii <= n by XXREAL_0: 2;

        assume

         A12: ii = (jj + n);

        then n <= ii by NAT_1: 11;

        then i = n by A11, XXREAL_0: 1;

        then j = 0 by A12;

        hence contradiction by A7, FINSEQ_3: 25;

      end;

      (f . (jj + n)) = ((f /^ n) . j) by A7, Th27

      .= (f . i) by A5, FUNCT_1: 47, A6, A8;

      hence contradiction by A1, A5, A2, A9, A10;

    end;

    theorem :: FINSEQ_5:35

    p in ( rng f) implies (f |-- p) = (f /^ (p .. f))

    proof

      assume

       A1: p in ( rng f);

      then

       A2: ( len (f |-- p)) = (( len f) - (p .. f)) by FINSEQ_4:def 6;

      

       A3: (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

      then

       A4: ( len (f /^ (p .. f))) = (( len f) - (p .. f)) by RFINSEQ:def 1;

      

       A5: ( Seg ( len (f |-- p))) = ( dom (f |-- p)) & ( Seg ( len (f /^ (p .. f)))) = ( dom (f /^ (p .. f))) by FINSEQ_1:def 3;

      now

        let i be Nat;

        assume

         A6: i in ( dom (f |-- p));

        

        hence ((f |-- p) . i) = (f . (i + (p .. f))) by A1, FINSEQ_4:def 6

        .= ((f /^ (p .. f)) . i) by A2, A3, A4, A5, A6, RFINSEQ:def 1;

      end;

      hence thesis by A2, A4, FINSEQ_2: 9;

    end;

    theorem :: FINSEQ_5:36

    

     Th36: for f,g be FinSequence holds ((f ^ g) /^ (( len f) + i)) = (g /^ i)

    proof

      let f,g be FinSequence;

      

       A1: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;

      per cases ;

        suppose

         A2: i <= ( len g);

        then (( len f) + i) <= (( len f) + ( len g)) by XREAL_1: 6;

        

        then

         A3: ( len ((f ^ g) /^ (( len f) + i))) = ((( len g) + ( len f)) - (( len f) + i)) by A1, RFINSEQ:def 1

        .= (( len g) - i)

        .= ( len (g /^ i)) by A2, RFINSEQ:def 1;

        now

          let k;

          assume

           A4: 1 <= k & k <= ( len (g /^ i));

          then

           A5: k in ( dom (g /^ i)) by FINSEQ_3: 25;

          then

           A6: (i + k) in ( dom g) by Th26;

          k in ( dom ((f ^ g) /^ (( len f) + i))) by A3, A4, FINSEQ_3: 25;

          

          hence (((f ^ g) /^ (( len f) + i)) . k) = ((f ^ g) . ((( len f) + i) + k)) by Th27

          .= ((f ^ g) . (( len f) + (i + k)))

          .= (g . (i + k)) by A6, FINSEQ_1:def 7

          .= ((g /^ i) . k) by A5, Th27;

        end;

        hence thesis by A3;

      end;

        suppose

         A7: i > ( len g);

        then (( len f) + i) > ( len (f ^ g)) by A1, XREAL_1: 6;

        

        hence ((f ^ g) /^ (( len f) + i)) = {} by RFINSEQ:def 1

        .= (g /^ i) by A7, RFINSEQ:def 1;

      end;

    end;

    theorem :: FINSEQ_5:37

    

     Th37: for f,g be FinSequence holds ((f ^ g) /^ ( len f)) = g

    proof

      let f,g be FinSequence;

      

      thus ((f ^ g) /^ ( len f)) = ((f ^ g) /^ (( len f) + 0 ))

      .= (g /^ 0 ) by Th36

      .= g;

    end;

    registration

      let f,g be FinSequence;

      reduce ((f ^ g) /^ ( len f)) to g;

      reducibility by Th37;

    end

    theorem :: FINSEQ_5:38

    

     Th38: p in ( rng f) implies (f /. (p .. f)) = p

    proof

      assume p in ( rng f);

      then (p .. f) in ( dom f) & (f . (p .. f)) = p by FINSEQ_4: 19, FINSEQ_4: 20;

      hence thesis by PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_5:39

    

     Th39: i in ( dom f) implies ((f /. i) .. f) <= i

    proof

      set p = (f /. i);

      

       A1: (p .. f) = (( Sgm (f " {p})) . 1) by FINSEQ_4:def 4;

      (f " {p}) c= ( dom f) by RELAT_1: 132;

      then

       A2: (f " {p}) c= ( Seg ( len f)) by FINSEQ_1:def 3;

      assume

       A3: i in ( dom f);

      then (f /. i) = (f . i) by PARTFUN1:def 6;

      then (f . i) in {p} by TARSKI:def 1;

      then i in (f " {p}) by A3, FUNCT_1:def 7;

      then i in ( rng ( Sgm (f " {p}))) by A2, FINSEQ_1:def 13;

      then

      consider l be object such that

       A4: l in ( dom ( Sgm (f " {p}))) and

       A5: (( Sgm (f " {p})) . l) = i by FUNCT_1:def 3;

      reconsider l as Element of NAT by A4;

      1 <= l & l <= ( len ( Sgm (f " {p}))) by A4, FINSEQ_3: 25;

      hence thesis by A1, A2, A5, FINSEQ_3: 41;

    end;

    theorem :: FINSEQ_5:40

    p in ( rng (f | i)) implies (p .. (f | i)) = (p .. f)

    proof

      

       A1: ( dom (f | i)) c= ( dom f) by Th18;

      assume

       A2: p in ( rng (f | i));

      then

       A3: (p .. (f | i)) in ( dom (f | i)) by FINSEQ_4: 20;

      

      then (f /. (p .. (f | i))) = ((f | i) /. (p .. (f | i))) by FINSEQ_4: 70

      .= p by A2, Th38;

      then

       A4: (p .. f) <= (p .. (f | i)) by A3, A1, Th39;

      (p .. (f | i)) <= ( len (f | i)) by A2, FINSEQ_4: 21;

      then

       A5: (p .. f) <= ( len (f | i)) by A4, XXREAL_0: 2;

      

       A6: ( rng (f | i)) c= ( rng f) by Th19;

      then 1 <= (p .. f) by A2, FINSEQ_4: 21;

      then

       A7: (p .. f) in ( dom (f | i)) by A5, FINSEQ_3: 25;

      

      then ((f | i) /. (p .. f)) = (f /. (p .. f)) by FINSEQ_4: 70

      .= p by A2, A6, Th38;

      then (p .. (f | i)) <= (p .. f) by A7, Th39;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: FINSEQ_5:41

    i in ( dom f) & f is one-to-one implies ((f /. i) .. f) = i

    proof

      assume

       A1: i in ( dom f);

      assume f is one-to-one;

      then ((f . i) .. f) = i by A1, Th11;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    definition

      let D, f;

      let p be set;

      :: FINSEQ_5:def1

      func f -: p -> FinSequence of D equals (f | (p .. f));

      correctness ;

    end

    theorem :: FINSEQ_5:42

    

     Th42: p in ( rng f) implies ( len (f -: p)) = (p .. f)

    proof

      assume p in ( rng f);

      then (p .. f) in ( dom f) by FINSEQ_4: 20;

      then (p .. f) <= ( len f) by FINSEQ_3: 25;

      hence thesis by FINSEQ_1: 59;

    end;

    theorem :: FINSEQ_5:43

    

     Th43: p in ( rng f) & i in ( Seg (p .. f)) implies ((f -: p) /. i) = (f /. i)

    proof

      assume that

       A1: p in ( rng f) and

       A2: i in ( Seg (p .. f));

      (p .. f) in ( dom f) by A1, FINSEQ_4: 20;

      hence thesis by A2, FINSEQ_4: 71;

    end;

    theorem :: FINSEQ_5:44

    p in ( rng f) implies ((f -: p) /. 1) = (f /. 1)

    proof

      assume

       A1: p in ( rng f);

      then 1 <= (p .. f) by FINSEQ_4: 21;

      then 1 in ( Seg (p .. f));

      hence thesis by A1, Th43;

    end;

    theorem :: FINSEQ_5:45

    p in ( rng f) implies ((f -: p) /. (p .. f)) = p

    proof

      assume

       A1: p in ( rng f);

      then

       A2: (p .. f) in ( dom f) by FINSEQ_4: 20;

      1 <= (p .. f) by A1, FINSEQ_4: 21;

      then (p .. f) in ( Seg (p .. f));

      

      hence ((f -: p) /. (p .. f)) = (f /. (p .. f)) by A1, Th43

      .= (f . (p .. f)) by A2, PARTFUN1:def 6

      .= p by A1, FINSEQ_4: 19;

    end;

    theorem :: FINSEQ_5:46

    for x be set st x in ( rng f) & p in ( rng f) & (x .. f) <= (p .. f) holds x in ( rng (f -: p))

    proof

      let x be set;

      assume that

       A1: x in ( rng f) and

       A2: p in ( rng f) and

       A3: (x .. f) <= (p .. f);

      set g = (f -: p), i = (x .. f);

      1 <= i by A1, FINSEQ_4: 21;

      then

       A4: i in ( Seg (p .. f)) by A3;

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

      then

       A5: i in ( dom g) by A2, A4, Th42;

      then (g . i) in ( rng g) by FUNCT_1:def 3;

      then (g /. i) in ( rng g) by A5, PARTFUN1:def 6;

      then

       A6: (f /. i) in ( rng g) by A2, A4, Th43;

      i in ( dom f) by A1, FINSEQ_4: 20;

      then (f . i) in ( rng g) by A6, PARTFUN1:def 6;

      hence thesis by A1, FINSEQ_4: 19;

    end;

    theorem :: FINSEQ_5:47

    p in ( rng f) implies (f -: p) is non empty

    proof

      assume

       A1: p in ( rng f);

      then 1 <= (p .. f) by FINSEQ_4: 21;

      then 1 <= ( len (f -: p)) by A1, Th42;

      hence thesis;

    end;

    theorem :: FINSEQ_5:48

    ( rng (f -: p)) c= ( rng f) by Th19;

    registration

      let D, p;

      let f be one-to-one FinSequence of D;

      cluster (f -: p) -> one-to-one;

      coherence ;

    end

    definition

      let D, f, p;

      :: FINSEQ_5:def2

      func f :- p -> FinSequence of D equals ( <*p*> ^ (f /^ (p .. f)));

      coherence ;

    end

    theorem :: FINSEQ_5:49

    

     Th49: p in ( rng f) implies ex i be Element of NAT st (i + 1) = (p .. f) & (f :- p) = (f /^ i)

    proof

      assume

       A1: p in ( rng f);

      then

      reconsider i = ((p .. f) - 1) as Element of NAT by FINSEQ_4: 21, INT_1: 5;

      

       A2: (p .. f) in ( dom f) by A1, FINSEQ_4: 20;

      take i;

      thus

       A3: (i + 1) = (p .. f);

      

      thus (f :- p) = ( <*(f /. (p .. f))*> ^ (f /^ (p .. f))) by A1, Th38

      .= (f /^ i) by A3, A2, Th31;

    end;

    theorem :: FINSEQ_5:50

    

     Th50: p in ( rng f) implies ( len (f :- p)) = ((( len f) - (p .. f)) + 1)

    proof

      assume

       A1: p in ( rng f);

      then

       A2: (p .. f) <= ( len f) by FINSEQ_4: 21;

      consider i be Element of NAT such that

       A3: (i + 1) = (p .. f) and

       A4: (f :- p) = (f /^ i) by A1, Th49;

      i <= (p .. f) by A3, NAT_1: 11;

      then i <= ( len f) by A2, XXREAL_0: 2;

      

      hence ( len (f :- p)) = (( len f) - i) by A4, RFINSEQ:def 1

      .= ((( len f) - (p .. f)) + 1) by A3;

    end;

    theorem :: FINSEQ_5:51

    

     Th51: p in ( rng f) & (j + 1) in ( dom (f :- p)) implies (j + (p .. f)) in ( dom f)

    proof

      assume that

       A1: p in ( rng f) and

       A2: (j + 1) in ( dom (f :- p));

      (j + 1) <= ( len (f :- p)) by A2, FINSEQ_3: 25;

      then (j + 1) <= ((( len f) - (p .. f)) + 1) by A1, Th50;

      then j <= (( len f) - (p .. f)) by XREAL_1: 6;

      then

       A3: (j + (p .. f)) <= ( len f) by XREAL_1: 19;

      

       A4: (p .. f) <= (j + (p .. f)) by NAT_1: 11;

      1 <= (p .. f) by A1, FINSEQ_4: 21;

      then 1 <= (j + (p .. f)) by A4, XXREAL_0: 2;

      hence thesis by A3, FINSEQ_3: 25;

    end;

    registration

      let D, p, f;

      cluster (f :- p) -> non empty;

      coherence ;

    end

    theorem :: FINSEQ_5:52

    

     Th52: p in ( rng f) & (j + 1) in ( dom (f :- p)) implies ((f :- p) /. (j + 1)) = (f /. (j + (p .. f)))

    proof

      assume that

       A1: p in ( rng f) and

       A2: (j + 1) in ( dom (f :- p));

      

       A3: (j + (p .. f)) in ( dom f) by A1, A2, Th51;

      set i = (j + 1);

      

       A4: (p .. f) <= ( len f) by A1, FINSEQ_4: 21;

      consider k be Element of NAT such that

       A5: (k + 1) = (p .. f) and

       A6: (f :- p) = (f /^ k) by A1, Th49;

      k <= (p .. f) by A5, NAT_1: 11;

      then

       A7: k <= ( len f) by A4, XXREAL_0: 2;

      

      thus ((f :- p) /. i) = ((f :- p) . i) by A2, PARTFUN1:def 6

      .= (f . (i + k)) by A2, A6, A7, RFINSEQ:def 1

      .= (f /. (j + (p .. f))) by A5, A3, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_5:53

    ((f :- p) /. 1) = p by Th15;

    theorem :: FINSEQ_5:54

    p in ( rng f) implies ((f :- p) /. ( len (f :- p))) = (f /. ( len f))

    proof

      

       A1: ( len (f :- p)) in ( dom (f :- p)) by Th6;

      assume

       A2: p in ( rng f);

      then (p .. f) <= ( len f) by FINSEQ_4: 21;

      then

      reconsider j = (( len f) - (p .. f)) as Element of NAT by INT_1: 5;

      ( len (f :- p)) = (j + 1) by A2, Th50;

      

      hence ((f :- p) /. ( len (f :- p))) = (f /. (j + (p .. f))) by A2, A1, Th52

      .= (f /. ( len f));

    end;

    theorem :: FINSEQ_5:55

    p in ( rng f) implies ( rng (f :- p)) c= ( rng f)

    proof

      assume p in ( rng f);

      then ex i be Element of NAT st (i + 1) = (p .. f) & (f :- p) = (f /^ i) by Th49;

      hence thesis by Th33;

    end;

    theorem :: FINSEQ_5:56

    p in ( rng f) & f is one-to-one implies (f :- p) is one-to-one

    proof

      assume p in ( rng f);

      then ex i be Element of NAT st (i + 1) = (p .. f) & (f :- p) = (f /^ i) by Th49;

      hence thesis;

    end;

    reserve i for Nat;

    definition

      let f be FinSequence;

      :: FINSEQ_5:def3

      func Rev f -> FinSequence means

      : Def3: ( len it ) = ( len f) & for i st i in ( dom it ) holds (it . i) = (f . ((( len f) - i) + 1));

      existence

      proof

        deffunc F( Nat) = (f . ((( len f) - $1) + 1));

        ex p be FinSequence st ( len p) = ( len f) & for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

        hence thesis;

      end;

      uniqueness

      proof

        

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

        let f1,f2 be FinSequence such that

         A2: ( len f1) = ( len f) and

         A3: for i st i in ( dom f1) holds (f1 . i) = (f . ((( len f) - i) + 1)) and

         A4: ( len f2) = ( len f) and

         A5: for i st i in ( dom f2) holds (f2 . i) = (f . ((( len f) - i) + 1));

        

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

        

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

        now

          let i be Nat;

          assume

           A8: i in ( dom f);

          then (f1 . i) = (f . ((( len f) - i) + 1)) by A2, A3, A6, A1;

          hence (f1 . i) = (f2 . i) by A4, A5, A7, A1, A8;

        end;

        hence thesis by A2, A4, A6, A1, FINSEQ_2: 9;

      end;

      involutiveness

      proof

        let g,f be FinSequence;

        assume that

         A9: ( len g) = ( len f) and

         A10: for i st i in ( dom g) holds (g . i) = (f . ((( len f) - i) + 1));

        thus ( len f) = ( len g) by A9;

        let i;

        assume

         A11: i in ( dom f);

        then i in ( dom g) by A9, FINSEQ_3: 29;

        then i <= ( len g) by FINSEQ_3: 25;

        then

        reconsider j = (( len g) - i) as Element of NAT by INT_1: 5;

        i >= 1 by A11, FINSEQ_3: 25;

        then (j + i) >= (j + 1) by XREAL_1: 6;

        then j < ( len g) by NAT_1: 13;

        then 1 <= (j + 1) & (j + 1) <= ( len g) by NAT_1: 11, NAT_1: 13;

        then

         A12: (j + 1) in ( dom g) by FINSEQ_3: 25;

        

        thus (f . i) = (f . ((( len f) - (j + 1)) + 1)) by A9

        .= (g . ((( len g) - i) + 1)) by A10, A12;

      end;

    end

    theorem :: FINSEQ_5:57

    

     Th57: for f be FinSequence holds ( dom f) = ( dom ( Rev f)) & ( rng f) = ( rng ( Rev f))

    proof

      let f be FinSequence;

      

      thus

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

      .= ( Seg ( len ( Rev f))) by Def3

      .= ( dom ( Rev f)) by FINSEQ_1:def 3;

      

       A2: ( len f) = ( len ( Rev f)) by Def3;

      hereby

        let x be object;

        assume x in ( rng f);

        then

        consider i be Nat such that

         A3: i in ( dom f) and

         A4: (f . i) = x by FINSEQ_2: 10;

        i <= ( len f) by A3, FINSEQ_3: 25;

        then

        reconsider j = ((( len f) - i) + 1) as Element of NAT by Th1;

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

        then j in ( Seg ( len ( Rev f))) by A2, A3, Th2;

        then

         A5: j in ( dom ( Rev f)) by FINSEQ_1:def 3;

        then (( Rev f) . j) = (f . ((( len f) - j) + 1)) by Def3;

        hence x in ( rng ( Rev f)) by A4, A5, FUNCT_1:def 3;

      end;

      let x be object;

      assume x in ( rng ( Rev f));

      then

      consider i be Nat such that

       A6: i in ( dom ( Rev f)) and

       A7: (( Rev f) . i) = x by FINSEQ_2: 10;

      i <= ( len f) by A2, A6, FINSEQ_3: 25;

      then

      reconsider j = ((( len f) - i) + 1) as Element of NAT by Th1;

      i in ( Seg ( len ( Rev f))) by A6, FINSEQ_1:def 3;

      then j in ( Seg ( len ( Rev f))) by A2, Th2;

      then

       A8: j in ( dom ( Rev f)) by FINSEQ_1:def 3;

      (( Rev f) . i) = (f . ((( len f) - i) + 1)) by A6, Def3;

      hence thesis by A1, A7, A8, FUNCT_1:def 3;

    end;

    theorem :: FINSEQ_5:58

    

     Th58: for f be FinSequence st i in ( dom f) holds (( Rev f) . i) = (f . ((( len f) - i) + 1))

    proof

      let f be FinSequence;

      ( dom f) = ( dom ( Rev f)) by Th57;

      hence thesis by Def3;

    end;

    theorem :: FINSEQ_5:59

    

     Th59: for f be FinSequence, i,j be Nat st i in ( dom f) & (i + j) = (( len f) + 1) holds j in ( dom ( Rev f))

    proof

      let f be FinSequence, i,j be Nat such that

       A1: i in ( dom f) and

       A2: (i + j) = (( len f) + 1);

      

       A3: ( dom f) = ( Seg ( len f)) & ( dom f) = ( dom ( Rev f)) by Th57, FINSEQ_1:def 3;

      j = ((( len f) - i) + 1) by A2;

      hence thesis by A1, A3, Th2;

    end;

    registration

      let f be empty FinSequence;

      cluster ( Rev f) -> empty;

      coherence

      proof

        ( len {} ) = 0 ;

        then ( len ( Rev {} )) = 0 by Def3;

        hence thesis;

      end;

    end

    theorem :: FINSEQ_5:60

    for x be object holds ( Rev <*x*>) = <*x*>

    proof

      let x be object;

      set f = <*x*>;

      

       A1: ( len f) = 1 by FINSEQ_1: 39;

      now

        let i;

        assume i in ( dom f);

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

        then i = 1 by A1, FINSEQ_1: 2, TARSKI:def 1;

        hence (f . i) = (f . ((( len f) - i) + 1)) by FINSEQ_1: 39;

      end;

      hence thesis by Def3;

    end;

    theorem :: FINSEQ_5:61

    for x1,x2 be object holds ( Rev <*x1, x2*>) = <*x2, x1*>

    proof

      let x1,x2 be object;

      set f = <*x1, x2*>, g = <*x2, x1*>;

      

       A1: ( len f) = 2 by FINSEQ_1: 44;

      

       A2: ( len g) = 2 by FINSEQ_1: 44;

      now

        let i;

        assume i in ( dom g);

        then

         A3: i in ( Seg ( len f)) by A1, A2, FINSEQ_1:def 3;

        per cases by A1, A3, FINSEQ_1: 2, TARSKI:def 2;

          suppose

           A4: i = 1;

          

          hence (g . i) = x2 by FINSEQ_1: 44

          .= (f . ((( len f) - i) + 1)) by A1, A4, FINSEQ_1: 44;

        end;

          suppose

           A5: i = 2;

          

          hence (g . i) = x1 by FINSEQ_1: 44

          .= (f . ((( len f) - i) + 1)) by A1, A5, FINSEQ_1: 44;

        end;

      end;

      hence thesis by A1, A2, Def3;

    end;

    theorem :: FINSEQ_5:62

    

     Th62: for f be FinSequence holds (f . 1) = (( Rev f) . ( len f)) & (f . ( len f)) = (( Rev f) . 1)

    proof

      let f be FinSequence;

      per cases ;

        suppose

         A1: f is empty;

        

        hence (f . 1) = {}

        .= (( Rev f) . ( len f)) by A1;

        

        thus (f . ( len f)) = {} by A1

        .= (( Rev f) . 1) by A1;

      end;

        suppose

         A3: f is non empty;

        then ( len f) in ( Seg ( len f)) by FINSEQ_1: 3;

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

        

        hence (( Rev f) . ( len f)) = (f . ((( len f) - ( len f)) + 1)) by Th58

        .= (f . 1);

        ( len f) >= 1 by A3, NAT_1: 14;

        then 1 in ( dom f) by FINSEQ_3: 25;

        

        hence (( Rev f) . 1) = (f . ((( len f) - 1) + 1)) by Th58

        .= (f . ( len f));

      end;

    end;

    registration

      let f be one-to-one FinSequence;

      cluster ( Rev f) -> one-to-one;

      coherence

      proof

        set g = ( Rev f);

        let x1,x2 be object such that

         A1: x1 in ( dom g) and

         A2: x2 in ( dom g) and

         A3: (g . x1) = (g . x2);

        reconsider i1 = x1, i2 = x2 as Element of NAT by A1, A2;

        

         A4: ( len g) = ( len f) by Def3;

        then i1 <= ( len f) & i2 <= ( len f) by A1, A2, FINSEQ_3: 25;

        then

        reconsider i19 = ((( len f) - i1) + 1), i29 = ((( len f) - i2) + 1) as Element of NAT by Th1;

        

         A5: (f . i19) = (g . x1) by A1, Def3

        .= (f . i29) by A2, A3, Def3;

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

        then i19 in ( dom f) & i29 in ( dom f) by A1, A2, A4, Th2;

        then i19 = i29 by A5, FUNCT_1:def 4;

        hence thesis;

      end;

    end

    theorem :: FINSEQ_5:63

    

     Th63: for f be FinSequence, x be object holds ( Rev (f ^ <*x*>)) = ( <*x*> ^ ( Rev f))

    proof

      let f be FinSequence, x be object;

      set n = (( len f) + 1), g = <*x*>;

      

       A1: ( len (g ^ ( Rev f))) = (( len g) + ( len ( Rev f))) by FINSEQ_1: 22

      .= (1 + ( len ( Rev f))) by FINSEQ_1: 39

      .= n by Def3;

      

       A2: ( len (f ^ g)) = n by FINSEQ_2: 16;

      then

       A3: ( len ( Rev (f ^ g))) = n by Def3;

      now

        let i be Nat;

        

         A4: ( len g) = 1 by FINSEQ_1: 40;

        assume

         A5: i in ( dom ( Rev (f ^ g)));

        then

         A6: 1 <= i by FINSEQ_3: 25;

        

         A7: i <= n by A3, A5, FINSEQ_3: 25;

        per cases by A6, XXREAL_0: 1;

          suppose

           A8: i = 1;

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

          then

           A9: 1 in ( dom g) by A4;

          

          thus (( Rev (f ^ g)) . i) = ((f ^ g) . ((n - 1) + 1)) by A2, A5, A8, Def3

          .= x by FINSEQ_1: 42

          .= (g . 1) by FINSEQ_1: 40

          .= ((g ^ ( Rev f)) . i) by A8, A9, FINSEQ_1:def 7;

        end;

          suppose

           A10: i > 1;

          then

          reconsider j = (i - 1) as Element of NAT by NAT_1: 20;

          consider l be Nat such that

           A11: i = (l + 1) by A10, NAT_1: 6;

          reconsider k = ((n - i) + 1) as Element of NAT by A7, Th1;

          n < (( len f) + i) by A10, XREAL_1: 8;

          then (n - i) < ((( len f) + i) - i) by XREAL_1: 9;

          then k < (( len f) + 1) by XREAL_1: 6;

          then

           A12: k <= ( len f) by NAT_1: 13;

          (i - i) <= (n - i) by A7, XREAL_1: 9;

          then ( 0 + 1) <= k by XREAL_1: 6;

          then

           A13: k in ( dom f) by A12, FINSEQ_3: 25;

          l <> 0 by A10, A11;

          then

           A14: 1 <= j by A11, NAT_1: 14;

          j <= (n - 1) by A7, XREAL_1: 9;

          then

           A15: j in ( dom f) by A14, FINSEQ_3: 25;

          

          thus (( Rev (f ^ g)) . i) = ((f ^ g) . ((n - i) + 1)) by A2, A5, Def3

          .= (f . ((( len f) - j) + 1)) by A13, FINSEQ_1:def 7

          .= (( Rev f) . j) by A15, Th58

          .= ((g ^ ( Rev f)) . i) by A1, A7, A4, A10, FINSEQ_1: 24;

        end;

      end;

      hence thesis by A1, A3, FINSEQ_2: 9;

    end;

    theorem :: FINSEQ_5:64

    for f,g be FinSequence holds ( Rev (f ^ g)) = (( Rev g) ^ ( Rev f))

    proof

      let f be FinSequence;

      defpred P[ FinSequence] means ( Rev (f ^ $1)) = (( Rev $1) ^ ( Rev f));

      

       A1: P[ {} ]

      proof

        set g = {} ;

        

        thus ( Rev (f ^ g)) = ( Rev f) by FINSEQ_1: 34

        .= (( Rev g) ^ ( Rev f)) by FINSEQ_1: 34;

      end;

      

       A2: for g be FinSequence, x be object st P[g] holds P[(g ^ <*x*>)]

      proof

        let g be FinSequence, x be object such that

         A3: P[g];

        

        thus ( Rev (f ^ (g ^ <*x*>))) = ( Rev ((f ^ g) ^ <*x*>)) by FINSEQ_1: 32

        .= ( <*x*> ^ (( Rev g) ^ ( Rev f))) by A3, Th63

        .= (( <*x*> ^ ( Rev g)) ^ ( Rev f)) by FINSEQ_1: 32

        .= (( Rev (g ^ <*x*>)) ^ ( Rev f)) by Th63;

      end;

      thus for g be FinSequence holds P[g] from FINSEQ_1:sch 3( A1, A2);

    end;

    definition

      let D be set, f be FinSequence of D;

      :: original: Rev

      redefine

      func Rev f -> FinSequence of D ;

      coherence

      proof

        set n = ( len f);

        

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

        now

          let i be Nat;

          set j = ((n - i) + 1);

          assume i in ( dom ( Rev f));

          then i in ( Seg ( len ( Rev f))) by FINSEQ_1:def 3;

          then

           A2: i in ( Seg n) by Def3;

          then j in ( Seg n) by Th2;

          then (f . j) in D by A1, FINSEQ_2: 11;

          hence (( Rev f) . i) in D by A1, A2, Th58;

        end;

        hence thesis by FINSEQ_2: 12;

      end;

    end

    theorem :: FINSEQ_5:65

    f is non empty implies (f /. 1) = (( Rev f) /. ( len f)) & (f /. ( len f)) = (( Rev f) /. 1)

    proof

      

       A1: ( dom f) = ( dom ( Rev f)) by Th57;

      assume

       A2: f is non empty;

      then

       A3: ( len f) in ( dom f) by Th6;

      1 in ( dom f) by A2, Th6;

      

      hence (f /. 1) = (f . 1) by PARTFUN1:def 6

      .= (( Rev f) . ( len f)) by Th62

      .= (( Rev f) /. ( len f)) by A3, A1, PARTFUN1:def 6;

      

      thus (f /. ( len f)) = (f . ( len f)) by A3, PARTFUN1:def 6

      .= (( Rev f) . 1) by Th62

      .= (( Rev f) /. 1) by A2, A1, Th6, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_5:66

    i in ( dom f) & (i + j) = (( len f) + 1) implies (f /. i) = (( Rev f) /. j)

    proof

      assume that

       A1: i in ( dom f) and

       A2: (i + j) = (( len f) + 1);

      

       A3: j in ( dom ( Rev f)) by A1, A2, Th59;

      

       A4: i = ((( len f) - j) + 1) by A2;

      

      thus (f /. i) = (f . i) by A1, PARTFUN1:def 6

      .= (( Rev f) . j) by A4, A3, Def3

      .= (( Rev f) /. j) by A3, PARTFUN1:def 6;

    end;

    definition

      let D, f, p;

      let n be Nat;

      :: FINSEQ_5:def4

      func Ins (f,n,p) -> FinSequence of D equals (((f | n) ^ <*p*>) ^ (f /^ n));

      coherence ;

    end

    theorem :: FINSEQ_5:67

    ( Ins (f, 0 ,p)) = ( <*p*> ^ f) by FINSEQ_1: 34;

    theorem :: FINSEQ_5:68

    

     Th68: ( len f) <= n implies ( Ins (f,n,p)) = (f ^ <*p*>)

    proof

      assume

       A1: ( len f) <= n;

      then (f /^ n) is empty by Th32;

      

      hence ( Ins (f,n,p)) = ((f | n) ^ <*p*>) by FINSEQ_1: 34

      .= (f ^ <*p*>) by A1, FINSEQ_1: 58;

    end;

    theorem :: FINSEQ_5:69

    ( len ( Ins (f,n,p))) = (( len f) + 1)

    proof

      per cases ;

        suppose

         A1: n <= ( len f);

        

        thus ( len ( Ins (f,n,p))) = (( len ((f | n) ^ <*p*>)) + ( len (f /^ n))) by FINSEQ_1: 22

        .= (( len ((f | n) ^ <*p*>)) + (( len f) - n)) by A1, RFINSEQ:def 1

        .= ((( len (f | n)) + ( len <*p*>)) + (( len f) - n)) by FINSEQ_1: 22

        .= ((( len (f | n)) + 1) + (( len f) - n)) by FINSEQ_1: 39

        .= ((n + 1) + (( len f) - n)) by A1, FINSEQ_1: 59

        .= (( len f) + 1);

      end;

        suppose ( len f) < n;

        then ( Ins (f,n,p)) = (f ^ <*p*>) by Th68;

        hence thesis by FINSEQ_2: 16;

      end;

    end;

    theorem :: FINSEQ_5:70

    

     Th70: ( rng ( Ins (f,n,p))) = ( {p} \/ ( rng f))

    proof

      

      thus ( rng ( Ins (f,n,p))) = (( rng ((f | n) ^ <*p*>)) \/ ( rng (f /^ n))) by FINSEQ_1: 31

      .= ((( rng (f | n)) \/ ( rng <*p*>)) \/ ( rng (f /^ n))) by FINSEQ_1: 31

      .= ((( rng (f | n)) \/ ( rng (f /^ n))) \/ ( rng <*p*>)) by XBOOLE_1: 4

      .= (( rng ((f | n) ^ (f /^ n))) \/ ( rng <*p*>)) by FINSEQ_1: 31

      .= (( rng <*p*>) \/ ( rng f)) by RFINSEQ: 8

      .= ( {p} \/ ( rng f)) by FINSEQ_1: 38;

    end;

    registration

      let D, f, n, p;

      cluster ( Ins (f,n,p)) -> non empty;

      coherence ;

    end

    theorem :: FINSEQ_5:71

    p in ( rng ( Ins (f,n,p)))

    proof

      p in {p} by TARSKI:def 1;

      then p in ( {p} \/ ( rng f)) by XBOOLE_0:def 3;

      hence thesis by Th70;

    end;

    theorem :: FINSEQ_5:72

    

     Th72: i in ( dom (f | n)) implies (( Ins (f,n,p)) . i) = (f . i)

    proof

      assume

       A1: i in ( dom (f | n));

      

      thus (( Ins (f,n,p)) . i) = (((f | n) ^ ( <*p*> ^ (f /^ n))) . i) by FINSEQ_1: 32

      .= ((f | n) . i) by A1, Lm1

      .= (f . i) by A1, FUNCT_1: 47;

    end;

    theorem :: FINSEQ_5:73

    n <= ( len f) implies (( Ins (f,n,p)) . (n + 1)) = p

    proof

      

       A1: 1 <= (n + 1) by NAT_1: 11;

      assume n <= ( len f);

      then

       A2: ( len (f | n)) = n by FINSEQ_1: 59;

      then ( len ((f | n) ^ <*p*>)) = (n + 1) by FINSEQ_2: 16;

      then (n + 1) in ( dom ((f | n) ^ <*p*>)) by A1, FINSEQ_3: 25;

      

      hence (( Ins (f,n,p)) . (n + 1)) = (((f | n) ^ <*p*>) . (n + 1)) by Lm1

      .= p by A2, FINSEQ_1: 42;

    end;

    theorem :: FINSEQ_5:74

    (n + 1) <= i & i <= ( len f) implies (( Ins (f,n,p)) . (i + 1)) = (f . i)

    proof

      assume that

       A1: (n + 1) <= i and

       A2: i <= ( len f);

      reconsider j = (i - (n + 1)) as Element of NAT by A1, INT_1: 5;

      (n + (j + 1)) <= ( len f) by A2;

      then

       A3: (j + 1) <= (( len f) - n) by XREAL_1: 19;

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

      then

       A4: n <= i by A1, XXREAL_0: 2;

      then ( len (f | n)) = n by A2, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A5: ( len ((f | n) ^ <*p*>)) = (n + 1) by FINSEQ_2: 16;

      n <= ( len f) by A2, A4, XXREAL_0: 2;

      then 1 <= (j + 1) & (j + 1) <= ( len (f /^ n)) by A3, NAT_1: 11, RFINSEQ:def 1;

      then

       A6: (j + 1) in ( dom (f /^ n)) by FINSEQ_3: 25;

      ((n + 1) + (j + 1)) = (i + 1);

      

      hence (( Ins (f,n,p)) . (i + 1)) = ((f /^ n) . (j + 1)) by A5, A6, FINSEQ_1:def 7

      .= (f . (n + (j + 1))) by A6, Th27

      .= (f . i);

    end;

    theorem :: FINSEQ_5:75

    1 <= n & f is non empty implies (( Ins (f,n,p)) . 1) = (f . 1)

    proof

      assume that

       A1: 1 <= n and

       A2: f is non empty;

      

       A3: n <= ( len f) implies ( len (f | n)) = n by FINSEQ_1: 59;

      1 <= ( len f) by A2, NAT_1: 14;

      then 1 <= ( len (f | n)) by A1, A3, FINSEQ_1: 58;

      then 1 in ( dom (f | n)) by FINSEQ_3: 25;

      hence thesis by Th72;

    end;

    theorem :: FINSEQ_5:76

    f is one-to-one & not p in ( rng f) implies ( Ins (f,n,p)) is one-to-one

    proof

      assume that

       A1: f is one-to-one and

       A2: not p in ( rng f);

      now

        let x be object;

        assume

         A3: x in ( rng (f /^ n));

        ( rng (f /^ n)) c= ( rng f) by Th33;

        then x in ( rng f) by A3;

        then not x in {p} by A2, TARSKI:def 1;

        then

         A4: not x in ( rng <*p*>) by FINSEQ_1: 38;

        ( rng (f | n)) misses ( rng (f /^ n)) by A1, Th34;

        then not x in ( rng (f | n)) by A3, XBOOLE_0: 3;

        then not x in (( rng (f | n)) \/ ( rng <*p*>)) by A4, XBOOLE_0:def 3;

        hence not x in ( rng ((f | n) ^ <*p*>)) by FINSEQ_1: 31;

      end;

      then

       A5: ( rng ((f | n) ^ <*p*>)) misses ( rng (f /^ n)) by XBOOLE_0: 3;

      now

        let x be object;

        assume x in ( rng <*p*>);

        then x in {p} by FINSEQ_1: 38;

        then

         A6: not x in ( rng f) by A2, TARSKI:def 1;

        ( rng (f | n)) c= ( rng f) by Th19;

        hence not x in ( rng (f | n)) by A6;

      end;

      then <*p*> is one-to-one & ( rng (f | n)) misses ( rng <*p*>) by FINSEQ_3: 93, XBOOLE_0: 3;

      then ((f | n) ^ <*p*>) is one-to-one by A1, FINSEQ_3: 91;

      hence thesis by A1, A5, FINSEQ_3: 91;

    end;

    begin

    theorem :: FINSEQ_5:77

    for i1,i2 be Nat st i1 <= i2 holds ((f | i1) | i2) = (f | i1) & ((f | i2) | i1) = (f | i1)

    proof

      let i1,i2 be Nat;

      assume

       A1: i1 <= i2;

      ( len (f | i1)) <= i1 by Th17;

      hence ((f | i1) | i2) = (f | i1) by A1, FINSEQ_1: 58, XXREAL_0: 2;

      ( Seg i1) c= ( Seg i2) by A1, FINSEQ_1: 5;

      hence thesis by FUNCT_1: 51;

    end;

    theorem :: FINSEQ_5:78

    for i be Nat holds (( <*> D) | i) = ( <*> D);

    theorem :: FINSEQ_5:79

    ( Rev ( <*> D)) = ( <*> D);

    registration

      cluster non trivial for FinSequence;

      existence

      proof

        take <* 0 , 0 *>;

        thus thesis;

      end;

    end

    theorem :: FINSEQ_5:80

    for f be FinSequence of D, l1,l2 be Nat holds ((f /^ l1) | (l2 -' l1)) = ((f | l2) /^ l1)

    proof

      let f be FinSequence of D, l1,l2 be Nat;

      per cases ;

        suppose

         A1: l1 <= l2;

        per cases ;

          suppose

           A2: l2 <= ( len f);

          then

           A3: (l2 - l1) <= (( len f) - l1) by XREAL_1: 9;

          

           A4: l1 <= ( len (f | l2)) by A1, A2, FINSEQ_1: 59;

          

          then

           A5: ( len ((f | l2) /^ l1)) = (( len (f | l2)) - l1) by RFINSEQ:def 1

          .= (l2 - l1) by A2, FINSEQ_1: 59

          .= (l2 -' l1) by A1, XREAL_1: 233;

          

           A6: l1 <= ( len f) by A1, A2, XXREAL_0: 2;

          then ( len (f /^ l1)) = (( len f) - l1) by RFINSEQ:def 1;

          then

           A7: (l2 -' l1) <= ( len (f /^ l1)) by A1, A3, XREAL_1: 233;

          

           A8: for k be Nat st 1 <= k & k <= ( len ((f | l2) /^ l1)) holds (((f /^ l1) | (l2 -' l1)) . k) = (((f | l2) /^ l1) . k)

          proof

            let k be Nat such that

             A9: 1 <= k and

             A10: k <= ( len ((f | l2) /^ l1));

            

             A11: k in ( dom ((f | l2) /^ l1)) by A9, A10, FINSEQ_3: 25;

            k <= (l2 - l1) by A1, A5, A10, XREAL_1: 233;

            then

             A12: (k + l1) <= ((l2 - l1) + l1) by XREAL_1: 6;

            k <= ( len (f /^ l1)) by A7, A5, A10, XXREAL_0: 2;

            then

             A13: k in ( dom (f /^ l1)) by A9, FINSEQ_3: 25;

            k in ( Seg (l2 -' l1)) by A5, A9, A10;

            

            then (((f /^ l1) | (l2 -' l1)) . k) = ((f /^ l1) . k) by FUNCT_1: 49

            .= (f . (k + l1)) by A6, A13, RFINSEQ:def 1

            .= ((f | l2) . (k + l1)) by A12, FINSEQ_3: 112

            .= (((f | l2) /^ l1) . k) by A4, A11, RFINSEQ:def 1;

            hence thesis;

          end;

          ( len ((f /^ l1) | (l2 -' l1))) = (l2 -' l1) by A7, FINSEQ_1: 59;

          hence thesis by A5, A8;

        end;

          suppose

           A14: l2 > ( len f);

          

           A15: ( len (f /^ l1)) = (( len f) -' l1) by RFINSEQ: 29;

          (f | l2) = f by A14, FINSEQ_1: 58;

          hence thesis by A14, A15, FINSEQ_1: 58, NAT_D: 42;

        end;

      end;

        suppose

         A16: l1 > l2;

        reconsider l19 = l1, l29 = l2 as Element of NAT by ORDINAL1:def 12;

        (l1 - l1) > (l2 - l1) by A16, XREAL_1: 9;

        then (l2 -' l1) = 0 by XREAL_0:def 2;

        then

         A17: ((f /^ l1) | (l2 -' l1)) = {} ;

        per cases ;

          suppose l1 <= ( len f);

          then l19 > ( len (f | l29)) by A16, FINSEQ_1: 59, XXREAL_0: 2;

          hence thesis by A17, Th32;

        end;

          suppose

           A18: l1 > ( len f);

          ( len (f | l29)) <= ( len f) by Th16;

          hence thesis by A17, A18, Th32, XXREAL_0: 2;

        end;

      end;

    end;

    reserve D for set,

f for FinSequence of D;

    theorem :: FINSEQ_5:81

    ( len f) >= 2 implies (f | 2) = <*(f /. 1), (f /. 2)*>

    proof

      set d1 = (f /. 1), d2 = (f /. 2);

      assume

       A1: ( len f) >= 2;

      then

       A2: ( len (f | 2)) = 2 by FINSEQ_1: 59;

      reconsider D as non empty set by A1;

      reconsider f as FinSequence of D;

      2 in ( dom (f | 2)) by A2, FINSEQ_3: 25;

      

      then

       A3: d2 = ((f | 2) /. 2) by FINSEQ_4: 70

      .= ((f | 2) . 2) by A2, FINSEQ_4: 15;

      1 in ( dom (f | 2)) by A2, FINSEQ_3: 25;

      

      then d1 = ((f | 2) /. 1) by FINSEQ_4: 70

      .= ((f | 2) . 1) by A2, FINSEQ_4: 15;

      hence thesis by A2, A3, FINSEQ_1: 44;

    end;

    theorem :: FINSEQ_5:82

    for D be set, f be FinSequence of D st (k + 1) <= ( len f) holds (f | (k + 1)) = ((f | k) ^ <*(f /. (k + 1))*>)

    proof

      let D be set, f be FinSequence of D;

      

       A1: 1 <= (k + 1) by NAT_1: 12;

      assume (k + 1) <= ( len f);

      then

       A2: (k + 1) in ( dom f) by A1, FINSEQ_3: 25;

      

      then (f | ( Seg (k + 1))) = ((f | k) ^ <*(f . (k + 1))*>) by Th10

      .= ((f | k) ^ <*(f /. (k + 1))*>) by A2, PARTFUN1:def 6;

      hence thesis;

    end;

    theorem :: FINSEQ_5:83

    

     Th83: for p be FinSequence holds for i be Nat st i < ( len p) holds (p | (i + 1)) = ((p | i) ^ <*(p . (i + 1))*>)

    proof

      let p be FinSequence;

      let i be Nat;

      assume i < ( len p);

      then

       A1: (i + 1) <= ( len p) by NAT_1: 13;

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

      then (i + 1) in ( dom p) by A1, FINSEQ_3: 25;

      hence thesis by Th10;

    end;

    theorem :: FINSEQ_5:84

    for p be FinSequence holds for n be Nat st 1 <= n & n <= ( len p) holds p = (((p | (n -' 1)) ^ <*(p . n)*>) ^ (p /^ n))

    proof

      let p be FinSequence;

      let n be Nat;

      assume that

       A1: 1 <= n and

       A2: n <= ( len p);

      ( len p) >= ((n -' 1) + 1) by A1, A2, XREAL_1: 235;

      then

       A3: ( len p) > (n -' 1) by NAT_1: 13;

      (p | n) = (p | ((n -' 1) + 1)) by A1, XREAL_1: 235

      .= ((p | (n -' 1)) ^ <*(p . ((n -' 1) + 1))*>) by A3, Th83

      .= ((p | (n -' 1)) ^ <*(p . n)*>) by A1, XREAL_1: 235;

      hence thesis by RFINSEQ: 8;

    end;

    theorem :: FINSEQ_5:85

    

     Th3: for D be non empty set holds for f be non empty FinSequence of D holds (f /^ 1) = ( Del (f,1))

    proof

      let D be non empty set;

      let f be non empty FinSequence of D;

      consider i be Nat such that

       A1: (i + 1) = ( len f) by NAT_1: 6;

      reconsider i as Element of NAT by ORDINAL1:def 12;

      

       A2: 1 <= ( len f) by A1, NAT_1: 11;

      ( len (f /^ 1)) = ( len ( Del (f,1))) & for k be Nat st 1 <= k & k <= ( len (f /^ 1)) holds ((f /^ 1) . k) = (( Del (f,1)) . k)

      proof

        

         A3: ( len (f /^ 1)) = ((i + 1) - 1) by A1, A2, RFINSEQ:def 1

        .= i;

        1 in ( dom f) by Th6;

        hence ( len (f /^ 1)) = ( len ( Del (f,1))) by A1, A3, FINSEQ_3: 109;

        

         A4: 1 in ( dom f) by Th6;

        let k be Nat such that

         A5: 1 <= k & k <= ( len (f /^ 1));

        k in ( dom (f /^ 1)) by A5, FINSEQ_3: 25;

        

        hence ((f /^ 1) . k) = (f . (k + 1)) by A2, RFINSEQ:def 1

        .= (( Del (f,1)) . k) by A1, A3, A5, A4, FINSEQ_3: 111;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_5:86

    for D be non empty set holds for f be non empty FinSequence of D holds f = ( <*(f . 1)*> ^ ( Del (f,1)))

    proof

      let D be non empty set;

      let f be non empty FinSequence of D;

      

       A1: 1 in ( dom f) by Th6;

      

      thus f = ( <*(f /. 1)*> ^ (f /^ 1)) by Th29

      .= ( <*(f . 1)*> ^ (f /^ 1)) by A1, PARTFUN1:def 6

      .= ( <*(f . 1)*> ^ ( Del (f,1))) by Th3;

    end;