finseq_4.miz



    begin

    reserve f for Function;

    reserve p,q for FinSequence;

    reserve A,B,C for set,

x,x1,x2,y,z for object;

    reserve k,l,m,n for Nat;

    reserve a for Nat;

    definition

      let f;

      let x be object;

      :: FINSEQ_4:def1

      pred f is_one-to-one_at x means (f " ( Im (f,x))) = {x};

    end

    theorem :: FINSEQ_4:1

    

     Th1: f is_one-to-one_at x implies x in ( dom f)

    proof

      assume f is_one-to-one_at x;

      then (f " ( Im (f,x))) = {x};

      then x in (f " ( Im (f,x))) by TARSKI:def 1;

      hence thesis by FUNCT_1:def 7;

    end;

    theorem :: FINSEQ_4:2

    

     Th2: f is_one-to-one_at x iff x in ( dom f) & (f " {(f . x)}) = {x}

    proof

      thus f is_one-to-one_at x implies x in ( dom f) & (f " {(f . x)}) = {x}

      proof

        assume

         A1: f is_one-to-one_at x;

        hence

         A2: x in ( dom f) by Th1;

        (f " ( Im (f,x))) = {x} by A1;

        hence thesis by A2, FUNCT_1: 59;

      end;

      assume x in ( dom f) & (f " {(f . x)}) = {x};

      hence (f " ( Im (f,x))) = {x} by FUNCT_1: 59;

    end;

    theorem :: FINSEQ_4:3

    

     Th3: f is_one-to-one_at x iff x in ( dom f) & for z st z in ( dom f) & x <> z holds (f . x) <> (f . z)

    proof

      thus f is_one-to-one_at x implies x in ( dom f) & for z st z in ( dom f) & x <> z holds (f . x) <> (f . z)

      proof

        assume

         A1: f is_one-to-one_at x;

        hence x in ( dom f) by Th1;

        let z;

        assume that

         A2: z in ( dom f) and

         A3: x <> z and

         A4: (f . x) = (f . z);

        (f . x) in {(f . x)} by TARSKI:def 1;

        then z in (f " {(f . x)}) by A2, A4, FUNCT_1:def 7;

        then z in {x} by A1, Th2;

        hence thesis by A3, TARSKI:def 1;

      end;

      assume that

       A5: x in ( dom f) and

       A6: for z st z in ( dom f) & x <> z holds (f . x) <> (f . z) and

       A7: not f is_one-to-one_at x;

      (f " {(f . x)}) <> {x} by A5, A7, Th2;

      then

      consider y be object such that

       A8: y in (f " {(f . x)}) & not y in {x} or y in {x} & not y in (f " {(f . x)}) by TARSKI: 2;

      (f . x) in {(f . x)} by TARSKI:def 1;

      then

       A9: x in (f " {(f . x)}) by A5, FUNCT_1:def 7;

      now

        per cases by A8;

          suppose

           A10: y in (f " {(f . x)}) & not y in {x};

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

          then

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

          y in ( dom f) & x <> y by A10, FUNCT_1:def 7, TARSKI:def 1;

          hence thesis by A6, A11;

        end;

          suppose not y in (f " {(f . x)}) & y in {x};

          hence thesis by A9, TARSKI:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_4:4

    (for x st x in ( dom f) holds f is_one-to-one_at x) iff f is one-to-one

    proof

      thus (for x st x in ( dom f) holds f is_one-to-one_at x) implies f is one-to-one

      proof

        assume

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

        let x1,x2 be object;

        assume that

         A2: x1 in ( dom f) and

         A3: x2 in ( dom f) & (f . x1) = (f . x2);

        f is_one-to-one_at x1 by A1, A2;

        hence thesis by A3, Th3;

      end;

      assume

       A4: f is one-to-one;

      let x;

      assume

       A5: x in ( dom f);

      then for z holds z in ( dom f) & x <> z implies (f . x) <> (f . z) by A4;

      hence thesis by A5, Th3;

    end;

    definition

      let R be Relation, y be object;

      :: FINSEQ_4:def2

      pred R just_once_values y means

      : Def2: ( card ( Coim (R,y))) = 1;

    end

    theorem :: FINSEQ_4:5

    

     Th5: f just_once_values y implies y in ( rng f)

    proof

      assume f just_once_values y;

      then ( card ( Coim (f,y))) = 1;

      then ( rng f) meets {y} by CARD_1: 27, RELAT_1: 138;

      then

      consider x be object such that

       A1: x in (( rng f) /\ {y}) by XBOOLE_0: 4;

      x in {y} by A1, XBOOLE_0:def 4;

      then y = x by TARSKI:def 1;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: FINSEQ_4:6

    

     Th6: f just_once_values y iff ex x st {x} = (f " {y}) by CARD_2: 42;

    theorem :: FINSEQ_4:7

    

     Th7: f just_once_values y iff ex x be object st x in ( dom f) & y = (f . x) & for z be object st z in ( dom f) & z <> x holds (f . z) <> y

    proof

      thus f just_once_values y implies ex x be object st x in ( dom f) & y = (f . x) & for z be object st z in ( dom f) & z <> x holds (f . z) <> y

      proof

        assume

         A1: f just_once_values y;

        then

         A2: ( card ( Coim (f,y))) = 1;

        y in ( rng f) by A1, Th5;

        then

        consider x1 be object such that

         A3: x1 in ( dom f) and

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

        (f . x1) in {y} by A4, TARSKI:def 1;

        then

         A5: x1 in (f " {y}) by A3, FUNCT_1:def 7;

        take x1;

        thus x1 in ( dom f) & y = (f . x1) by A3, A4;

        let z be object;

        assume that

         A6: z in ( dom f) and

         A7: z <> x1 and

         A8: (f . z) = y;

        

         A9: (f " {y}) is finite by A2;

        (f . z) in {y} by A8, TARSKI:def 1;

        then z in (f " {y}) by A6, FUNCT_1:def 7;

        then {z, x1} c= (f " {y}) by A5, ZFMISC_1: 32;

        then ( card {z, x1}) <= 1 by A9, A2, NAT_1: 43;

        then 2 <= 1 by A7, CARD_2: 57;

        hence thesis;

      end;

      given x be object such that

       A10: x in ( dom f) and

       A11: y = (f . x) and

       A12: for z be object st z in ( dom f) & z <> x holds (f . z) <> y;

      

       A13: {x} = (f " {y})

      proof

        thus {x} c= (f " {y})

        proof

          let x1 be object;

          assume x1 in {x};

          then

           A14: x1 = x by TARSKI:def 1;

          (f . x) in {y} by A11, TARSKI:def 1;

          hence thesis by A10, A14, FUNCT_1:def 7;

        end;

        let x1 be object;

        assume

         A15: x1 in (f " {y});

        then (f . x1) in {y} by FUNCT_1:def 7;

        then

         A16: (f . x1) = y by TARSKI:def 1;

        x1 in ( dom f) by A15, FUNCT_1:def 7;

        then x1 = x by A12, A16;

        hence thesis by TARSKI:def 1;

      end;

      ( card ( Coim (f,y))) = 1 by A13, CARD_1: 30;

      hence thesis;

    end;

    theorem :: FINSEQ_4:8

    

     Th8: f is one-to-one iff for y st y in ( rng f) holds f just_once_values y

    proof

      thus f is one-to-one implies for y st y in ( rng f) holds f just_once_values y

      proof

        assume

         A1: f is one-to-one;

        let y;

        assume y in ( rng f);

        then

        consider x be object such that

         A2: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

        for z be object holds z in ( dom f) & z <> x implies (f . z) <> y by A1, A2;

        hence thesis by A2, Th7;

      end;

      assume

       A3: for y st y in ( rng f) holds f just_once_values y;

      let x,y be object;

      assume that

       A4: x in ( dom f) and

       A5: y in ( dom f) & (f . x) = (f . y);

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

      then f just_once_values (f . x) by A3;

      then

      consider x1 such that

       A6: {x1} = (f " {(f . x)}) by Th6;

      

       A7: (f . x) in {(f . x)} by TARSKI:def 1;

      then

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

      x in (f " {(f . x)}) by A4, A7, FUNCT_1:def 7;

      then x = x1 by A6, TARSKI:def 1;

      hence thesis by A6, A8, TARSKI:def 1;

    end;

    theorem :: FINSEQ_4:9

    

     Th9: f is_one-to-one_at x iff x in ( dom f) & f just_once_values (f . x)

    proof

      thus f is_one-to-one_at x implies x in ( dom f) & f just_once_values (f . x)

      proof

        assume

         A1: f is_one-to-one_at x;

        hence x in ( dom f) by Th1;

         {x} = (f " {(f . x)}) by A1, Th2;

        hence thesis by Th6;

      end;

      assume that

       A2: x in ( dom f) and

       A3: f just_once_values (f . x);

      consider z such that

       A4: (f " {(f . x)}) = {z} by A3, Th6;

      (f . x) in {(f . x)} by TARSKI:def 1;

      then x in {z} by A2, A4, FUNCT_1:def 7;

      then x = z by TARSKI:def 1;

      hence thesis by A2, A4, Th2;

    end;

    definition

      let f, y;

      assume

       A1: f just_once_values y;

      :: FINSEQ_4:def3

      func f <- y -> set means

      : Def3: it in ( dom f) & (f . it ) = y;

      existence

      proof

        y in ( rng f) by A1, Th5;

        then

        consider x be object such that

         A2: x in ( dom f) & (f . x) = y by FUNCT_1:def 3;

        take x;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let x1,x2 be set;

        assume that

         A3: x1 in ( dom f) & (f . x1) = y and

         A4: x2 in ( dom f) & (f . x2) = y;

        consider x be object such that x in ( dom f) and (f . x) = y and

         A5: for z be object st z in ( dom f) & z <> x holds (f . z) <> y by A1, Th7;

        x = x1 by A3, A5;

        hence thesis by A4, A5;

      end;

    end

    theorem :: FINSEQ_4:10

    f just_once_values y implies ( Im (f,(f <- y))) = {y}

    proof

      assume

       A1: f just_once_values y;

      then (f <- y) in ( dom f) by Def3;

      

      hence ( Im (f,(f <- y))) = {(f . (f <- y))} by FUNCT_1: 59

      .= {y} by A1, Def3;

    end;

    theorem :: FINSEQ_4:11

    

     Th11: f just_once_values y implies (f " {y}) = {(f <- y)}

    proof

      assume

       A1: f just_once_values y;

      then

      consider x such that

       A2: {x} = (f " {y}) by Th6;

      

       A3: x in (f " {y}) by A2, ZFMISC_1: 31;

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

      then

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

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

      hence thesis by A1, A2, A4, Def3;

    end;

    theorem :: FINSEQ_4:12

    f is one-to-one & y in ( rng f) implies ((f " ) . y) = (f <- y)

    proof

      assume that

       A1: f is one-to-one and

       A2: y in ( rng f);

      consider x be object such that

       A3: x in ( dom f) & (f . x) = y by A2, FUNCT_1:def 3;

      f just_once_values y by A1, A2, Th8;

      then x = (f <- y) by A3, Def3;

      hence thesis by A1, A3, FUNCT_1: 32;

    end;

    theorem :: FINSEQ_4:13

    f is_one-to-one_at x implies (f <- (f . x)) = x

    proof

      assume f is_one-to-one_at x;

      then x in ( dom f) & f just_once_values (f . x) by Th9;

      hence thesis by Def3;

    end;

    theorem :: FINSEQ_4:14

    f just_once_values y implies f is_one-to-one_at (f <- y)

    proof

      assume

       A1: f just_once_values y;

       A2:

      now

        let x;

        assume x in ( dom f) & x <> (f <- y);

        then (f . x) <> y by A1, Def3;

        hence (f . x) <> (f . (f <- y)) by A1, Def3;

      end;

      (f <- y) in ( dom f) by A1, Def3;

      hence thesis by A2, Th3;

    end;

    reserve D for non empty set;

    reserve d,d1,d2,d3 for Element of D;

    definition

      let D;

      let d1, d2;

      :: original: <*

      redefine

      func <*d1,d2*> -> FinSequence of D ;

      coherence by FINSEQ_2: 13;

    end

    definition

      let D;

      let d1, d2, d3;

      :: original: <*

      redefine

      func <*d1,d2,d3*> -> FinSequence of D ;

      coherence by FINSEQ_2: 14;

    end

    theorem :: FINSEQ_4:15

    for i be Nat holds for D be set, P be FinSequence of D st 1 <= i & i <= ( len P) holds (P /. i) = (P . i)

    proof

      let i be Nat;

      let D be set, P be FinSequence of D;

      assume 1 <= i & i <= ( len P);

      then i in ( dom P) by FINSEQ_3: 25;

      hence thesis by PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:16

    ( <*d*> /. 1) = d

    proof

      

       A1: 1 in {1} by FINSEQ_1: 2;

      ( dom <*d*>) = {1} & ( <*d*> . 1) = d by FINSEQ_1: 2, FINSEQ_1:def 8;

      hence thesis by A1, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:17

    ( <*d1, d2*> /. 1) = d1 & ( <*d1, d2*> /. 2) = d2

    proof

      set s = <*d1, d2*>;

      

       A1: (s . 2) = d2 & 1 in {1, 2} by FINSEQ_1: 2, FINSEQ_1: 44;

      

       A2: 2 in {1, 2} by FINSEQ_1: 2;

      ( dom s) = {1, 2} & (s . 1) = d1 by FINSEQ_1: 2, FINSEQ_1: 44, FINSEQ_1: 89;

      hence thesis by A1, A2, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:18

    ( <*d1, d2, d3*> /. 1) = d1 & ( <*d1, d2, d3*> /. 2) = d2 & ( <*d1, d2, d3*> /. 3) = d3

    proof

      set s = <*d1, d2, d3*>;

      

       A1: (s . 2) = d2 & (s . 3) = d3 by FINSEQ_1: 45;

      

       A2: 1 in {1, 2, 3} & 2 in {1, 2, 3} by FINSEQ_3: 1;

      

       A3: 3 in {1, 2, 3} by FINSEQ_3: 1;

      ( dom s) = {1, 2, 3} & (s . 1) = d1 by FINSEQ_1: 45, FINSEQ_1: 89, FINSEQ_3: 1;

      hence thesis by A1, A2, A3, PARTFUN1:def 6;

    end;

    definition

      let p;

      let x be object;

      :: FINSEQ_4:def4

      func x .. p -> Element of NAT equals (( Sgm (p " {x})) . 1);

      coherence

      proof

        set q = ( Sgm (p " {x}));

        per cases ;

          suppose not 1 in ( dom q);

          then (q . 1) = 0 by FUNCT_1:def 2;

          hence thesis;

        end;

          suppose

           A1: 1 in ( dom q);

          

           A2: ( rng q) c= NAT by FINSEQ_1:def 4;

          (q . 1) in ( rng q) by A1, FUNCT_1:def 3;

          hence thesis by A2;

        end;

      end;

    end

    theorem :: FINSEQ_4:19

    

     Th19: x in ( rng p) implies (p . (x .. p)) = x

    proof

      set q = ( Sgm (p " {x}));

      

       A1: (p " {x}) c= ( dom p) & ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3, RELAT_1: 132;

      assume x in ( rng p);

      then (p " {x}) <> {} by FUNCT_1: 72;

      then ( rng q) <> {} by A1, FINSEQ_1:def 13;

      then 1 in ( dom q) by FINSEQ_3: 32;

      then

       A2: (q . 1) in ( rng q) by FUNCT_1:def 3;

      ( rng q) = (p " {x}) by A1, FINSEQ_1:def 13;

      then (p . (x .. p)) in {x} by A2, FUNCT_1:def 7;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FINSEQ_4:20

    

     Th20: x in ( rng p) implies (x .. p) in ( dom p)

    proof

      

       A1: (p " {x}) c= ( dom p) & ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3, RELAT_1: 132;

      assume x in ( rng p);

      then (p " {x}) <> {} by FUNCT_1: 72;

      then ( rng ( Sgm (p " {x}))) <> {} by A1, FINSEQ_1:def 13;

      then 1 in ( dom ( Sgm (p " {x}))) by FINSEQ_3: 32;

      then (x .. p) in ( rng ( Sgm (p " {x}))) by FUNCT_1:def 3;

      then (x .. p) in (p " {x}) by A1, FINSEQ_1:def 13;

      hence thesis by FUNCT_1:def 7;

    end;

    theorem :: FINSEQ_4:21

    

     Th21: x in ( rng p) implies 1 <= (x .. p) & (x .. p) <= ( len p)

    proof

      assume x in ( rng p);

      then (x .. p) in ( dom p) by Th20;

      hence thesis by FINSEQ_3: 25;

    end;

    theorem :: FINSEQ_4:22

    

     Th22: x in ( rng p) implies ((x .. p) - 1) is Element of NAT & (( len p) - (x .. p)) is Element of NAT

    proof

      assume x in ( rng p);

      then 1 <= (x .. p) & (x .. p) <= ( len p) by Th21;

      hence thesis by INT_1: 5;

    end;

    theorem :: FINSEQ_4:23

    

     Th23: x in ( rng p) implies (x .. p) in (p " {x})

    proof

      assume

       A1: x in ( rng p);

      then (p . (x .. p)) = x by Th19;

      then

       A2: (p . (x .. p)) in {x} by TARSKI:def 1;

      (x .. p) in ( dom p) by A1, Th20;

      hence thesis by A2, FUNCT_1:def 7;

    end;

    theorem :: FINSEQ_4:24

    

     Th24: for k st k in ( dom p) & k < (x .. p) holds (p . k) <> x

    proof

      let k;

      set q = ( Sgm (p " {x}));

      assume that

       A1: k in ( dom p) and

       A2: k < (x .. p) and

       A3: (p . k) = x;

      

       A4: x in {x} by TARSKI:def 1;

      

       A5: (p " {x}) c= ( dom p) & ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3, RELAT_1: 132;

      then ( rng q) = (p " {x}) by FINSEQ_1:def 13;

      then k in ( rng q) by A1, A3, A4, FUNCT_1:def 7;

      then

      consider y be object such that

       A6: y in ( dom q) and

       A7: (q . y) = k by FUNCT_1:def 3;

      reconsider y as Element of NAT by A6;

       A8:

      now

        assume not 1 < y;

        then 1 = y or y < 1 by XXREAL_0: 1;

        hence contradiction by A2, A6, A7, FINSEQ_3: 24, NAT_1: 14;

      end;

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

      then y <= ( len q) by A6, FINSEQ_1: 1;

      hence contradiction by A2, A5, A7, A8, FINSEQ_1:def 13;

    end;

    theorem :: FINSEQ_4:25

    

     Th25: p just_once_values x implies (p <- x) = (x .. p)

    proof

      assume

       A1: p just_once_values x;

      then x in ( rng p) by Th5;

      then (x .. p) in ( dom p) & (p . (x .. p)) = x by Th19, Th20;

      hence thesis by A1, Def3;

    end;

    theorem :: FINSEQ_4:26

    

     Th26: p just_once_values x implies for k st k in ( dom p) & k <> (x .. p) holds (p . k) <> x

    proof

      assume

       A1: p just_once_values x;

      let k;

      assume

       A2: k in ( dom p) & k <> (x .. p) & (p . k) = x;

      (p <- x) = (x .. p) by A1, Th25;

      hence thesis by A1, A2, Def3;

    end;

    theorem :: FINSEQ_4:27

    

     Th27: x in ( rng p) & (for k st k in ( dom p) & k <> (x .. p) holds (p . k) <> x) implies p just_once_values x

    proof

      assume that

       A1: x in ( rng p) and

       A2: for k st k in ( dom p) & k <> (x .. p) holds (p . k) <> x;

      

       A3: for z be object st z in ( dom p) & z <> (x .. p) holds (p . z) <> x by A2;

      (p . (x .. p)) = x & (x .. p) in ( dom p) by A1, Th19, Th20;

      hence thesis by A3, Th7;

    end;

    theorem :: FINSEQ_4:28

    p just_once_values x iff x in ( rng p) & {(x .. p)} = (p " {x})

    proof

      thus p just_once_values x implies x in ( rng p) & {(x .. p)} = (p " {x})

      proof

        assume

         A1: p just_once_values x;

        then (x .. p) = (p <- x) by Th25;

        hence thesis by A1, Th5, Th11;

      end;

      assume that

       A2: x in ( rng p) and

       A3: {(x .. p)} = (p " {x});

       A4:

      now

        let z be object;

        assume that

         A5: z in ( dom p) and

         A6: z <> (x .. p) and

         A7: (p . z) = x;

        (p . z) in {x} by A7, TARSKI:def 1;

        then z in (p " {x}) by A5, FUNCT_1:def 7;

        hence contradiction by A3, A6, TARSKI:def 1;

      end;

      (p . (x .. p)) = x & (x .. p) in ( dom p) by A2, Th19, Th20;

      hence thesis by A4, Th7;

    end;

    theorem :: FINSEQ_4:29

    p is one-to-one & x in ( rng p) implies {(x .. p)} = (p " {x})

    proof

      assume that

       A1: p is one-to-one and

       A2: x in ( rng p);

      thus {(x .. p)} c= (p " {x})

      proof

        let y be object;

        assume y in {(x .. p)};

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

        hence thesis by A2, Th23;

      end;

      let y be object;

      assume

       A3: y in (p " {x});

      then

       A4: y in ( dom p) by FUNCT_1:def 7;

      (p . y) in {x} by A3, FUNCT_1:def 7;

      then

       A5: (p . y) = x by TARSKI:def 1;

      (p . (x .. p)) = x & (x .. p) in ( dom p) by A2, Th19, Th20;

      then (x .. p) = y by A1, A4, A5;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FINSEQ_4:30

    

     Th30: p just_once_values x iff ( len (p - {x})) = (( len p) - 1)

    proof

      thus p just_once_values x implies ( len (p - {x})) = (( len p) - 1) by FINSEQ_3: 59;

      assume ( len (p - {x})) = (( len p) - 1);

      

      then (( len p) + ( - 1)) = (( len p) - ( card (p " {x}))) by FINSEQ_3: 59

      .= (( len p) + ( - ( card (p " {x}))));

      hence thesis;

    end;

    reserve L,M for Element of NAT ;

    theorem :: FINSEQ_4:31

    

     Th31: p just_once_values x implies for k st k in ( dom (p - {x})) holds (k < (x .. p) implies ((p - {x}) . k) = (p . k)) & ((x .. p) <= k implies ((p - {x}) . k) = (p . (k + 1)))

    proof

      assume

       A1: p just_once_values x;

      set q = (p - {x});

      let k;

      assume

       A2: k in ( dom (p - {x}));

      set A = { L : L in ( dom p) & L <= k & (p . L) in {x} };

      

       A3: ( dom (p - {x})) c= ( dom p) by FINSEQ_3: 63;

      thus k < (x .. p) implies ((p - {x}) . k) = (p . k)

      proof

        assume

         A4: k < (x .. p);

        A c= {}

        proof

          let y be object;

          assume y in A;

          then

          consider L such that y = L and

           A5: L in ( dom p) & L <= k and

           A6: (p . L) in {x};

          (p . L) <> x by A1, A4, A5, Th26;

          hence thesis by A6, TARSKI:def 1;

        end;

        then

         A7: A = {} ;

        (p . k) <> x by A1, A2, A3, A4, Th26;

        then not (p . k) in {x} by TARSKI:def 1;

        then (q . (k - 0 )) = (p . k) by A2, A3, A7, CARD_1: 27, FINSEQ_3: 85;

        hence thesis;

      end;

      set B = { M : M in ( dom p) & M <= (k + 1) & (p . M) in {x} };

      assume

       A8: (x .. p) <= k;

      

       A9: x in ( rng p) by A1, Th5;

      

       A10: B = {(x .. p)}

      proof

        thus B c= {(x .. p)}

        proof

          let y be object;

          assume y in B;

          then

          consider M such that

           A11: M = y and

           A12: M in ( dom p) and M <= (k + 1) and

           A13: (p . M) in {x};

          (p . M) = x by A13, TARSKI:def 1;

          then M = (x .. p) by A1, A12, Th26;

          hence thesis by A11, TARSKI:def 1;

        end;

        let y be object;

        assume y in {(x .. p)};

        then

         A14: y = (x .. p) by TARSKI:def 1;

        (p . (x .. p)) = x by A9, Th19;

        then

         A15: (p . (x .. p)) in {x} by TARSKI:def 1;

        (x .. p) in ( dom p) & (x .. p) <= (k + 1) by A9, A8, Th20, NAT_1: 12;

        hence thesis by A14, A15;

      end;

      then

      reconsider B as finite set;

      ( dom q) = ( Seg ( len q)) & ( len (p - {x})) = (( len p) - 1) by A1, Th30, FINSEQ_1:def 3;

      then k <= (( len p) - 1) by A2, FINSEQ_1: 1;

      then 1 <= (k + 1) & (k + 1) <= ( len p) by NAT_1: 12, XREAL_1: 19;

      then (k + 1) in ( Seg ( len p));

      then

       A16: (k + 1) in ( dom p) by FINSEQ_1:def 3;

      now

        (x .. p) <> (k + 1) by A8, XREAL_1: 29;

        then

         A17: (p . (k + 1)) <> x by A1, A16, Th26;

        assume (p . (k + 1)) in {x};

        hence contradiction by A17, TARSKI:def 1;

      end;

      then ((p - {x}) . ((k + 1) - ( card B))) = (p . (k + 1)) by A16, FINSEQ_3: 85;

      then (q . ((k + 1) - 1)) = (p . (k + 1)) by A10, CARD_1: 30;

      hence thesis;

    end;

    theorem :: FINSEQ_4:32

    p is one-to-one & x in ( rng p) implies for k st k in ( dom (p - {x})) holds (((p - {x}) . k) = (p . k) iff k < (x .. p)) & (((p - {x}) . k) = (p . (k + 1)) iff (x .. p) <= k)

    proof

      assume that

       A1: p is one-to-one and

       A2: x in ( rng p);

      set q = (p - {x});

      let k;

      assume

       A3: k in ( dom (p - {x}));

      

       A4: p just_once_values x by A1, A2, Th8;

      then ( dom q) = ( Seg ( len q)) & ( len (p - {x})) = (( len p) - 1) by Th30, FINSEQ_1:def 3;

      then k <= (( len p) - 1) by A3, FINSEQ_1: 1;

      then 1 <= (k + 1) & (k + 1) <= ( len p) by NAT_1: 12, XREAL_1: 19;

      then (k + 1) in ( Seg ( len p));

      then

       A5: ( dom (p - {x})) c= ( dom p) & (k + 1) in ( dom p) by FINSEQ_1:def 3, FINSEQ_3: 63;

      thus ((p - {x}) . k) = (p . k) implies k < (x .. p)

      proof

        assume that

         A6: ((p - {x}) . k) = (p . k) and

         A7: not k < (x .. p);

        (q . k) = (p . (k + 1)) by A4, A3, A7, Th31;

        then (k + 0 ) = (k + 1) by A1, A3, A5, A6;

        hence thesis;

      end;

      thus k < (x .. p) implies ((p - {x}) . k) = (p . k) by A4, A3, Th31;

      thus ((p - {x}) . k) = (p . (k + 1)) implies (x .. p) <= k

      proof

        assume

         A8: ((p - {x}) . k) = (p . (k + 1));

        assume not (x .. p) <= k;

        then (p . (k + 1)) = (p . k) by A4, A3, A8, Th31;

        then (k + 0 ) = (k + 1) by A1, A3, A5;

        hence thesis;

      end;

      thus thesis by A4, A3, Th31;

    end;

    definition

      let p;

      let x;

      assume

       A1: x in ( rng p);

      :: FINSEQ_4:def5

      func p -| x -> FinSequence means

      : Def5: ex n st n = ((x .. p) - 1) & it = (p | ( Seg n));

      existence

      proof

        reconsider n = ((x .. p) - 1) as Element of NAT by A1, Th22;

        reconsider q = (p | ( Seg n)) as FinSequence by FINSEQ_1: 15;

        take q;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: FINSEQ_4:33

    

     Th33: x in ( rng p) & n = ((x .. p) - 1) implies (p | ( Seg n)) = (p -| x)

    proof

      assume x in ( rng p);

      then ex m st m = ((x .. p) - 1) & (p | ( Seg m)) = (p -| x) by Def5;

      hence thesis;

    end;

    theorem :: FINSEQ_4:34

    

     Th34: x in ( rng p) implies ( len (p -| x)) = ((x .. p) - 1)

    proof

      assume

       A1: x in ( rng p);

      then

      consider n such that

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

       A3: (p | ( Seg n)) = (p -| x) by Def5;

      

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

      (n + 1) <= ( len p) by A1, A2, Th21;

      then n <= ( len p) by A4, XXREAL_0: 2;

      hence thesis by A2, A3, FINSEQ_1: 17;

    end;

    theorem :: FINSEQ_4:35

    

     Th35: x in ( rng p) & n = ((x .. p) - 1) implies ( dom (p -| x)) = ( Seg n)

    proof

      assume x in ( rng p);

      then ( len (p -| x)) = ((x .. p) - 1) by Th34;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: FINSEQ_4:36

    

     Th36: x in ( rng p) & k in ( dom (p -| x)) implies (p . k) = ((p -| x) . k)

    proof

      assume that

       A1: x in ( rng p) and

       A2: k in ( dom (p -| x));

      ex n st n = ((x .. p) - 1) & (p | ( Seg n)) = (p -| x) by A1, Def5;

      hence thesis by A2, FUNCT_1: 47;

    end;

    theorem :: FINSEQ_4:37

    

     Th37: x in ( rng p) implies not x in ( rng (p -| x))

    proof

      assume that

       A1: x in ( rng p) and

       A2: x in ( rng (p -| x));

      reconsider n = ((x .. p) - 1) as Element of NAT by A1, Th22;

      set r = (p | ( Seg n));

      

       A3: r = (p -| x) by A1, Th33;

      then

      consider y be object such that

       A4: y in ( dom r) and

       A5: (r . y) = x by A2, FUNCT_1:def 3;

      

       A6: ( dom r) = ( Seg n) by A1, A3, Th35;

      then

      reconsider y as Element of NAT by A4;

      y <= n by A4, A6, FINSEQ_1: 1;

      then

       A7: (y + 1) <= (x .. p) by XREAL_1: 19;

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

      then ( dom r) c= ( dom p) & y < (x .. p) by A7, RELAT_1: 60, XXREAL_0: 2;

      then (p . y) <> x by A4, Th24;

      hence thesis by A4, A5, FUNCT_1: 47;

    end;

    theorem :: FINSEQ_4:38

    x in ( rng p) implies ( rng (p -| x)) misses {x}

    proof

      assume x in ( rng p);

      then not x in ( rng (p -| x)) by Th37;

      then for y be object st y in ( rng (p -| x)) holds not y in {x} by TARSKI:def 1;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: FINSEQ_4:39

    x in ( rng p) implies ( rng (p -| x)) c= ( rng p)

    proof

      assume x in ( rng p);

      then ex n st n = ((x .. p) - 1) & (p | ( Seg n)) = (p -| x) by Def5;

      hence thesis by RELAT_1: 70;

    end;

    theorem :: FINSEQ_4:40

    x in ( rng p) implies ((x .. p) = 1 iff (p -| x) = {} )

    proof

      assume

       A1: x in ( rng p);

      thus (x .. p) = 1 implies (p -| x) = {}

      proof

        assume

         A2: (x .. p) = 1;

        ( len (p -| x)) = ((x .. p) - 1) by A1, Th34

        .= 0 by A2;

        hence thesis;

      end;

      assume (p -| x) = {} ;

      then

       A3: ( len (p -| x)) = 0 ;

      ( len (p -| x)) = ((x .. p) - 1) by A1, Th34;

      hence thesis by A3;

    end;

    theorem :: FINSEQ_4:41

    x in ( rng p) & p is FinSequence of D implies (p -| x) is FinSequence of D

    proof

      assume x in ( rng p);

      then ex n st n = ((x .. p) - 1) & (p | ( Seg n)) = (p -| x) by Def5;

      hence thesis by FINSEQ_1: 18;

    end;

    definition

      let p;

      let x;

      assume

       A1: x in ( rng p);

      :: FINSEQ_4:def6

      func p |-- x -> FinSequence means

      : Def6: ( len it ) = (( len p) - (x .. p)) & for k st k in ( dom it ) holds (it . k) = (p . (k + (x .. p)));

      existence

      proof

        deffunc F( Nat) = (p . ($1 + (x .. p)));

        reconsider n = (( len p) - (x .. p)) as Element of NAT by A1, Th22;

        consider q such that

         A2: ( len q) = n & for k be Nat st k in ( dom q) holds (q . k) = F(k) from FINSEQ_1:sch 2;

        take q;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let q,r be FinSequence;

        assume that

         A3: ( len q) = (( len p) - (x .. p)) and

         A4: for k st k in ( dom q) holds (q . k) = (p . (k + (x .. p)));

        assume that

         A5: ( len r) = (( len p) - (x .. p)) and

         A6: for k st k in ( dom r) holds (r . k) = (p . (k + (x .. p)));

        now

          let k be Nat;

          

           A7: ( dom q) = ( Seg ( len q)) & ( dom r) = ( Seg ( len r)) by FINSEQ_1:def 3;

          assume

           A8: k in ( dom q);

          then (q . k) = (p . (k + (x .. p))) by A4;

          hence (q . k) = (r . k) by A3, A5, A6, A8, A7;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

    end

    theorem :: FINSEQ_4:42

    

     Th42: x in ( rng p) & n = (( len p) - (x .. p)) implies ( dom (p |-- x)) = ( Seg n)

    proof

      assume x in ( rng p);

      then ( len (p |-- x)) = (( len p) - (x .. p)) by Def6;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: FINSEQ_4:43

    

     Th43: x in ( rng p) & n in ( dom (p |-- x)) implies (n + (x .. p)) in ( dom p)

    proof

      assume that

       A1: x in ( rng p) and

       A2: n in ( dom (p |-- x));

      reconsider m = (( len p) - (x .. p)) as Element of NAT by A1, Th22;

      n in ( Seg m) by A1, A2, Th42;

      then n <= (( len p) - (x .. p)) by FINSEQ_1: 1;

      then

       A3: (n + (x .. p)) <= ( len p) by XREAL_1: 19;

      1 <= n by A2, FINSEQ_3: 25;

      then 1 <= (n + (x .. p)) by NAT_1: 12;

      hence thesis by A3, FINSEQ_3: 25;

    end;

    theorem :: FINSEQ_4:44

    x in ( rng p) implies ( rng (p |-- x)) c= ( rng p)

    proof

      assume

       A1: x in ( rng p);

      let y be object;

      assume y in ( rng (p |-- x));

      then

      consider z be object such that

       A2: z in ( dom (p |-- x)) and

       A3: ((p |-- x) . z) = y by FUNCT_1:def 3;

      reconsider z as Element of NAT by A2;

      y = (p . (z + (x .. p))) & (z + (x .. p)) in ( dom p) by A1, A2, A3, Def6, Th43;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: FINSEQ_4:45

    

     Th45: p just_once_values x iff x in ( rng p) & not x in ( rng (p |-- x))

    proof

      thus p just_once_values x implies x in ( rng p) & not x in ( rng (p |-- x))

      proof

        assume

         A1: p just_once_values x;

        hence

         A2: x in ( rng p) by Th5;

        assume x in ( rng (p |-- x));

        then

        consider z be object such that

         A3: z in ( dom (p |-- x)) and

         A4: ((p |-- x) . z) = x by FUNCT_1:def 3;

        reconsider z as Element of NAT by A3;

        ((p |-- x) . z) = (p . (z + (x .. p))) & (z + (x .. p)) in ( dom p) by A2, A3, Def6, Th43;

        then (z + (x .. p)) = ( 0 + (x .. p)) by A1, A4, Th26;

        hence thesis by A3, FINSEQ_3: 24;

      end;

      assume that

       A5: x in ( rng p) and

       A6: not x in ( rng (p |-- x));

      now

        let k;

        assume that

         A7: k in ( dom p) and

         A8: k <> (x .. p) and

         A9: (p . k) = x;

        now

          per cases by A8, XXREAL_0: 1;

            suppose k < (x .. p);

            then (k + 1) <= (x .. p) by NAT_1: 13;

            then k <= ((x .. p) - 1) by XREAL_1: 19;

            then

             A10: k <= ( len (p -| x)) by A5, Th34;

            1 <= k by A7, FINSEQ_3: 25;

            then

             A11: k in ( dom (p -| x)) by A10, FINSEQ_3: 25;

            then x = ((p -| x) . k) by A5, A9, Th36;

            then x in ( rng (p -| x)) by A11, FUNCT_1:def 3;

            hence contradiction by A5, Th37;

          end;

            suppose

             A12: (x .. p) < k;

            then

            consider m be Nat such that

             A13: k = ((x .. p) + m) by NAT_1: 10;

            ((x .. p) + 0 ) < ((x .. p) + m) by A12, A13;

            then 0 < m;

            then

             A14: ( 0 + 1) <= m by NAT_1: 13;

            (m + (x .. p)) <= ( len p) by A7, A13, FINSEQ_3: 25;

            then m <= (( len p) - (x .. p)) by XREAL_1: 19;

            then m <= ( len (p |-- x)) by A5, Def6;

            then

             A15: m in ( dom (p |-- x)) by A14, FINSEQ_3: 25;

            then ((p |-- x) . m) = (p . k) by A5, A13, Def6;

            hence contradiction by A6, A9, A15, FUNCT_1:def 3;

          end;

        end;

        hence contradiction;

      end;

      hence thesis by A5, Th27;

    end;

    theorem :: FINSEQ_4:46

    

     Th46: x in ( rng p) & p is one-to-one implies not x in ( rng (p |-- x))

    proof

      assume that

       A1: x in ( rng p) and

       A2: p is one-to-one and

       A3: x in ( rng (p |-- x));

      

       A4: ( len (p |-- x)) = (( len p) - (x .. p)) by A1, Def6;

      consider y be object such that

       A5: y in ( dom (p |-- x)) and

       A6: ((p |-- x) . y) = x by A3, FUNCT_1:def 3;

      reconsider y as Element of NAT by A5;

      

       A7: 1 <= (y + (x .. p)) by A1, Th21, NAT_1: 12;

      

       A8: y in ( Seg ( len (p |-- x))) by A5, FINSEQ_1:def 3;

      then y <= ( len (p |-- x)) by FINSEQ_1: 1;

      then (y + (x .. p)) <= ( len p) by A4, XREAL_1: 19;

      then (y + (x .. p)) in ( Seg ( len p)) by A7;

      then

       A9: (y + (x .. p)) in ( dom p) by FINSEQ_1:def 3;

      

       A10: (x .. p) in ( dom p) & (p . (x .. p)) = x by A1, Th19, Th20;

      ((p |-- x) . y) = (p . (y + (x .. p))) by A1, A5, Def6;

      then ( 0 + (x .. p)) = (y + (x .. p)) by A2, A6, A10, A9;

      hence thesis by A8, FINSEQ_1: 1;

    end;

    theorem :: FINSEQ_4:47

    p just_once_values x iff x in ( rng p) & ( rng (p |-- x)) misses {x}

    proof

      thus p just_once_values x implies x in ( rng p) & ( rng (p |-- x)) misses {x}

      proof

        assume

         A1: p just_once_values x;

        hence x in ( rng p) by Th45;

        assume not ( rng (p |-- x)) misses {x};

        then

         A2: ex y be object st y in ( rng (p |-- x)) & y in {x} by XBOOLE_0: 3;

         not x in ( rng (p |-- x)) by A1, Th45;

        hence thesis by A2, TARSKI:def 1;

      end;

      assume that

       A3: x in ( rng p) and

       A4: ( rng (p |-- x)) misses {x};

      now

        

         A5: x in {x} by TARSKI:def 1;

        assume x in ( rng (p |-- x));

        hence contradiction by A4, A5, XBOOLE_0: 3;

      end;

      hence thesis by A3, Th45;

    end;

    theorem :: FINSEQ_4:48

    x in ( rng p) & p is one-to-one implies ( rng (p |-- x)) misses {x}

    proof

      assume x in ( rng p) & p is one-to-one;

      then not x in ( rng (p |-- x)) by Th46;

      then for y be object st y in ( rng (p |-- x)) holds not y in {x} by TARSKI:def 1;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: FINSEQ_4:49

    x in ( rng p) implies ((x .. p) = ( len p) iff (p |-- x) = {} )

    proof

      assume

       A1: x in ( rng p);

      thus (x .. p) = ( len p) implies (p |-- x) = {}

      proof

        assume

         A2: (x .. p) = ( len p);

        ( len (p |-- x)) = (( len p) - (x .. p)) by A1, Def6

        .= 0 by A2;

        hence thesis;

      end;

      assume (p |-- x) = {} ;

      then

       A3: ( len (p |-- x)) = 0 ;

      ( len (p |-- x)) = (( len p) - (x .. p)) by A1, Def6;

      hence thesis by A3;

    end;

    theorem :: FINSEQ_4:50

    x in ( rng p) & p is FinSequence of D implies (p |-- x) is FinSequence of D

    proof

      assume that

       A1: x in ( rng p) and

       A2: p is FinSequence of D;

      ( rng (p |-- x)) c= D

      proof

        

         A3: ( len (p |-- x)) = (( len p) - (x .. p)) by A1, Def6;

        let y be object;

        assume y in ( rng (p |-- x));

        then

        consider z be object such that

         A4: z in ( dom (p |-- x)) and

         A5: ((p |-- x) . z) = y by FUNCT_1:def 3;

        reconsider z as Element of NAT by A4;

        ( dom (p |-- x)) = ( Seg ( len (p |-- x))) by FINSEQ_1:def 3;

        then z <= ( len (p |-- x)) by A4, FINSEQ_1: 1;

        then

         A6: (z + (x .. p)) <= ( len p) by A3, XREAL_1: 19;

        1 <= (z + (x .. p)) by A1, Th21, NAT_1: 12;

        then (z + (x .. p)) in ( Seg ( len p)) by A6;

        then

         A7: (z + (x .. p)) in ( dom p) by FINSEQ_1:def 3;

        y = (p . (z + (x .. p))) by A1, A4, A5, Def6;

        then

         A8: y in ( rng p) by A7, FUNCT_1:def 3;

        ( rng p) c= D by A2, FINSEQ_1:def 4;

        hence thesis by A8;

      end;

      hence thesis by FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_4:51

    

     Th51: x in ( rng p) implies p = (((p -| x) ^ <*x*>) ^ (p |-- x))

    proof

      set q1 = (p -| x);

      set q2 = (p |-- x);

      set r = (q1 ^ <*x*>);

      assume

       A1: x in ( rng p);

       A2:

      now

        let k be Nat;

        assume k in ( dom q2);

        

        then (q2 . k) = (p . ((((x .. p) - 1) + 1) + k)) by A1, Def6

        .= (p . ((( len q1) + 1) + k)) by A1, Th34

        .= (p . ((( len q1) + ( len <*x*>)) + k)) by FINSEQ_1: 40

        .= (p . (( len r) + k)) by FINSEQ_1: 22;

        hence (p . (( len r) + k)) = (q2 . k);

      end;

       A3:

      now

        let k be Nat;

        assume

         A4: k in ( dom r);

        now

          per cases by A4, FINSEQ_1: 25;

            suppose

             A5: k in ( dom q1);

            

            hence (r . k) = (q1 . k) by FINSEQ_1:def 7

            .= (p . k) by A1, A5, Th36;

          end;

            suppose ex n be Nat st n in ( dom <*x*>) & k = (( len q1) + n);

            then

            consider n be Nat such that

             A6: n in ( dom <*x*>) and

             A7: k = (( len q1) + n);

            n in {1} by A6, FINSEQ_1: 2, FINSEQ_1:def 8;

            then

             A8: n = 1 by TARSKI:def 1;

            

            hence (r . k) = ( <*x*> . 1) by A6, A7, FINSEQ_1:def 7

            .= x by FINSEQ_1:def 8

            .= (p . (((x .. p) - 1) + 1)) by A1, Th19

            .= (p . k) by A1, A7, A8, Th34;

          end;

        end;

        hence (p . k) = (r . k);

      end;

      ( len p) = ((( len p) - (x .. p)) + (x .. p))

      .= ((((x .. p) - 1) + 1) + ( len q2)) by A1, Def6

      .= ((( len q1) + 1) + ( len q2)) by A1, Th34

      .= ((( len q1) + ( len <*x*>)) + ( len q2)) by FINSEQ_1: 40

      .= (( len r) + ( len q2)) by FINSEQ_1: 22;

      hence thesis by A3, A2, FINSEQ_3: 38;

    end;

    theorem :: FINSEQ_4:52

    x in ( rng p) & p is one-to-one implies (p -| x) is one-to-one

    proof

      assume x in ( rng p);

      

      then p = (((p -| x) ^ <*x*>) ^ (p |-- x)) by Th51

      .= ((p -| x) ^ ( <*x*> ^ (p |-- x))) by FINSEQ_1: 32;

      hence thesis by FINSEQ_3: 91;

    end;

    theorem :: FINSEQ_4:53

    x in ( rng p) & p is one-to-one implies (p |-- x) is one-to-one

    proof

      assume x in ( rng p);

      then p = (((p -| x) ^ <*x*>) ^ (p |-- x)) by Th51;

      hence thesis by FINSEQ_3: 91;

    end;

    theorem :: FINSEQ_4:54

    

     Th54: p just_once_values x iff x in ( rng p) & (p - {x}) = ((p -| x) ^ (p |-- x))

    proof

      set q = (p - {x});

      set r = (p -| x);

      set s = (p |-- x);

      thus p just_once_values x implies x in ( rng p) & (p - {x}) = ((p -| x) ^ (p |-- x))

      proof

        assume

         A1: p just_once_values x;

        hence

         A2: x in ( rng p) by Th5;

         A3:

        now

          (x .. p) <= ( len p) by A2, Th21;

          then ((x .. p) - 1) <= (( len p) - 1) by XREAL_1: 9;

          then ( len r) <= (( len p) - 1) by A2, Th34;

          then ( len r) <= ( len q) by A1, Th30;

          then

           A4: ( Seg ( len r)) c= ( Seg ( len q)) by FINSEQ_1: 5;

          let k be Nat;

          

           A5: ( Seg ( len r)) = ( dom r) & ( Seg ( len q)) = ( dom q) by FINSEQ_1:def 3;

          assume

           A6: k in ( dom r);

          then k in ( Seg ( len r)) by FINSEQ_1:def 3;

          then k <= ( len r) by FINSEQ_1: 1;

          then k <= ((x .. p) - 1) by A2, Th34;

          then

           A7: (k + 1) <= (x .. p) by XREAL_1: 19;

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

          then

           A8: k < (x .. p) by A7, XXREAL_0: 2;

          (r . k) = (p . k) by A2, A6, Th36;

          hence (q . k) = (r . k) by A1, A6, A4, A5, A8, Th31;

        end;

         A9:

        now

          reconsider m = ((x .. p) - 1) as Element of NAT by A2, Th22;

          let k be Nat;

          set z = (k + m);

          assume

           A10: k in ( dom s);

          then

           A11: (s . k) = (p . (k + (x .. p))) by A2, Def6;

          

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

          then

           A13: 1 <= k by A10, FINSEQ_1: 1;

          then ((x .. p) + 1) <= (k + (x .. p)) by XREAL_1: 7;

          then

           A14: (x .. p) <= ((k + (x .. p)) - 1) by XREAL_1: 19;

          k <= ( len s) by A10, A12, FINSEQ_1: 1;

          then k <= (( len p) - (x .. p)) by A2, Def6;

          then (k + (x .. p)) <= ( len p) by XREAL_1: 19;

          then ((k + (x .. p)) - 1) <= (( len p) - 1) by XREAL_1: 9;

          then

           A15: ((k + (x .. p)) - 1) <= ( len q) by A1, Th30;

          1 <= (x .. p) by A2, Th21;

          then (1 + 1) <= (k + (x .. p)) by A13, XREAL_1: 7;

          then

           A16: 1 <= ((k + (x .. p)) - 1) by XREAL_1: 19;

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

          then z in ( dom q) by A16, A15;

          

          then (q . z) = (p . (z + 1)) by A1, A14, Th31

          .= (p . (k + (x .. p)));

          hence (q . (( len r) + k)) = (s . k) by A2, A11, Th34;

        end;

        (( len r) + ( len s)) = (((x .. p) - 1) + ( len s)) by A2, Th34

        .= (((x .. p) - 1) + (( len p) - (x .. p))) by A2, Def6

        .= (( len p) - 1)

        .= ( len q) by A1, Th30;

        then ( dom q) = ( Seg (( len r) + ( len s))) by FINSEQ_1:def 3;

        hence thesis by A3, A9, FINSEQ_1:def 7;

      end;

      assume

       A17: x in ( rng p);

      assume

       A18: (p - {x}) = ((p -| x) ^ (p |-- x));

      now

        let k;

        assume that

         A19: k in ( dom p) and

         A20: k <> (x .. p) and

         A21: (p . k) = x;

         {(x .. p), k} c= (p " {x})

        proof

          let y be object;

          assume

           A22: y in {(x .. p), k};

          

           A23: x in {x} by TARSKI:def 1;

          (x .. p) in ( dom p) & (p . (x .. p)) = x by A17, Th19, Th20;

          then

           A24: (x .. p) in (p " {x}) by A23, FUNCT_1:def 7;

          k in (p " {x}) by A19, A21, A23, FUNCT_1:def 7;

          hence thesis by A22, A24, TARSKI:def 2;

        end;

        then ( card {(x .. p), k}) <= ( card (p " {x})) by NAT_1: 43;

        then

         A25: 2 <= ( card (p " {x})) by A20, CARD_2: 57;

        

         A26: ( len q) = (( len p) - ( card (p " {x}))) by FINSEQ_3: 59

        .= (( len p) + ( - ( card (p " {x}))));

        ( len q) = (( len r) + ( len s)) by A18, FINSEQ_1: 22

        .= (((x .. p) - 1) + ( len s)) by A17, Th34

        .= (((x .. p) - 1) + (( len p) - (x .. p))) by A17, Def6

        .= (( len p) + ( - 1));

        hence contradiction by A26, A25;

      end;

      hence thesis by A17, Th27;

    end;

    theorem :: FINSEQ_4:55

    x in ( rng p) & p is one-to-one implies (p - {x}) = ((p -| x) ^ (p |-- x))

    proof

      assume x in ( rng p) & p is one-to-one;

      then p just_once_values x by Th8;

      hence thesis by Th54;

    end;

    theorem :: FINSEQ_4:56

    

     Th56: x in ( rng p) & (p - {x}) is one-to-one & (p - {x}) = ((p -| x) ^ (p |-- x)) implies p is one-to-one

    proof

      assume that

       A1: x in ( rng p) and

       A2: (p - {x}) is one-to-one and

       A3: (p - {x}) = ((p -| x) ^ (p |-- x));

      set q = (p - {x});

      let x1,x2 be object;

      assume that

       A4: x1 in ( dom p) and

       A5: x2 in ( dom p) and

       A6: (p . x1) = (p . x2);

      reconsider k1 = x1, k2 = x2 as Element of NAT by A4, A5;

      

       A7: p just_once_values x by A1, A3, Th54;

      now

        per cases by XXREAL_0: 1;

          suppose x1 = (x .. p) & x2 = (x .. p);

          hence thesis;

        end;

          suppose x1 = (x .. p) & (x .. p) < k2;

          hence thesis by A1, A5, A6, A7, Th19, Th26;

        end;

          suppose x1 = (x .. p) & k2 < (x .. p);

          hence thesis by A1, A5, A6, A7, Th19, Th26;

        end;

          suppose k1 < (x .. p) & (x .. p) = x2;

          hence thesis by A1, A4, A6, A7, Th19, Th26;

        end;

          suppose

           A8: k1 < (x .. p) & (x .. p) < k2;

          (x .. p) <= ( len p) by A1, Th21;

          then k1 < ( len p) by A8, XXREAL_0: 2;

          then (k1 + 1) <= ( len p) by NAT_1: 13;

          then k1 <= (( len p) - 1) by XREAL_1: 19;

          then

           A9: k1 <= ( len q) by A7, Th30;

          k1 in ( Seg ( len p)) by A4, FINSEQ_1:def 3;

          then 1 <= k1 by FINSEQ_1: 1;

          then k1 in ( Seg ( len q)) by A9;

          then

           A10: k1 in ( dom q) by FINSEQ_1:def 3;

          then

           A11: (q . k1) = (p . k1) by A7, A8, Th31;

          consider m2 be Nat such that

           A12: k2 = (m2 + 1) by A8, NAT_1: 6;

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

          

           A13: (x .. p) <= m2 by A8, A12, NAT_1: 13;

          k2 in ( Seg ( len p)) by A5, FINSEQ_1:def 3;

          then k2 <= ( len p) by FINSEQ_1: 1;

          then m2 <= (( len p) - 1) by A12, XREAL_1: 19;

          then

           A14: m2 <= ( len q) by A7, Th30;

          1 <= (x .. p) by A1, Th21;

          then 1 <= m2 by A13, XXREAL_0: 2;

          then m2 in ( Seg ( len q)) by A14;

          then

           A15: m2 in ( dom (p - {x})) by FINSEQ_1:def 3;

          then (q . m2) = (p . k2) by A7, A12, A13, Th31;

          hence thesis by A2, A6, A8, A10, A13, A15, A11;

        end;

          suppose

           A16: k1 < (x .. p) & k2 < (x .. p);

          

           A17: (x .. p) <= ( len p) by A1, Th21;

          then k2 < ( len p) by A16, XXREAL_0: 2;

          then (k2 + 1) <= ( len p) by NAT_1: 13;

          then k2 <= (( len p) - 1) by XREAL_1: 19;

          then

           A18: k2 <= ( len q) by A7, Th30;

          k2 in ( Seg ( len p)) by A5, FINSEQ_1:def 3;

          then 1 <= k2 by FINSEQ_1: 1;

          then k2 in ( Seg ( len q)) by A18;

          then

           A19: k2 in ( dom q) by FINSEQ_1:def 3;

          then

           A20: (p . k2) = ((p - {x}) . k2) by A7, A16, Th31;

          k1 < ( len p) by A16, A17, XXREAL_0: 2;

          then (k1 + 1) <= ( len p) by NAT_1: 13;

          then k1 <= (( len p) - 1) by XREAL_1: 19;

          then

           A21: k1 <= ( len q) by A7, Th30;

          k1 in ( Seg ( len p)) by A4, FINSEQ_1:def 3;

          then 1 <= k1 by FINSEQ_1: 1;

          then k1 in ( Seg ( len q)) by A21;

          then

           A22: k1 in ( dom q) by FINSEQ_1:def 3;

          then (p . k1) = ((p - {x}) . k1) by A7, A16, Th31;

          hence thesis by A2, A6, A22, A19, A20;

        end;

          suppose

           A23: (x .. p) < k1 & (x .. p) < k2;

          then

          consider m2 be Nat such that

           A24: k2 = (m2 + 1) by NAT_1: 6;

          consider m1 be Nat such that

           A25: k1 = (m1 + 1) by A23, NAT_1: 6;

          reconsider m1, m2 as Element of NAT by ORDINAL1:def 12;

          k2 in ( Seg ( len p)) by A5, FINSEQ_1:def 3;

          then k2 <= ( len p) by FINSEQ_1: 1;

          then m2 <= (( len p) - 1) by A24, XREAL_1: 19;

          then

           A26: m2 <= ( len q) by A7, Th30;

          

           A27: 1 <= (x .. p) by A1, Th21;

          

           A28: (x .. p) <= m2 by A23, A24, NAT_1: 13;

          then 1 <= m2 by A27, XXREAL_0: 2;

          then m2 in ( Seg ( len q)) by A26;

          then

           A29: m2 in ( dom (p - {x})) by FINSEQ_1:def 3;

          then

           A30: (p . k2) = ((p - {x}) . m2) by A7, A24, A28, Th31;

          k1 in ( Seg ( len p)) by A4, FINSEQ_1:def 3;

          then k1 <= ( len p) by FINSEQ_1: 1;

          then m1 <= (( len p) - 1) by A25, XREAL_1: 19;

          then

           A31: m1 <= ( len q) by A7, Th30;

          

           A32: (x .. p) <= m1 by A23, A25, NAT_1: 13;

          then 1 <= m1 by A27, XXREAL_0: 2;

          then m1 in ( Seg ( len q)) by A31;

          then

           A33: m1 in ( dom (p - {x})) by FINSEQ_1:def 3;

          then (p . k1) = ((p - {x}) . m1) by A7, A25, A32, Th31;

          hence thesis by A2, A6, A25, A24, A33, A29, A30;

        end;

          suppose (x .. p) < k1 & (x .. p) = x2;

          hence thesis by A1, A4, A6, A7, Th19, Th26;

        end;

          suppose

           A34: (x .. p) < k1 & k2 < (x .. p);

          (x .. p) <= ( len p) by A1, Th21;

          then k2 < ( len p) by A34, XXREAL_0: 2;

          then (k2 + 1) <= ( len p) by NAT_1: 13;

          then k2 <= (( len p) - 1) by XREAL_1: 19;

          then

           A35: k2 <= ( len q) by A7, Th30;

          k2 in ( Seg ( len p)) by A5, FINSEQ_1:def 3;

          then 1 <= k2 by FINSEQ_1: 1;

          then k2 in ( Seg ( len q)) by A35;

          then

           A36: k2 in ( dom q) by FINSEQ_1:def 3;

          then

           A37: (q . k2) = (p . k2) by A7, A34, Th31;

          consider m2 be Nat such that

           A38: k1 = (m2 + 1) by A34, NAT_1: 6;

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

          

           A39: (x .. p) <= m2 by A34, A38, NAT_1: 13;

          k1 in ( Seg ( len p)) by A4, FINSEQ_1:def 3;

          then k1 <= ( len p) by FINSEQ_1: 1;

          then m2 <= (( len p) - 1) by A38, XREAL_1: 19;

          then

           A40: m2 <= ( len q) by A7, Th30;

          1 <= (x .. p) by A1, Th21;

          then 1 <= m2 by A39, XXREAL_0: 2;

          then m2 in ( Seg ( len q)) by A40;

          then

           A41: m2 in ( dom (p - {x})) by FINSEQ_1:def 3;

          then (q . m2) = (p . k1) by A7, A38, A39, Th31;

          hence thesis by A2, A6, A34, A36, A39, A41, A37;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_4:57

    x in ( rng p) & p is one-to-one implies ( rng (p -| x)) misses ( rng (p |-- x))

    proof

      assume that

       A1: x in ( rng p) and

       A2: p is one-to-one;

      p = (((p -| x) ^ <*x*>) ^ (p |-- x)) by A1, Th51;

      then ( rng (p |-- x)) misses ( rng ((p -| x) ^ <*x*>)) by A2, FINSEQ_3: 91;

      hence thesis by FINSEQ_1: 29, XBOOLE_1: 63;

    end;

    theorem :: FINSEQ_4:58

    

     Th58: A is finite implies ex p st ( rng p) = A & p is one-to-one

    proof

      defpred P[ set] means ex p st ( rng p) = $1 & p is one-to-one;

      ( rng {} ) = {} ;

      then

       A1: P[ {} ];

      now

        let B, C;

        assume that B in A and C c= A;

        given p such that

         A2: ( rng p) = C and

         A3: p is one-to-one;

         A4:

        now

          assume

           A5: not B in C;

          take q = (p ^ <*B*>);

          

          thus ( rng q) = (( rng p) \/ ( rng <*B*>)) by FINSEQ_1: 31

          .= (C \/ {B}) by A2, FINSEQ_1: 38;

          thus q is one-to-one

          proof

            let x,y be object;

            assume that

             A6: x in ( dom q) & y in ( dom q) and

             A7: (q . x) = (q . y);

            reconsider k = x, l = y as Element of NAT by A6;

             A8:

            now

              assume

               A9: k in ( dom p);

              given n be Nat such that

               A10: n in ( dom <*B*>) and

               A11: l = (( len p) + n);

              n in {1} by A10, FINSEQ_1: 2, FINSEQ_1: 38;

              then

               A12: n = 1 by TARSKI:def 1;

              ( <*B*> . n) = (q . k) by A7, A10, A11, FINSEQ_1:def 7

              .= (p . k) by A9, FINSEQ_1:def 7;

              then B = (p . k) by A12, FINSEQ_1:def 8;

              hence thesis by A2, A5, A9, FUNCT_1:def 3;

            end;

             A13:

            now

              assume

               A14: l in ( dom p);

              given n be Nat such that

               A15: n in ( dom <*B*>) and

               A16: k = (( len p) + n);

              n in {1} by A15, FINSEQ_1: 2, FINSEQ_1: 38;

              then

               A17: n = 1 by TARSKI:def 1;

              ( <*B*> . n) = (q . l) by A7, A15, A16, FINSEQ_1:def 7

              .= (p . l) by A14, FINSEQ_1:def 7;

              then B = (p . l) by A17, FINSEQ_1:def 8;

              hence thesis by A2, A5, A14, FUNCT_1:def 3;

            end;

             A18:

            now

              given m1 be Nat such that

               A19: m1 in ( dom <*B*>) and

               A20: k = (( len p) + m1);

              m1 in {1} by A19, FINSEQ_1: 2, FINSEQ_1:def 8;

              then

               A21: m1 = 1 by TARSKI:def 1;

              given m2 be Nat such that

               A22: m2 in ( dom <*B*>) and

               A23: l = (( len p) + m2);

              m2 in {1} by A22, FINSEQ_1: 2, FINSEQ_1:def 8;

              hence thesis by A20, A23, A21, TARSKI:def 1;

            end;

            now

              assume

               A24: k in ( dom p) & l in ( dom p);

              then (q . k) = (p . k) & (q . l) = (p . l) by FINSEQ_1:def 7;

              hence thesis by A3, A7, A24;

            end;

            hence thesis by A6, A8, A13, A18, FINSEQ_1: 25;

          end;

        end;

        now

          assume

           A25: B in C;

          take q = p;

          thus ( rng q) = (C \/ {B}) & q is one-to-one by A2, A3, A25, ZFMISC_1: 40;

        end;

        hence ex p st ( rng p) = (C \/ {B}) & p is one-to-one by A4;

      end;

      then

       A26: for B,C be set st B in A & C c= A & P[C] holds P[(C \/ {B})];

      assume

       A27: A is finite;

      thus P[A] from FINSET_1:sch 2( A27, A1, A26);

    end;

    theorem :: FINSEQ_4:59

    

     Th59: ( rng p) c= ( dom p) & p is one-to-one implies ( rng p) = ( dom p)

    proof

      defpred P[ Nat] means for q st ( len q) = $1 & ( rng q) c= ( dom q) & q is one-to-one holds ( rng q) = ( dom q);

      

       A1: ( len p) = ( len p);

      now

        let k;

        assume

         A2: for q st ( len q) = k & ( rng q) c= ( dom q) & q is one-to-one holds ( rng q) = ( dom q);

        let q;

        assume that

         A3: ( len q) = (k + 1) and

         A4: ( rng q) c= ( dom q) and

         A5: q is one-to-one;

        

         A6: ( dom q) = ( Seg (k + 1)) by A3, FINSEQ_1:def 3;

        ( dom q) c= ( rng q)

        proof

          let x be object;

          assume

           A7: x in ( dom q);

          then

          reconsider n = x as Element of NAT ;

          per cases ;

            suppose

             A8: (k + 1) in ( rng q);

            now

              per cases ;

                suppose n = (k + 1);

                hence thesis by A8;

              end;

                suppose n <> (k + 1);

                then not x in {(k + 1)} by TARSKI:def 1;

                then x in (( Seg (k + 1)) \ {(k + 1)}) by A6, A7, XBOOLE_0:def 5;

                then

                 A9: x in ( Seg k) by FINSEQ_1: 10;

                set r = (q - {(k + 1)});

                

                 A10: ( len r) = ((k + 1) - 1) by A3, A5, A8, FINSEQ_3: 90;

                then

                 A11: ( dom r) = ( Seg k) by FINSEQ_1:def 3;

                

                 A12: ( rng r) = (( rng q) \ {(k + 1)}) by FINSEQ_3: 65;

                then ( rng r) c= (( Seg (k + 1)) \ {(k + 1)}) by A4, A6, XBOOLE_1: 33;

                then ( rng r) c= ( dom r) by A11, FINSEQ_1: 10;

                then ( rng r) = ( dom r) by A2, A5, A10, FINSEQ_3: 87;

                hence thesis by A12, A11, A9;

              end;

            end;

            hence thesis;

          end;

            suppose

             A13: not (k + 1) in ( rng q);

            

             A14: ( rng q) c= ( Seg k)

            proof

              let x be object;

              assume

               A15: x in ( rng q);

              then not x in {(k + 1)} by A13, TARSKI:def 1;

              then x in (( Seg (k + 1)) \ {(k + 1)}) by A4, A6, A15, XBOOLE_0:def 5;

              hence thesis by FINSEQ_1: 10;

            end;

            

             A16: (k + 1) in ( Seg (k + 1)) by FINSEQ_1: 4;

            then

             A17: (q . (k + 1)) in ( rng q) by A6, FUNCT_1:def 3;

            reconsider r = (q | ( Seg k)) as FinSequence by FINSEQ_1: 15;

            

             A18: ( dom r) c= ( dom q) & k < (k + 1) by RELAT_1: 60, XREAL_1: 29;

            

             A19: ( len r) = k by A3, FINSEQ_3: 53;

            then

             A20: ( dom r) = ( Seg k) by FINSEQ_1:def 3;

            ( rng r) c= ( rng q) & r is one-to-one by A5, FUNCT_1: 52, RELAT_1: 70;

            then ( rng r) = ( dom r) by A2, A19, A20, A14, XBOOLE_1: 1;

            then

            consider x be object such that

             A21: x in ( dom r) and

             A22: (r . x) = (q . (k + 1)) by A20, A14, A17, FUNCT_1:def 3;

            reconsider n = x as Element of NAT by A21;

            (r . x) = (q . x) & n <= k by A20, A21, FINSEQ_1: 1, FUNCT_1: 49;

            hence thesis by A5, A6, A16, A21, A22, A18;

          end;

        end;

        hence ( rng q) = ( dom q) by A4;

      end;

      then

       A23: for k st P[k] holds P[(k + 1)];

      now

        let q;

        assume

         A24: ( len q) = 0 ;

        assume that ( rng q) c= ( dom q) and q is one-to-one;

        q = {} by A24;

        hence ( rng q) = ( dom q);

      end;

      then

       A25: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A25, A23);

      hence thesis by A1;

    end;

    theorem :: FINSEQ_4:60

    

     Th60: ( rng p) = ( dom p) implies p is one-to-one

    proof

      defpred P[ Nat] means for p st ( len p) = $1 & ( rng p) = ( dom p) holds p is one-to-one;

      

       A1: ( len p) = ( len p);

       A2:

      now

        let k;

        assume

         A3: P[k];

        thus P[(k + 1)]

        proof

          set x = (k + 1);

          let p;

          set q = (p - {(k + 1)});

          assume that

           A4: ( len p) = (k + 1) and

           A5: ( rng p) = ( dom p);

          

           A6: ( dom p) = ( Seg (k + 1)) by A4, FINSEQ_1:def 3;

          then

           A7: (k + 1) in ( rng p) by A5, FINSEQ_1: 4;

          now

            ( rng q) = (( Seg (k + 1)) \ {(k + 1)}) by A5, A6, FINSEQ_3: 65

            .= ( Seg k) by FINSEQ_1: 10;

            then ( card ( rng q)) = k by FINSEQ_1: 57;

            then

             A8: ( card k) = ( card ( rng q));

            (p . (x .. p)) = x by A5, A6, Th19, FINSEQ_1: 4;

            then

             A9: (p . (x .. p)) in {(k + 1)} by TARSKI:def 1;

            let l;

            assume that

             A10: l in ( dom p) and

             A11: l <> ((k + 1) .. p) and

             A12: (p . l) = (k + 1);

            

             A13: ( card {(x .. p), l}) = 2 by A11, CARD_2: 57;

            (p . l) in {(k + 1)} by A12, TARSKI:def 1;

            then

             A14: l in (p " {x}) by A10, FUNCT_1:def 7;

            (x .. p) in ( dom p) by A5, A6, Th20, FINSEQ_1: 4;

            then (x .. p) in (p " {x}) by A9, FUNCT_1:def 7;

            then {(x .. p), l} c= (p " {(k + 1)}) by A14, ZFMISC_1: 32;

            then

             A15: 2 <= ( card (p " {(k + 1)})) by A13, NAT_1: 43;

            ( len q) = ((k + 1) - ( card (p " {(k + 1)}))) by A4, FINSEQ_3: 59;

            then (2 + ( len q)) <= (( card (p " {x})) + ((k + 1) - ( card (p " {(k + 1)})))) by A15, XREAL_1: 6;

            then ((( len q) + 1) + 1) <= (k + 1);

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

            then

             A16: ( len q) <= (k - 1) by XREAL_1: 19;

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

            then ( card ( Segm k)) c= ( card ( dom q)) & ( card ( Segm ( len q))) = ( card ( dom q)) by CARD_1: 12, FINSEQ_1: 57, A8;

            then k <= ( len q) by NAT_1: 40;

            then k <= (k - 1) by A16, XXREAL_0: 2;

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

            hence contradiction by XREAL_1: 6;

          end;

          then

           A17: p just_once_values (k + 1) by A7, Th27;

          

          then

           A18: ( len q) = ((k + 1) - 1) by A4, Th30

          .= k;

          

           A19: q = ((p -| (k + 1)) ^ (p |-- (k + 1))) by A17, Th54;

          ( rng q) = (( Seg (k + 1)) \ {(k + 1)}) by A5, A6, FINSEQ_3: 65

          .= ( Seg k) by FINSEQ_1: 10;

          then ( dom q) = ( rng q) by A18, FINSEQ_1:def 3;

          hence thesis by A3, A7, A18, A19, Th56;

        end;

      end;

      

       A20: P[ 0 ]

      proof

        let p;

        assume ( len p) = 0 ;

        then p = {} ;

        hence thesis;

      end;

      for k holds P[k] from NAT_1:sch 2( A20, A2);

      hence thesis by A1;

    end;

    theorem :: FINSEQ_4:61

    ( rng p) = ( rng q) & ( len p) = ( len q) & q is one-to-one implies p is one-to-one

    proof

      assume that

       A1: ( rng p) = ( rng q) and

       A2: ( len p) = ( len q) and

       A3: q is one-to-one;

      

       A4: ( rng p) = ( dom (q " )) by A1, A3, FUNCT_1: 33;

      

      then

       A5: ( dom ((q " ) * p)) = ( dom p) by RELAT_1: 27

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

      then

      reconsider r = ((q " ) * p) as FinSequence by FINSEQ_1:def 2;

      ( rng r) = ( rng (q " )) by A4, RELAT_1: 28

      .= ( dom q) by A3, FUNCT_1: 33

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

      then r is one-to-one by A2, A5, Th60;

      hence thesis by A4, FUNCT_1: 26;

    end;

    

     Lm1: for A,B be finite set, f be Function of A, B st ( card A) = ( card B) & f is onto holds f is one-to-one

    proof

      let A,B be finite set, f be Function of A, B;

      assume that

       A1: ( card A) = ( card B) and

       A2: f is onto;

      

       a2: ( rng f) = B by A2, FUNCT_2:def 3;

      

       A3: (A,B) are_equipotent by A1, CARD_1: 5;

      consider p such that

       A4: ( rng p) = A and

       A5: p is one-to-one by Th58;

      (( dom p),(p .: ( dom p))) are_equipotent by A5, CARD_1: 33;

      then (( dom p),A) are_equipotent by A4, RELAT_1: 113;

      then

       A6: (( dom p),B) are_equipotent by A3, WELLORD2: 15;

      reconsider X = ( dom p) as finite set;

      consider q such that

       A7: ( rng q) = B and

       A8: q is one-to-one by Th58;

      

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

      (( dom q),(q .: ( dom q))) are_equipotent by A8, CARD_1: 33;

      then (( dom q),B) are_equipotent by A7, RELAT_1: 113;

      then (( dom p),( dom q)) are_equipotent by A6, WELLORD2: 15;

      

      then ( card X) = ( card ( Seg ( len q))) by A9, CARD_1: 5

      .= ( len q) by FINSEQ_1: 57;

      

      then

       A10: ( len q) = ( card ( Seg ( len p))) by FINSEQ_1:def 3

      .= ( len p) by FINSEQ_1: 57;

      now

        per cases ;

          suppose B = {} ;

          hence thesis;

        end;

          suppose

           A11: B <> {} ;

          then ( rng p) = ( dom f) by A4, FUNCT_2:def 1;

          

          then

           A12: ( rng (f * p)) = B by a2, RELAT_1: 28

          .= ( dom (q " )) by A7, A8, FUNCT_1: 33;

          ( dom (q " )) = ( rng q) by A8, FUNCT_1: 33;

          then ( rng f) c= ( dom (q " )) by A7, RELAT_1:def 19;

          then ( dom ((q " ) * f)) = ( dom f) by RELAT_1: 27;

          then ( rng p) = ( dom ((q " ) * f)) by A4, A11, FUNCT_2:def 1;

          

          then

           A13: ( dom (((q " ) * f) * p)) = ( dom p) by RELAT_1: 27

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

          then

          reconsider g = (((q " ) * f) * p) as FinSequence by FINSEQ_1:def 2;

          g = ((q " ) * (f * p)) by RELAT_1: 36;

          

          then ( rng g) = ( rng (q " )) by A12, RELAT_1: 28

          .= ( dom q) by A8, FUNCT_1: 33

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

          then

           A14: g is one-to-one by A10, A13, Th60;

          (q * g) = (q * ((q " ) * (f * p))) by RELAT_1: 36

          .= ((q * (q " )) * (f * p)) by RELAT_1: 36

          .= (( id ( rng q)) * (f * p)) by A8, FUNCT_1: 39

          .= ((( id ( rng q)) * f) * p) by RELAT_1: 36

          .= (f * p) by a2, A7, RELAT_1: 54;

          

          then ((q * g) * (p " )) = (f * (p * (p " ))) by RELAT_1: 36

          .= (f * ( id ( rng p))) by A5, FUNCT_1: 39

          .= (f * ( id ( dom f))) by A4, A11, FUNCT_2:def 1

          .= f by RELAT_1: 52;

          hence thesis by A5, A8, A14;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINSEQ_4:62

    

     Th62: p is one-to-one iff ( card ( rng p)) = ( len p)

    proof

      thus p is one-to-one implies ( card ( rng p)) = ( len p)

      proof

        assume p is one-to-one;

        then (( dom p),(p .: ( dom p))) are_equipotent by CARD_1: 33;

        then (( dom p),( rng p)) are_equipotent by RELAT_1: 113;

        then (( Seg ( len p)),( rng p)) are_equipotent by FINSEQ_1:def 3;

        then ( card ( Seg ( len p))) = ( card ( rng p)) by CARD_1: 5;

        hence thesis by FINSEQ_1: 57;

      end;

      reconsider f = p as Function of ( dom p), ( rng p) by FUNCT_2: 1;

      reconsider B = ( dom p) as finite set;

      assume ( card ( rng p)) = ( len p);

      then ( card ( rng p)) = ( card ( Seg ( len p))) by FINSEQ_1: 57;

      then

       A1: ( card ( rng p)) = ( card B) by FINSEQ_1:def 3;

      f is onto by FUNCT_2:def 3;

      hence thesis by Lm1, A1;

    end;

    reserve f for Function of A, B;

    

     Lemacik: for A,B be finite set, f be Function of A, B st ( card A) = ( card B) & f is one-to-one holds f is onto

    proof

      let A,B be finite set;

      let f be Function of A, B;

      assume that

       A1: ( card A) = ( card B) and

       A2: f is one-to-one;

      

       A3: (A,B) are_equipotent by A1, CARD_1: 5;

      consider p such that

       A4: ( rng p) = A and

       A5: p is one-to-one by Th58;

      (( dom p),(p .: ( dom p))) are_equipotent by A5, CARD_1: 33;

      then (( dom p),A) are_equipotent by A4, RELAT_1: 113;

      then

       A6: (( dom p),B) are_equipotent by A3, WELLORD2: 15;

      consider q such that

       A7: ( rng q) = B and

       A8: q is one-to-one by Th58;

      

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

      (( dom q),(q .: ( dom q))) are_equipotent by A8, CARD_1: 33;

      then (( dom q),B) are_equipotent by A7, RELAT_1: 113;

      then (( dom p),( dom q)) are_equipotent by A6, WELLORD2: 15;

      

      then ( card ( dom p)) = ( card ( Seg ( len q))) by A9, CARD_1: 5

      .= ( len q) by FINSEQ_1: 57;

      

      then

       A10: ( len q) = ( card ( Seg ( len p))) by FINSEQ_1:def 3

      .= ( len p) by FINSEQ_1: 57;

      per cases ;

        suppose B = {} ;

        then ( rng f) = B;

        hence thesis by FUNCT_2:def 3;

      end;

        suppose

         A11: B <> {} ;

        ( dom (q " )) = ( rng q) by A8, FUNCT_1: 33;

        then ( rng f) c= ( dom (q " )) by A7, RELAT_1:def 19;

        then ( dom ((q " ) * f)) = ( dom f) by RELAT_1: 27;

        then ( rng p) = ( dom ((q " ) * f)) by A4, A11, FUNCT_2:def 1;

        

        then

         A12: ( dom (((q " ) * f) * p)) = ( dom p) by RELAT_1: 27

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

        then

        reconsider g = (((q " ) * f) * p) as FinSequence by FINSEQ_1:def 2;

        g = ((q " ) * (f * p)) by RELAT_1: 36;

        then ( rng g) c= ( rng (q " )) by RELAT_1: 26;

        then ( rng g) c= ( dom q) by A8, FUNCT_1: 33;

        then ( rng g) c= ( dom g) by A10, A12, FINSEQ_1:def 3;

        then ( rng g) = ( dom g) by A2, A5, A8, Th59;

        then ( rng g) = ( dom q) by A10, A12, FINSEQ_1:def 3;

        then

         A13: ( rng (q * g)) = B by A7, RELAT_1: 28;

        

         A14: ( rng f) c= ( rng q) by A7, RELAT_1:def 19;

        

         A15: ( rng p) = ( dom f) by A4, A11, FUNCT_2:def 1;

        (q * g) = (q * ((q " ) * (f * p))) by RELAT_1: 36

        .= ((q * (q " )) * (f * p)) by RELAT_1: 36

        .= (( id ( rng q)) * (f * p)) by A8, FUNCT_1: 39

        .= ((( id ( rng q)) * f) * p) by RELAT_1: 36

        .= (f * p) by A14, RELAT_1: 53;

        then ( rng f) = B by A13, A15, RELAT_1: 28;

        hence thesis by FUNCT_2:def 3;

      end;

    end;

    theorem :: FINSEQ_4:63

    for A,B be finite set, f be Function of A, B st ( card A) = ( card B) holds f is one-to-one iff f is onto by Lemacik, Lm1;

    ::$Canceled

    ::$Notion-Name

    ::$Notion-Name

    theorem :: FINSEQ_4:65

    ( card B) in ( card A) & B <> {} implies ex x, y st x in A & y in A & x <> y & (f . x) = (f . y)

    proof

      assume that

       A1: ( card B) in ( card A) and

       A2: B <> {} and

       A3: for x, y st x in A & y in A & x <> y holds (f . x) <> (f . y);

      

       A4: ( dom f) = A by A2, FUNCT_2:def 1;

      then for x,y be object holds x in ( dom f) & y in ( dom f) & (f . x) = (f . y) implies x = y by A3;

      then f is one-to-one;

      then (( dom f),(f .: ( dom f))) are_equipotent by CARD_1: 33;

      then (( dom f),( rng f)) are_equipotent by RELAT_1: 113;

      then

       A5: ( card A) = ( card ( rng f)) by A4, CARD_1: 5;

      ( rng f) c= B by RELAT_1:def 19;

      then ( card A) c= ( card B) by A5, CARD_1: 11;

      hence contradiction by A1, CARD_1: 4;

    end;

    theorem :: FINSEQ_4:66

    

     Th66: ( card A) in ( card B) implies ex x st x in B & for y st y in A holds (f . y) <> x

    proof

      assume that

       A1: ( card A) in ( card B) and

       A2: for x st x in B holds ex y st y in A & (f . y) = x;

      

       A3: ( dom f) = A by A1, CARD_1: 27, FUNCT_2:def 1;

      ( rng f) = B

      proof

        thus ( rng f) c= B by RELAT_1:def 19;

        let x be object;

        assume x in B;

        then ex y st y in A & (f . y) = x by A2;

        hence thesis by A3, FUNCT_1:def 3;

      end;

      then ( card B) c= ( card A) by A3, CARD_1: 12;

      hence thesis by A1, CARD_1: 4;

    end;

    begin

    theorem :: FINSEQ_4:67

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

    proof

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

      ( len (f ^ <*p*>)) = (( len f) + ( len <*p*>)) by FINSEQ_1: 22;

      then 1 <= (( len f) + 1) & (( len f) + 1) <= ( len (f ^ <*p*>)) by FINSEQ_1: 39, NAT_1: 11;

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

      

      hence ((f ^ <*p*>) /. (( len f) + 1)) = ((f ^ <*p*>) . (( len f) + 1)) by PARTFUN1:def 6

      .= p by FINSEQ_1: 42;

    end;

    theorem :: FINSEQ_4:68

    for E be non empty set, p,q be FinSequence of E st k in ( dom p) holds ((p ^ q) /. k) = (p /. k)

    proof

      let E be non empty set, p,q be FinSequence of E;

      assume

       A1: k in ( dom p);

      then k in ( dom (p ^ q)) by FINSEQ_3: 22;

      

      hence ((p ^ q) /. k) = ((p ^ q) . k) by PARTFUN1:def 6

      .= (p . k) by A1, FINSEQ_1:def 7

      .= (p /. k) by A1, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:69

    for E be non empty set, p,q be FinSequence of E st k in ( dom q) holds ((p ^ q) /. (( len p) + k)) = (q /. k)

    proof

      let E be non empty set, p,q be FinSequence of E;

      assume

       A1: k in ( dom q);

      then (( len p) + k) in ( dom (p ^ q)) by FINSEQ_1: 28;

      

      hence ((p ^ q) /. (( len p) + k)) = ((p ^ q) . (( len p) + k)) by PARTFUN1:def 6

      .= (q . k) by A1, FINSEQ_1:def 7

      .= (q /. k) by A1, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:70

    for m be Nat holds for D be set, p be FinSequence of D st a in ( dom (p | m)) holds ((p | m) qua FinSequence of D /. a) = (p /. a)

    proof

      let m be Nat;

      let D be set, p be FinSequence of D;

      assume

       A1: a in ( dom (p | m));

      then a in (( dom p) /\ ( Seg m)) by RELAT_1: 61;

      then

       A2: a in ( dom p) by XBOOLE_0:def 4;

      

      thus ((p | m) /. a) = ((p | ( Seg m)) . a) by A1, PARTFUN1:def 6

      .= (p . a) by A1, FUNCT_1: 47

      .= (p /. a) by A2, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:71

    

     Th71: for D be set, f be FinSequence of D, n, m st n in ( dom f) & m in ( Seg n) holds m in ( dom f) & ((f | n) /. m) = (f /. m)

    proof

      let D be set, f be FinSequence of D, n, m;

      assume that

       A1: n in ( dom f) and

       A2: m in ( Seg n);

      ( dom f) = ( Seg ( len f)) & n <= ( len f) by A1, FINSEQ_1:def 3, FINSEQ_3: 25;

      then

       A3: ( Seg n) c= ( dom f) by FINSEQ_1: 5;

      hence m in ( dom f) by A2;

      

       A4: ( Seg n) = (( dom f) /\ ( Seg n)) by A3, XBOOLE_1: 28

      .= ( dom (f | n)) by RELAT_1: 61;

      

      hence ((f | n) /. m) = ((f | n) . m) by A2, PARTFUN1:def 6

      .= (f . m) by A2, A4, FUNCT_1: 47

      .= (f /. m) by A2, A3, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:72

    for X be finite set st n <= ( card X) holds ex A be finite Subset of X st ( card A) = n

    proof

      let X be finite set such that

       A1: n <= ( card X);

      consider p be FinSequence such that

       A2: ( rng p) = X and

       A3: p is one-to-one by Th58;

      reconsider q = (p | ( Seg n)) as FinSequence by FINSEQ_1: 15;

      n <= ( len p) by A1, A2, A3, Th62;

      then

       A4: ( len q) = n by FINSEQ_1: 17;

      reconsider A = ( rng q) as Subset of X by A2, RELAT_1: 70;

      q is one-to-one by A3, FUNCT_1: 52;

      then ( card A) = n by A4, Th62;

      hence thesis;

    end;

    reserve f for Function;

    theorem :: FINSEQ_4:73

    f is one-to-one & x in ( rng f) implies ( card ( Coim (f,x))) = 1 by Th8, Def2;

    definition

      let x1,x2,x3,x4 be object;

      :: FINSEQ_4:def7

      func <*x1,x2,x3,x4*> -> set equals ( <*x1, x2, x3*> ^ <*x4*>);

      correctness ;

      let x5 be object;

      :: FINSEQ_4:def8

      func <*x1,x2,x3,x4,x5*> -> set equals ( <*x1, x2, x3*> ^ <*x4, x5*>);

      correctness ;

    end

    registration

      let x1,x2,x3,x4 be object;

      cluster <*x1, x2, x3, x4*> -> non empty Function-like Relation-like;

      coherence ;

      let x5 be object;

      cluster <*x1, x2, x3, x4, x5*> -> non empty Function-like Relation-like;

      coherence ;

    end

    registration

      let x1,x2,x3,x4 be object;

      cluster <*x1, x2, x3, x4*> -> FinSequence-like;

      coherence ;

      let x5 be object;

      cluster <*x1, x2, x3, x4, x5*> -> FinSequence-like;

      coherence ;

    end

    definition

      let D be non empty set, x1,x2,x3,x4 be Element of D;

      :: original: <*

      redefine

      func <*x1,x2,x3,x4*> -> FinSequence of D ;

      coherence

      proof

         <*x1, x2, x3, x4*> = ( <*x1, x2, x3*> ^ <*x4*>);

        hence thesis;

      end;

    end

    definition

      let D be non empty set, x1,x2,x3,x4,x5 be Element of D;

      :: original: <*

      redefine

      func <*x1,x2,x3,x4,x5*> -> FinSequence of D ;

      coherence

      proof

         <*x1, x2, x3, x4, x5*> = ( <*x1, x2, x3*> ^ <*x4, x5*>);

        hence thesis;

      end;

    end

    reserve x1,x2,x3,x4,x5 for object;

    theorem :: FINSEQ_4:74

    

     Th74: <*x1, x2, x3, x4*> = ( <*x1, x2, x3*> ^ <*x4*>) & <*x1, x2, x3, x4*> = ( <*x1, x2*> ^ <*x3, x4*>) & <*x1, x2, x3, x4*> = ( <*x1*> ^ <*x2, x3, x4*>) & <*x1, x2, x3, x4*> = ((( <*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>)

    proof

      thus <*x1, x2, x3, x4*> = ( <*x1, x2, x3*> ^ <*x4*>);

      thus <*x1, x2, x3, x4*> = ( <*x1, x2*> ^ <*x3, x4*>) by FINSEQ_1: 32;

      

      hence <*x1, x2, x3, x4*> = ( <*x1*> ^ ( <*x2*> ^ <*x3, x4*>)) by FINSEQ_1: 32

      .= ( <*x1*> ^ <*x2, x3, x4*>) by FINSEQ_1: 43;

      thus thesis;

    end;

    theorem :: FINSEQ_4:75

    

     Th75: <*x1, x2, x3, x4, x5*> = ( <*x1, x2, x3*> ^ <*x4, x5*>) & <*x1, x2, x3, x4, x5*> = ( <*x1, x2, x3, x4*> ^ <*x5*>) & <*x1, x2, x3, x4, x5*> = (((( <*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) & <*x1, x2, x3, x4, x5*> = ( <*x1, x2*> ^ <*x3, x4, x5*>) & <*x1, x2, x3, x4, x5*> = ( <*x1*> ^ <*x2, x3, x4, x5*>)

    proof

      thus <*x1, x2, x3, x4, x5*> = ( <*x1, x2, x3*> ^ <*x4, x5*>);

      thus

       A1: <*x1, x2, x3, x4, x5*> = ( <*x1, x2, x3, x4*> ^ <*x5*>) by FINSEQ_1: 32;

      thus <*x1, x2, x3, x4, x5*> = (((( <*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) by FINSEQ_1: 32;

      

      thus <*x1, x2, x3, x4, x5*> = (( <*x1, x2*> ^ ( <*x3*> ^ <*x4*>)) ^ <*x5*>) by A1, FINSEQ_1: 32

      .= ( <*x1, x2*> ^ <*x3, x4, x5*>) by FINSEQ_1: 32;

      

      hence <*x1, x2, x3, x4, x5*> = ( <*x1*> ^ ( <*x2*> ^ <*x3, x4, x5*>)) by FINSEQ_1: 32

      .= ( <*x1*> ^ <*x2, x3, x4, x5*>) by Th74;

    end;

    reserve p for FinSequence;

    theorem :: FINSEQ_4:76

    

     Th76: p = <*x1, x2, x3, x4*> iff ( len p) = 4 & (p . 1) = x1 & (p . 2) = x2 & (p . 3) = x3 & (p . 4) = x4

    proof

      thus p = <*x1, x2, x3, x4*> implies ( len p) = 4 & (p . 1) = x1 & (p . 2) = x2 & (p . 3) = x3 & (p . 4) = x4

      proof

        set p3 = <*x1, x2, x3*>;

        assume

         A1: p = <*x1, x2, x3, x4*>;

        

        hence ( len p) = (( len <*x1, x2, x3*>) + ( len <*x4*>)) by FINSEQ_1: 22

        .= (3 + ( len <*x4*>)) by FINSEQ_1: 45

        .= (3 + 1) by FINSEQ_1: 40

        .= 4;

        

         A2: ( dom p3) = {1, 2, 3} by FINSEQ_1: 89, FINSEQ_3: 1;

        then 1 in ( dom p3) by ENUMSET1:def 1;

        

        hence (p . 1) = (p3 . 1) by A1, FINSEQ_1:def 7

        .= x1 by FINSEQ_1: 45;

        2 in ( dom p3) by A2, ENUMSET1:def 1;

        

        hence (p . 2) = (p3 . 2) by A1, FINSEQ_1:def 7

        .= x2 by FINSEQ_1: 45;

        3 in ( dom p3) by A2, ENUMSET1:def 1;

        

        hence (p . 3) = (p3 . 3) by A1, FINSEQ_1:def 7

        .= x3 by FINSEQ_1: 45;

        1 in {1} by TARSKI:def 1;

        then

         A3: 1 in ( dom <*x4*>) by FINSEQ_1: 2, FINSEQ_1:def 8;

        

        thus (p . 4) = ((p3 ^ <*x4*>) . (3 + 1)) by A1

        .= ((p3 ^ <*x4*>) . (( len p3) + 1)) by FINSEQ_1: 45

        .= ( <*x4*> . 1) by A3, FINSEQ_1:def 7

        .= x4 by FINSEQ_1:def 8;

      end;

      assume that

       A4: ( len p) = 4 and

       A5: (p . 1) = x1 and

       A6: (p . 2) = x2 and

       A7: (p . 3) = x3 and

       A8: (p . 4) = x4;

      

       A9: for k be Nat st k in ( dom <*x1, x2, x3*>) holds (p . k) = ( <*x1, x2, x3*> . k)

      proof

        

         A10: ( len <*x1, x2, x3*>) = 3 by FINSEQ_1: 45;

        let k be Nat;

        assume k in ( dom <*x1, x2, x3*>);

        then

         A11: k in {1, 2, 3} by A10, FINSEQ_1:def 3, FINSEQ_3: 1;

        per cases by A11, ENUMSET1:def 1;

          suppose k = 1;

          hence thesis by A5, FINSEQ_1: 45;

        end;

          suppose k = 2;

          hence thesis by A6, FINSEQ_1: 45;

        end;

          suppose k = 3;

          hence thesis by A7, FINSEQ_1: 45;

        end;

      end;

      

       A12: for k be Nat st k in ( dom <*x4*>) holds (p . (( len <*x1, x2, x3*>) + k)) = ( <*x4*> . k)

      proof

        let k be Nat;

        assume k in ( dom <*x4*>);

        then k in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        then

         A13: k = 1 by TARSKI:def 1;

        

        hence (p . (( len <*x1, x2, x3*>) + k)) = (p . (3 + 1)) by FINSEQ_1: 45

        .= ( <*x4*> . k) by A8, A13, FINSEQ_1:def 8;

      end;

      ( dom p) = ( Seg (3 + 1)) by A4, FINSEQ_1:def 3

      .= ( Seg (( len <*x1, x2, x3*>) + 1)) by FINSEQ_1: 45

      .= ( Seg (( len <*x1, x2, x3*>) + ( len <*x4*>))) by FINSEQ_1: 39;

      hence thesis by A9, A12, FINSEQ_1:def 7;

    end;

    ::$Canceled

    theorem :: FINSEQ_4:78

    

     Th77: p = <*x1, x2, x3, x4, x5*> iff ( len p) = 5 & (p . 1) = x1 & (p . 2) = x2 & (p . 3) = x3 & (p . 4) = x4 & (p . 5) = x5

    proof

      set p4 = <*x1, x2, x3, x4*>;

      thus p = <*x1, x2, x3, x4, x5*> implies ( len p) = 5 & (p . 1) = x1 & (p . 2) = x2 & (p . 3) = x3 & (p . 4) = x4 & (p . 5) = x5

      proof

        set p4 = <*x1, x2, x3, x4*>;

        1 in {1} by TARSKI:def 1;

        then

         A1: 1 in ( dom <*x5*>) by FINSEQ_1: 2, FINSEQ_1:def 8;

        assume

         A2: p = <*x1, x2, x3, x4, x5*>;

        then

         A3: p = (p4 ^ <*x5*>) by Th75;

        

        thus ( len p) = ( len ( <*x1, x2, x3, x4*> ^ <*x5*>)) by A2, Th75

        .= (( len <*x1, x2, x3, x4*>) + ( len <*x5*>)) by FINSEQ_1: 22

        .= (4 + ( len <*x5*>)) by Th76

        .= (4 + 1) by FINSEQ_1: 40

        .= 5;

        

         A4: ( dom p4) = {1, 2, 3, 4} by FINSEQ_1: 89, FINSEQ_3: 2;

        then 1 in ( dom p4) by ENUMSET1:def 2;

        

        hence (p . 1) = (p4 . 1) by A3, FINSEQ_1:def 7

        .= x1 by Th76;

        2 in ( dom p4) by A4, ENUMSET1:def 2;

        

        hence (p . 2) = (p4 . 2) by A3, FINSEQ_1:def 7

        .= x2 by Th76;

        3 in ( dom p4) by A4, ENUMSET1:def 2;

        

        hence (p . 3) = (p4 . 3) by A3, FINSEQ_1:def 7

        .= x3 by Th76;

        4 in ( dom p4) by A4, ENUMSET1:def 2;

        

        hence (p . 4) = (p4 . 4) by A3, FINSEQ_1:def 7

        .= x4 by Th76;

        

        thus (p . 5) = ((p4 ^ <*x5*>) . (4 + 1)) by A2, Th75

        .= ((p4 ^ <*x5*>) . (( len p4) + 1)) by Th76

        .= ( <*x5*> . 1) by A1, FINSEQ_1:def 7

        .= x5 by FINSEQ_1:def 8;

      end;

      assume that

       A5: ( len p) = 5 and

       A6: (p . 1) = x1 and

       A7: (p . 2) = x2 and

       A8: (p . 3) = x3 and

       A9: (p . 4) = x4 and

       A10: (p . 5) = x5;

      

       A11: for k be Nat st k in ( dom p4) holds (p . k) = (p4 . k)

      proof

        

         A12: ( len p4) = 4 by Th76;

        let k be Nat;

        assume k in ( dom p4);

        then

         A13: k in {1, 2, 3, 4} by A12, FINSEQ_1:def 3, FINSEQ_3: 2;

        per cases by A13, ENUMSET1:def 2;

          suppose k = 1;

          hence thesis by A6, Th76;

        end;

          suppose k = 2;

          hence thesis by A7, Th76;

        end;

          suppose k = 3;

          hence thesis by A8, Th76;

        end;

          suppose k = 4;

          hence thesis by A9, Th76;

        end;

      end;

      

       A14: for k be Nat st k in ( dom <*x5*>) holds (p . (( len p4) + k)) = ( <*x5*> . k)

      proof

        let k be Nat;

        assume k in ( dom <*x5*>);

        then k in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        then

         A15: k = 1 by TARSKI:def 1;

        

        hence (p . (( len p4) + k)) = (p . (4 + 1)) by Th76

        .= ( <*x5*> . k) by A10, A15, FINSEQ_1:def 8;

      end;

      ( dom p) = ( Seg (4 + 1)) by A5, FINSEQ_1:def 3

      .= ( Seg (( len p4) + 1)) by Th76

      .= ( Seg (( len p4) + ( len <*x5*>))) by FINSEQ_1: 39;

      

      hence p = (p4 ^ <*x5*>) by A11, A14, FINSEQ_1:def 7

      .= <*x1, x2, x3, x4, x5*> by Th75;

    end;

    reserve ND for non empty set;

    reserve y1,y2,y3,y4,y5 for Element of ND;

    ::$Canceled

    theorem :: FINSEQ_4:80

    ( <*y1, y2, y3, y4*> /. 1) = y1 & ( <*y1, y2, y3, y4*> /. 2) = y2 & ( <*y1, y2, y3, y4*> /. 3) = y3 & ( <*y1, y2, y3, y4*> /. 4) = y4

    proof

      set s = <*y1, y2, y3, y4*>;

      

       A1: 2 in {1, 2, 3, 4} & 3 in {1, 2, 3, 4} by FINSEQ_3: 2;

      

       A2: (s . 2) = y2 & (s . 3) = y3 by Th76;

      

       A3: 4 in {1, 2, 3, 4} by FINSEQ_3: 2;

      

       A4: (s . 4) = y4 & 1 in {1, 2, 3, 4} by Th76, FINSEQ_3: 2;

      ( dom s) = {1, 2, 3, 4} & (s . 1) = y1 by Th76, FINSEQ_1: 89, FINSEQ_3: 2;

      hence thesis by A2, A4, A1, A3, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:81

    ( <*y1, y2, y3, y4, y5*> /. 1) = y1 & ( <*y1, y2, y3, y4, y5*> /. 2) = y2 & ( <*y1, y2, y3, y4, y5*> /. 3) = y3 & ( <*y1, y2, y3, y4, y5*> /. 4) = y4 & ( <*y1, y2, y3, y4, y5*> /. 5) = y5

    proof

      set s = <*y1, y2, y3, y4, y5*>, i5 = {1, 2, 3, 4, 5};

      

       A1: 1 in i5 & 2 in i5 by FINSEQ_3: 3;

      

       A2: 3 in i5 & 4 in i5 by FINSEQ_3: 3;

      

       A3: (s . 4) = y4 & (s . 5) = y5 by Th77;

      

       A4: (s . 2) = y2 & (s . 3) = y3 by Th77;

      

       A5: 5 in i5 by FINSEQ_3: 3;

      ( dom s) = i5 & (s . 1) = y1 by Th77, FINSEQ_1: 89, FINSEQ_3: 3;

      hence thesis by A4, A3, A1, A2, A5, PARTFUN1:def 6;

    end;

    scheme :: FINSEQ_4:sch1

    Sch1 { D() -> non empty set , N() -> Nat , P[ object, object] } :

ex f be FinSequence of D() st ( len f) = N() & for n st n in ( Seg N()) holds P[n, (f /. n)]

      provided

       A1: for n st n in ( Seg N()) holds ex d be Element of D() st P[n, d];

      defpred P1[ object, object] means P[$1, $2] & $2 in D();

      reconsider X = D() as set;

       A2:

      now

        let x be object;

        assume

         A3: x in ( Seg N());

        then

        reconsider x9 = x as Element of NAT ;

        consider d be Element of D() such that

         A4: P[x9, d] by A1, A3;

        reconsider y = d as object;

        take y;

        thus y in X & P1[x, y] by A4;

      end;

      consider f be Function such that

       A5: ( dom f) = ( Seg N()) & ( rng f) c= X & for x be object st x in ( Seg N()) holds P1[x, (f . x)] from FUNCT_1:sch 6( A2);

      reconsider f as FinSequence by A5, FINSEQ_1:def 2;

      reconsider f as FinSequence of D() by A5, FINSEQ_1:def 4;

      take f;

      N() in NAT by ORDINAL1:def 12;

      hence ( len f) = N() by A5, FINSEQ_1:def 3;

      let n;

      assume

       A6: n in ( Seg N());

      then P[n, (f . n)] by A5;

      hence thesis by A5, A6, PARTFUN1:def 6;

    end;

    theorem :: FINSEQ_4:82

    

     Th80: for D be non empty set, p,q be FinSequence of D st p c= q holds ex p9 be FinSequence of D st (p ^ p9) = q

    proof

      let D be non empty set, p,q be FinSequence of D;

      assume

       A1: p c= q;

      ( dom p) = ( Seg ( len p)) & ( dom q) = ( Seg ( len q)) by FINSEQ_1:def 3;

      then ( Seg ( len p)) c= ( Seg ( len q)) by A1, GRFUNC_1: 2;

      then ( len p) <= ( len q) by FINSEQ_1: 5;

      then

      reconsider N = (( len q) - ( len p)) as Element of NAT by INT_1: 3, XREAL_1: 48;

      defpred P[ Nat, set] means (q /. (( len p) + $1)) = $2;

      

       A2: for n be Nat st n in ( Seg N) holds ex d be Element of D st P[n, d];

      consider f be FinSequence of D such that

       A3: ( len f) = N and

       A4: for n be Nat st n in ( Seg N) holds P[n, (f /. n)] from Sch1( A2);

      take f;

      

       A5: ( len (p ^ f)) = (( len p) + N) by A3, FINSEQ_1: 22

      .= ( len q);

      now

        let k be Nat;

        assume that

         A6: 1 <= k and

         A7: k <= ( len (p ^ f));

        k in ( Seg ( len q)) by A5, A6, A7;

        then

         A8: k in ( dom q) by FINSEQ_1:def 3;

        per cases ;

          suppose k <= ( len p);

          then k in ( Seg ( len p)) by A6;

          then

           A9: k in ( dom p) by FINSEQ_1:def 3;

          

          hence ((p ^ f) . k) = (p . k) by FINSEQ_1:def 7

          .= (q . k) by A1, A9, GRFUNC_1: 2;

        end;

          suppose

           A10: ( len p) < k;

          then (k - ( len p)) > 0 by XREAL_1: 50;

          then

          reconsider kk = (k - ( len p)) as Element of NAT by INT_1: 3;

          k <= (( len p) + ( len f)) by A7, FINSEQ_1: 22;

          then

           A11: kk <= ((( len p) + ( len f)) - ( len p)) by XREAL_1: 9;

          (k - ( len p)) >= ( 0 + 1) by A10, INT_1: 7, XREAL_1: 50;

          then

           A12: kk in ( Seg ( len f)) by A11;

          then

           A13: kk in ( dom f) by FINSEQ_1:def 3;

          

          thus ((p ^ f) . k) = (f . kk) by A7, A10, FINSEQ_1: 24

          .= (f /. kk) by A13, PARTFUN1:def 6

          .= (q /. (( len p) + kk)) by A3, A4, A12

          .= (q . k) by A8, PARTFUN1:def 6;

        end;

      end;

      hence thesis by A5;

    end;

    theorem :: FINSEQ_4:83

    for D be non empty set, p,q be FinSequence of D, i be Element of NAT st p c= q & 1 <= i & i <= ( len p) holds (q . i) = (p . i)

    proof

      let D be non empty set, p,q be FinSequence of D, i be Element of NAT ;

      assume p c= q;

      then

       A1: ex p9 be FinSequence of D st (p ^ p9) = q by Th80;

      assume 1 <= i & i <= ( len p);

      hence thesis by A1, FINSEQ_1: 64;

    end;

    scheme :: FINSEQ_4:sch2

    PiLambdaD { D() -> non empty set , l() -> Nat , F( set) -> Element of D() } :

ex g be FinSequence of D() st ( len g) = l() & for n be Nat st n in ( dom g) holds (g /. n) = F(n);

      consider g be FinSequence of D() such that

       A1: ( len g) = l() & for n be Nat st n in ( dom g) holds (g . n) = F(n) from FINSEQ_2:sch 1;

      take g;

      thus ( len g) = l() by A1;

      let n be Nat;

      assume

       A2: n in ( dom g);

      then (g . n) = F(n) by A1;

      hence thesis by A2, PARTFUN1:def 6;

    end;

    registration

      let x1,x2,x3,x4 be object;

      cluster <*x1, x2, x3, x4*> -> 4 -element;

      coherence ;

      let x5 be object;

      cluster <*x1, x2, x3, x4, x5*> -> 5 -element;

      coherence ;

    end

    begin

    theorem :: FINSEQ_4:84

    for m,n be Nat holds m < n implies ex p be Element of NAT st n = (m + p) & 1 <= p

    proof

      let m,n be Nat;

      assume

       A1: m < n;

      then

      consider p be Nat such that

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

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

      take p;

      thus n = (m + p) by A2;

      assume p < 1;

      then p < ( 0 + 1);

      then p = 0 by NAT_1: 13;

      hence contradiction by A1, A2;

    end;

    theorem :: FINSEQ_4:85

    for S be set, D1,D2 be non empty set, f1 be Function of S, D1, f2 be Function of D1, D2 holds f1 is bijective & f2 is bijective implies (f2 * f1) is bijective

    proof

      let S be set, D1,D2 be non empty set, f1 be Function of S, D1, f2 be Function of D1, D2;

      set f3 = (f2 * f1);

      

       A1: ( dom f2) = D1 by FUNCT_2:def 1;

      assume

       A2: f1 is bijective & f2 is bijective;

      then ( rng f2) = D2 & ( rng f1) = D1 by FUNCT_2:def 3;

      then ( rng f3) = D2 by A1, RELAT_1: 28;

      then f3 is one-to-one onto by A2, FUNCT_2:def 3;

      hence thesis;

    end;

    theorem :: FINSEQ_4:86

    for Y be set, E1,E2 be Equivalence_Relation of Y st ( Class E1) = ( Class E2) holds E1 = E2

    proof

      let Y be set, E1,E2 be Equivalence_Relation of Y such that

       A1: ( Class E1) = ( Class E2);

      now

        let x be object;

        hereby

          assume

           A2: x in E1;

          then

          consider a,b be object such that

           A3: x = [a, b] and

           A4: a in Y and

           A5: b in Y by RELSET_1: 2;

          reconsider a, b as Element of Y by A4, A5;

          ( Class (E1,b)) in ( Class E2) by A1, A4, EQREL_1:def 3;

          then

          consider c be object such that c in Y and

           A6: ( Class (E1,b)) = ( Class (E2,c)) by EQREL_1:def 3;

          b in ( Class (E1,b)) by A4, EQREL_1: 20;

          then [b, c] in E2 by A6, EQREL_1: 19;

          then

           A7: [c, b] in E2 by EQREL_1: 6;

          a in ( Class (E1,b)) by A2, A3, EQREL_1: 19;

          then [a, c] in E2 by A6, EQREL_1: 19;

          hence x in E2 by A3, A7, EQREL_1: 7;

        end;

        assume

         A8: x in E2;

        then

        consider a,b be object such that

         A9: x = [a, b] and

         A10: a in Y and

         A11: b in Y by RELSET_1: 2;

        reconsider a, b as Element of Y by A10, A11;

        ( Class (E2,b)) in ( Class E1) by A1, A10, EQREL_1:def 3;

        then

        consider c be object such that c in Y and

         A12: ( Class (E2,b)) = ( Class (E1,c)) by EQREL_1:def 3;

        b in ( Class (E2,b)) by A10, EQREL_1: 20;

        then [b, c] in E1 by A12, EQREL_1: 19;

        then

         A13: [c, b] in E1 by EQREL_1: 6;

        a in ( Class (E2,b)) by A8, A9, EQREL_1: 19;

        then [a, c] in E1 by A12, EQREL_1: 19;

        hence x in E1 by A9, A13, EQREL_1: 7;

      end;

      hence thesis;

    end;

    registration

      let Z be finite set;

      cluster -> finite for a_partition of Z;

      coherence ;

    end

    registration

      let X be non empty finite set;

      cluster non empty finite for a_partition of X;

      existence

      proof

        set p = the a_partition of X;

        take p;

        thus thesis;

      end;

    end

    theorem :: FINSEQ_4:87

    

     Th85: for X be non empty set, PX be a_partition of X holds for Pi be set st Pi in PX holds ex x be Element of X st x in Pi

    proof

      let X be non empty set, PX be a_partition of X;

      let Pi be set;

      assume Pi in PX;

      then

      reconsider Pi as Element of PX;

      set q = the Element of Pi;

      reconsider q as Element of X;

      take q;

      thus thesis;

    end;

    reserve X,A for non empty finite set,

PX for a_partition of X,

PA1,PA2 for a_partition of A;

    theorem :: FINSEQ_4:88

    ( card PX) <= ( card X)

    proof

      assume ( card PX) > ( card X);

      then ( card ( Segm ( card X))) in ( card ( Segm ( card PX))) by NAT_1: 41;

      then

      consider Pi be object such that

       A1: Pi in PX and

       A2: for x be object st x in X holds (( proj PX) . x) <> Pi by Th66;

      reconsider Pi as Element of PX by A1;

      consider q be Element of X such that

       A3: q in Pi by Th85;

      reconsider Pq = (( proj PX) . q) as Element of PX;

      

       A4: Pq = Pi or Pq misses Pi by EQREL_1:def 4;

      q in Pq by EQREL_1:def 9;

      hence contradiction by A2, A3, A4, XBOOLE_0: 3;

    end;

    theorem :: FINSEQ_4:89

    PA1 is_finer_than PA2 implies ( card PA2) <= ( card PA1)

    proof

      defpred P[ object, object] means ex A,B be set st A = $1 & B = $2 & A c= B;

      assume

       A1: PA1 is_finer_than PA2;

      

       A2: for e be object st e in PA1 holds ex u be object st u in PA2 & P[e, u]

      proof

        let e be object;

        reconsider ee = e as set by TARSKI: 1;

        assume e in PA1;

        then ee in PA1;

        then ex u be set st u in PA2 & ee c= u by SETFAM_1:def 2, A1;

        hence thesis;

      end;

      consider f be Function of PA1, PA2 such that

       A3: for e be object st e in PA1 holds P[e, (f . e)] from FUNCT_2:sch 1( A2);

      assume ( card PA1) < ( card PA2);

      then ( card ( Segm ( card PA1))) in ( card ( Segm ( card PA2))) by NAT_1: 41;

      then

      consider p2i be object such that

       A4: p2i in PA2 and

       A5: for x be object st x in PA1 holds (f . x) <> p2i by Th66;

      reconsider p2i as Element of PA2 by A4;

      consider q be Element of A such that

       A6: q in p2i by Th85;

      reconsider p2q = (f . (( proj PA1) . q)) as Element of PA2;

      

       A7: p2q = p2i or p2q misses p2i by EQREL_1:def 4;

       P[(( proj PA1) . q), (f . (( proj PA1) . q))] by A3;

      then q in (( proj PA1) . q) & (( proj PA1) . q) c= p2q by EQREL_1:def 9;

      hence contradiction by A5, A6, A7, XBOOLE_0: 3;

    end;

    theorem :: FINSEQ_4:90

    

     Th88: PA1 is_finer_than PA2 implies for p2 be Element of PA2 holds ex p1 be Element of PA1 st p1 c= p2

    proof

      assume

       A1: PA1 is_finer_than PA2;

      let p2 be Element of PA2;

      consider E1 be Equivalence_Relation of A such that

       A2: PA1 = ( Class E1) by EQREL_1: 34;

      reconsider p29 = p2 as Subset of A;

      consider E2 be Equivalence_Relation of A such that

       A3: PA2 = ( Class E2) by EQREL_1: 34;

      consider a be object such that

       A4: a in A and

       A5: p29 = ( Class (E2,a)) by A3, EQREL_1:def 3;

      

       A6: a in ( Class (E1,a)) by A4, EQREL_1: 20;

      reconsider E1a = ( Class (E1,a)) as Element of PA1 by A2, A4, EQREL_1:def 3;

      consider p22 be set such that

       A7: p22 in PA2 and

       A8: E1a c= p22 by A1, SETFAM_1:def 2;

      reconsider p229 = p22 as Subset of A by A7;

      take E1a;

      ex b be object st b in A & p229 = ( Class (E2,b)) by A3, A7, EQREL_1:def 3;

      hence thesis by A5, A8, A6, EQREL_1: 23;

    end;

    theorem :: FINSEQ_4:91

    PA1 is_finer_than PA2 & ( card PA1) = ( card PA2) implies PA1 = PA2

    proof

      defpred P[ object, object] means ex A,B be set st A = $1 & B = $2 & A c= B;

      assume that

       A1: PA1 is_finer_than PA2 and

       A2: ( card PA1) = ( card PA2);

      

       A3: for e be object st e in PA1 holds ex u be object st u in PA2 & P[e, u]

      proof

        let e be object;

        reconsider ee = e as set by TARSKI: 1;

        assume e in PA1;

        then ee in PA1;

        then ex u be set st u in PA2 & ee c= u by SETFAM_1:def 2, A1;

        hence thesis;

      end;

      consider f be Function of PA1, PA2 such that

       A4: for e be object st e in PA1 holds P[e, (f . e)] from FUNCT_2:sch 1( A3);

      

       A5: ( dom f) = PA1 by FUNCT_2:def 1;

      

       A6: PA2 c= ( rng f)

      proof

        let p2 be object;

        assume p2 in PA2;

        then

        reconsider p29 = p2 as Element of PA2;

        consider p1 be Element of PA1 such that

         A7: p1 c= p29 by A1, Th88;

        reconsider fp1 = (f . p1) as Subset of A by TARSKI:def 3;

         P[p1, (f . p1)] by A4;

        then

         A8: p1 c= (f . p1);

        p29 meets (f . p1)

        proof

          ex x be Element of A st x in p1 by Th85;

          hence thesis by A7, A8, XBOOLE_0: 3;

        end;

        then p29 = fp1 by EQREL_1:def 4;

        hence thesis by A5, FUNCT_1:def 3;

      end;

      ( rng f) c= PA2 by RELAT_1:def 19;

      then ( rng f) = PA2 by A6;

      then f is onto by FUNCT_2:def 3;

      then

       A9: f is one-to-one by A2, Lm1;

      

       A10: for x be Element of PA1 holds x = (f . x)

      proof

        let x be Element of PA1;

        reconsider fx = (f . x) as Subset of A by TARSKI:def 3;

        consider E1 be Equivalence_Relation of A such that

         A11: PA1 = ( Class E1) by EQREL_1: 34;

        assume x <> (f . x);

        then

        consider a be object such that

         A12: a in x & not a in (f . x) or a in (f . x) & not a in x by TARSKI: 2;

        

         A13: fx c= A;

        then

         A14: a in ( Class (E1,a)) by A12, EQREL_1: 20;

        reconsider CE1a = ( Class (E1,a)) as Element of PA1 by A13, A12, A11, EQREL_1:def 3;

        reconsider fCE1a = (f . CE1a) as Subset of A by TARSKI:def 3;

         P[x, (f . x)] by A4;

        then

         A15: x c= (f . x);

         P[CE1a, (f . CE1a)] by A4;

        then CE1a c= (f . CE1a);

        then fx meets fCE1a by A15, A12, A14, XBOOLE_0: 3;

        then fx = fCE1a by EQREL_1:def 4;

        hence contradiction by A5, A9, A15, A12, A14;

      end;

      now

        let x be object;

        hereby

          assume x in PA1;

          then

          reconsider x9 = x as Element of PA1;

          set fx = (f . x9);

          fx in PA2;

          hence x in PA2 by A10;

        end;

        assume x in PA2;

        then

        consider y be object such that

         A16: y in ( dom f) and

         A17: x = (f . y) by A6, FUNCT_1:def 3;

        reconsider y9 = y as Element of PA1 by A16, FUNCT_2:def 1;

        y9 = (f . y9) by A10;

        hence x in PA1 by A17;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let D be set, M be FinSequence of (D * );

      let k;

      cluster (M /. k) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let D be set, M be FinSequence of (D * );

      let k;

      cluster (M /. k) -> FinSequence-likeD -valued;

      coherence by FINSEQ_1:def 11;

    end

    reserve f for FinSequence of D;

    theorem :: FINSEQ_4:92

    m in ( dom f) implies (f /. 1) = ((f | m) /. 1)

    proof

      assume that

       A1: m in ( dom f);

      1 <= m by A1, FINSEQ_3: 25;

      then 1 in ( Seg m);

      hence thesis by A1, Th71;

    end;

    theorem :: FINSEQ_4:93

    m in ( dom f) implies (f /. m) = ((f | m) /. ( len (f | m)))

    proof

      assume that

       A1: m in ( dom f);

      m <= ( len f) by A1, FINSEQ_3: 25;

      then

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

      1 <= m by A1, FINSEQ_3: 25;

      then m in ( Seg m);

      hence thesis by A1, A2, Th71;

    end;