finseq_2.miz



    begin

    reserve i,j,k,l for natural Number;

    reserve A for set,

a,b,x,x1,x2,x3 for object;

    reserve D,D9,E for non empty set;

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

    reserve d9,d19,d29,d39 for Element of D9;

    reserve p,q,r for FinSequence;

    ::$Canceled

    theorem :: FINSEQ_2:2

    

     Th1: l = ( min (i,j)) implies (( Seg i) /\ ( Seg j)) = ( Seg l)

    proof

      i <= j or j <= i;

      then i <= j & (( Seg i) /\ ( Seg j)) = ( Seg i) or j <= i & (( Seg i) /\ ( Seg j)) = ( Seg j) by FINSEQ_1: 7;

      hence thesis by XXREAL_0:def 9;

    end;

    theorem :: FINSEQ_2:3

    

     Th2: i <= j implies ( max ( 0 ,(i - j))) = 0

    proof

      assume i <= j;

      then (i - i) <= (j - i) by XREAL_1: 9;

      then ( - (j - i)) <= ( - 0 );

      hence thesis by XXREAL_0:def 10;

    end;

    theorem :: FINSEQ_2:4

    

     Th3: j <= i implies ( max ( 0 ,(i - j))) = (i - j)

    proof

      assume j <= i;

      then (j - j) <= (i - j) by XREAL_1: 9;

      hence thesis by XXREAL_0:def 10;

    end;

    theorem :: FINSEQ_2:5

    ( max ( 0 ,(i - j))) is Element of NAT

    proof

      per cases ;

        suppose i <= j;

        hence thesis by Th2;

      end;

        suppose

         A1: j <= i;

        then (i - j) is Element of NAT by NAT_1: 21;

        hence thesis by A1, Th3;

      end;

    end;

    ::$Canceled

    theorem :: FINSEQ_2:7

    i in ( Seg (l + 1)) implies i in ( Seg l) or i = (l + 1)

    proof

      

       A0: i is Nat by TARSKI: 1;

      assume

       A1: i in ( Seg (l + 1));

      then i <= (l + 1) by FINSEQ_1: 1;

      then 1 <= i & i <= l or i = (l + 1) by A1, FINSEQ_1: 1, NAT_1: 8;

      hence thesis by A0;

    end;

    theorem :: FINSEQ_2:8

    i in ( Seg l) implies i in ( Seg (l + j))

    proof

      l <= (l + j) by NAT_1: 11;

      then ( Seg l) c= ( Seg (l + j)) by FINSEQ_1: 5;

      hence thesis;

    end;

    theorem :: FINSEQ_2:9

    ( len p) = ( len q) & (for j be Nat st j in ( dom p) holds (p . j) = (q . j)) implies p = q

    proof

      assume that

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

       A2: for j be Nat st j in ( dom p) holds (p . j) = (q . j);

      ( dom p) = ( Seg ( len p)) & ( dom q) = ( Seg ( len p)) by A1, FINSEQ_1:def 3;

      hence thesis by A2;

    end;

    theorem :: FINSEQ_2:10

    

     Th8: b in ( rng p) implies ex i be Nat st i in ( dom p) & (p . i) = b

    proof

      assume b in ( rng p);

      then ex a be object st a in ( dom p) & b = (p . a) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: FINSEQ_2:11

    

     Th9: for D be set holds for p be FinSequence of D st i in ( dom p) holds (p . i) in D

    proof

      let D be set;

      let p be FinSequence of D;

      assume i in ( dom p);

      then

       A1: (p . i) in ( rng p) by FUNCT_1:def 3;

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

      hence thesis by A1;

    end;

    theorem :: FINSEQ_2:12

    

     Th10: for D be set holds (for i be Nat st i in ( dom p) holds (p . i) in D) implies p is FinSequence of D

    proof

      let D be set;

      assume

       A1: for i be Nat st i in ( dom p) holds (p . i) in D;

      let b be object;

      assume b in ( rng p);

      then ex i be Nat st i in ( dom p) & (p . i) = b by Th8;

      hence thesis by A1;

    end;

    

     Lm1: ( rng <*x1, x2*>) = {x1, x2}

    proof

      

      thus ( rng <*x1, x2*>) = (( rng <*x1*>) \/ ( rng <*x2*>)) by FINSEQ_1: 31

      .= (( rng <*x1*>) \/ {x2}) by FINSEQ_1: 38

      .= ( {x1} \/ {x2}) by FINSEQ_1: 39

      .= {x1, x2} by ENUMSET1: 1;

    end;

    theorem :: FINSEQ_2:13

    

     Th11: <*d1, d2*> is FinSequence of D

    proof

      ( rng <*d1, d2*>) = {d1, d2} by Lm1;

      hence thesis by FINSEQ_1:def 4;

    end;

    

     Lm2: ( rng <*x1, x2, x3*>) = {x1, x2, x3}

    proof

      

      thus ( rng <*x1, x2, x3*>) = ( rng ( <*x1*> ^ <*x2, x3*>)) by FINSEQ_1: 43

      .= (( rng <*x1*>) \/ ( rng <*x2, x3*>)) by FINSEQ_1: 31

      .= ( {x1} \/ ( rng <*x2, x3*>)) by FINSEQ_1: 38

      .= ( {x1} \/ {x2, x3}) by Lm1

      .= {x1, x2, x3} by ENUMSET1: 2;

    end;

    theorem :: FINSEQ_2:14

    

     Th12: <*d1, d2, d3*> is FinSequence of D

    proof

      ( rng <*d1, d2, d3*>) = {d1, d2, d3} by Lm2;

      hence thesis by FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_2:15

    

     Th13: i in ( dom p) implies i in ( dom (p ^ q))

    proof

      

       A1: ( dom p) c= ( dom (p ^ q)) by FINSEQ_1: 26;

      assume i in ( dom p);

      hence thesis by A1;

    end;

    theorem :: FINSEQ_2:16

    

     Th14: ( len (p ^ <*a*>)) = (( len p) + 1)

    proof

      ( len (p ^ <*a*>)) = (( len p) + ( len <*a*>)) by FINSEQ_1: 22;

      hence thesis by FINSEQ_1: 39;

    end;

    theorem :: FINSEQ_2:17

    (p ^ <*a*>) = (q ^ <*b*>) implies p = q & a = b

    proof

      assume

       A1: (p ^ <*a*>) = (q ^ <*b*>);

      

       A2: ((p ^ <*a*>) . (( len p) + 1)) = a & ((q ^ <*b*>) . (( len q) + 1)) = b by FINSEQ_1: 42;

      ( len (p ^ <*a*>)) = (( len p) + 1) & ( len (q ^ <*b*>)) = (( len q) + 1) by Th14;

      hence thesis by A1, A2, FINSEQ_1: 33;

    end;

    theorem :: FINSEQ_2:18

    ( len p) = (i + 1) implies ex q, a st p = (q ^ <*a*>) by CARD_1: 27, FINSEQ_1: 46;

    theorem :: FINSEQ_2:19

    

     Th17: for p be FinSequence of A st ( len p) <> 0 holds ex q be FinSequence of A, d be Element of A st p = (q ^ <*d*>)

    proof

      let p be FinSequence of A;

      assume

       A1: ( len p) <> 0 ;

      then p <> {} ;

      then

      consider q be FinSequence, d be object such that

       A2: p = (q ^ <*d*>) by FINSEQ_1: 46;

      for i be Nat st i in ( dom q) holds (q . i) in A

      proof

        let i be Nat;

        assume i in ( dom q);

        then (p . i) = (q . i) & i in ( dom p) by A2, Th13, FINSEQ_1:def 7;

        hence thesis by Th9;

      end;

      then

       A3: q is FinSequence of A by Th10;

      ( len p) in ( Seg ( len p)) by A1, FINSEQ_1: 3;

      then

       A4: ( len p) in ( dom p) by FINSEQ_1:def 3;

      ( len p) = (( len q) + 1) by A2, Th14;

      then (p . ( len p)) = d by A2, FINSEQ_1: 42;

      then d is Element of A by A4, Th9;

      hence thesis by A2, A3;

    end;

    theorem :: FINSEQ_2:20

    

     Th18: q = (p | ( Seg i)) & ( len p) <= i implies p = q

    proof

      assume

       A1: q = (p | ( Seg i));

      assume ( len p) <= i;

      then ( Seg ( len p)) c= ( Seg i) by FINSEQ_1: 5;

      then ( dom p) c= ( Seg i) by FINSEQ_1:def 3;

      hence thesis by A1, RELAT_1: 68;

    end;

    theorem :: FINSEQ_2:21

    q = (p | ( Seg i)) implies ( len q) = ( min (i,( len p)))

    proof

      assume

       A1: q = (p | ( Seg i));

      now

        per cases ;

          case i <= ( len p);

          hence ( len q) = i by A1, FINSEQ_1: 17;

        end;

          case not i <= ( len p);

          hence ( len q) = ( len p) by A1, Th18;

        end;

      end;

      hence thesis by XXREAL_0:def 9;

    end;

    theorem :: FINSEQ_2:22

    

     Th20: ( len r) = (i + j) implies ex p, q st ( len p) = i & ( len q) = j & r = (p ^ q)

    proof

      assume

       A1: ( len r) = (i + j);

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

      reconsider p = (r | ( Seg z)) as FinSequence by FINSEQ_1: 15;

      consider q be FinSequence such that

       A2: r = (p ^ q) by FINSEQ_1: 80;

      take p, q;

      i <= ( len r) by A1, NAT_1: 11;

      hence ( len p) = i by FINSEQ_1: 17;

      then ( len (p ^ q)) = (i + ( len q)) by FINSEQ_1: 22;

      hence ( len q) = j by A1, A2;

      thus thesis by A2;

    end;

    theorem :: FINSEQ_2:23

    

     Th21: for r be FinSequence of D st ( len r) = (i + j) holds ex p,q be FinSequence of D st ( len p) = i & ( len q) = j & r = (p ^ q)

    proof

      let r be FinSequence of D;

      assume ( len r) = (i + j);

      then

      consider p,q be FinSequence such that

       A1: ( len p) = i & ( len q) = j and

       A2: r = (p ^ q) by Th20;

      p is FinSequence of D & q is FinSequence of D by A2, FINSEQ_1: 36;

      hence thesis by A1, A2;

    end;

    scheme :: FINSEQ_2:sch1

    SeqLambdaD { i() -> Nat , D() -> non empty set , F( set) -> Element of D() } :

ex z be FinSequence of D() st ( len z) = i() & for j be Nat st j in ( dom z) holds (z . j) = F(j);

      consider z be FinSequence such that

       A1: ( len z) = i() and

       A2: for i be Nat st i in ( dom z) holds (z . i) = F(i) from FINSEQ_1:sch 2;

      

       A3: ( Seg i()) = ( dom z) by A1, FINSEQ_1:def 3;

      for j be Nat st j in ( Seg i()) holds (z . j) in D()

      proof

        let j be Nat;

        assume j in ( Seg i());

        then (z . j) = F(j) by A2, A3;

        hence thesis;

      end;

      then

      reconsider z as FinSequence of D() by A3, Th10;

      take z;

      thus ( len z) = i() by A1;

      let j be Nat;

      thus thesis by A2;

    end;

    scheme :: FINSEQ_2:sch2

    IndSeqD { D() -> set , P[ set] } :

for p be FinSequence of D() holds P[p]

      provided

       A1: P[( <*> D())]

       and

       A2: for p be FinSequence of D() holds for x be Element of D() st P[p] holds P[(p ^ <*x*>)];

      defpred R[ set] means for p be FinSequence of D() st ( len p) = $1 holds P[p];

      

       A3: for i be Nat st R[i] holds R[(i + 1)]

      proof

        let i be Nat such that

         A4: for p be FinSequence of D() st ( len p) = i holds P[p];

        let p be FinSequence of D();

        assume

         A5: ( len p) = (i + 1);

        then

        consider q be FinSequence of D(), x be Element of D() such that

         A6: p = (q ^ <*x*>) by Th17;

        ( len p) = (( len q) + 1) by A6, Th14;

        hence thesis by A2, A4, A5, A6;

      end;

      let p be FinSequence of D();

      

       A7: ( len p) = ( len p);

      

       A8: R[ 0 ]

      proof

        let p be FinSequence of D();

        assume ( len p) = 0 ;

        then p = ( <*> D());

        hence thesis by A1;

      end;

      for i be Nat holds R[i] from NAT_1:sch 2( A8, A3);

      hence thesis by A7;

    end;

    theorem :: FINSEQ_2:24

    

     Th22: for D be set, D1 be Subset of D holds for p be FinSequence of D1 holds p is FinSequence of D

    proof

      let D be set, D1 be Subset of D;

      let p be FinSequence of D1;

      ( rng p) c= D1 by FINSEQ_1:def 4;

      hence ( rng p) c= D by XBOOLE_1: 1;

    end;

    theorem :: FINSEQ_2:25

    

     Th23: for f be Function of ( Seg i), D holds f is FinSequence of D

    proof

      let f be Function of ( Seg i), D;

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

      ( dom f) = ( Seg i) by FUNCT_2:def 1;

      then

       A1: f is FinSequence by FINSEQ_1:def 2;

      ( rng f) c= D by RELAT_1:def 19;

      hence thesis by A1, FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_2:26

    for p be FinSequence of D holds p is Function of ( dom p), D

    proof

      let p be FinSequence of D;

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

      hence thesis by FUNCT_2: 2;

    end;

    theorem :: FINSEQ_2:27

    for f be sequence of D holds (f | ( Seg i)) is FinSequence of D

    proof

      reconsider i as Nat by TARSKI: 1;

      for f be sequence of D holds (f | ( Seg i)) is FinSequence of D by Th23;

      hence thesis;

    end;

    theorem :: FINSEQ_2:28

    for f be sequence of D st q = (f | ( Seg i)) holds ( len q) = i

    proof

      let f be sequence of D;

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

      ( dom (f | ( Seg i))) = ( Seg i) by FUNCT_2:def 1;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: FINSEQ_2:29

    

     Th27: for f be Function st ( rng p) c= ( dom f) & q = (f * p) holds ( len q) = ( len p)

    proof

      let f be Function;

      assume ( rng p) c= ( dom f);

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

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

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: FINSEQ_2:30

    

     Th28: D = ( Seg i) implies for p be FinSequence holds for q be FinSequence of D st i <= ( len p) holds (p * q) is FinSequence

    proof

      assume

       A1: D = ( Seg i);

      let p be FinSequence;

      let q be FinSequence of D;

      assume i <= ( len p);

      then ( Seg i) c= ( Seg ( len p)) by FINSEQ_1: 5;

      then

       A2: ( Seg i) c= ( dom p) by FINSEQ_1:def 3;

      ( rng q) c= ( Seg i) by A1, FINSEQ_1:def 4;

      then ( dom (p * q)) = ( dom q) by A2, RELAT_1: 27, XBOOLE_1: 1;

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

      hence thesis by FINSEQ_1:def 2;

    end;

    theorem :: FINSEQ_2:31

    D = ( Seg i) implies for p be FinSequence of D9 holds for q be FinSequence of D st i <= ( len p) holds (p * q) is FinSequence of D9

    proof

      assume

       A1: D = ( Seg i);

      let p be FinSequence of D9;

      let q be FinSequence of D;

      assume i <= ( len p);

      then

      reconsider pq = (p * q) as FinSequence by A1, Th28;

      ( rng pq) c= ( rng p) & ( rng p) c= D9 by FINSEQ_1:def 4, RELAT_1: 26;

      then ( rng pq) c= D9;

      hence thesis by FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_2:32

    

     Th30: for A,D be set holds for p be FinSequence of A holds for f be Function of A, D holds (f * p) is FinSequence of D

    proof

      let A,D be set;

      let p be FinSequence of A;

      let f be Function of A, D;

      per cases ;

        suppose D = {} ;

        then (f * p) = ( <*> D);

        hence thesis;

      end;

        suppose

         A1: D <> {} ;

        

         A2: ( rng p) c= A by RELAT_1:def 19;

        

         A3: ( rng (f * p)) c= D by RELAT_1:def 19;

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

        then (f * p) is FinSequence by A2, FINSEQ_1: 16;

        hence thesis by A3, FINSEQ_1:def 4;

      end;

    end;

    theorem :: FINSEQ_2:33

    

     Th31: for p be FinSequence of A holds for f be Function of A, D9 st q = (f * p) holds ( len q) = ( len p)

    proof

      let p be FinSequence of A;

      let f be Function of A, D9;

      ( dom f) = A & ( rng p) c= A by FINSEQ_1:def 4, FUNCT_2:def 1;

      hence thesis by Th27;

    end;

    theorem :: FINSEQ_2:34

    for x be set, f be Function st x in ( dom f) holds (f * <*x*>) = <*(f . x)*>

    proof

      let x be set, f be Function;

      assume

       A1: x in ( dom f);

      then

      reconsider D = ( dom f), E = ( rng f) as non empty set by FUNCT_1: 3;

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

      then ( rng <*x*>) c= D by A1, ZFMISC_1: 31;

      then

      reconsider p = <*x*> as FinSequence of D by FINSEQ_1:def 4;

      reconsider f as Function of D, E by FUNCT_2:def 1, RELSET_1: 4;

      reconsider q = (f * p) as FinSequence of E by Th30;

      

       A2: (p . 1) = x by FINSEQ_1: 40;

      

       A3: ( len q) = ( len p) by Th31

      .= 1 by FINSEQ_1: 39;

      then 1 in ( Seg ( len q));

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

      then (q . 1) = (f . x) by A2, FUNCT_1: 12;

      hence thesis by A3, FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:35

    for p be FinSequence of D holds for f be Function of D, D9 st p = <*x1*> holds (f * p) = <*(f . x1)*>

    proof

      let p be FinSequence of D;

      let f be Function of D, D9 such that

       A1: p = <*x1*>;

      

       A2: (p . 1) = x1 by A1, FINSEQ_1: 40;

      reconsider q = (f * p) as FinSequence of D9 by Th30;

      ( len p) = 1 by A1, FINSEQ_1: 39;

      then

       A3: ( len q) = 1 by Th31;

      then 1 in ( Seg ( len q));

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

      then (q . 1) = (f . x1) by A2, FUNCT_1: 12;

      hence thesis by A3, FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:36

    

     Th34: for p be FinSequence of D holds for f be Function of D, D9 st p = <*x1, x2*> holds (f * p) = <*(f . x1), (f . x2)*>

    proof

      let p be FinSequence of D;

      let f be Function of D, D9 such that

       A1: p = <*x1, x2*>;

      

       A2: (p . 2) = x2 by A1, FINSEQ_1: 44;

      reconsider q = (f * p) as FinSequence of D9 by Th30;

      ( len p) = 2 by A1, FINSEQ_1: 44;

      then

       A3: ( len q) = 2 by Th31;

      then 2 in ( Seg ( len q));

      then 2 in ( dom q) by FINSEQ_1:def 3;

      then

       A4: (q . 2) = (f . x2) by A2, FUNCT_1: 12;

      1 in ( Seg ( len q)) by A3;

      then

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

      (p . 1) = x1 by A1, FINSEQ_1: 44;

      then (q . 1) = (f . x1) by A5, FUNCT_1: 12;

      hence thesis by A3, A4, FINSEQ_1: 44;

    end;

    theorem :: FINSEQ_2:37

    

     Th35: for p be FinSequence of D holds for f be Function of D, D9 st p = <*x1, x2, x3*> holds (f * p) = <*(f . x1), (f . x2), (f . x3)*>

    proof

      let p be FinSequence of D;

      let f be Function of D, D9 such that

       A1: p = <*x1, x2, x3*>;

      

       A2: (p . 2) = x2 by A1, FINSEQ_1: 45;

      reconsider q = (f * p) as FinSequence of D9 by Th30;

      ( len p) = 3 by A1, FINSEQ_1: 45;

      then

       A3: ( len q) = 3 by Th31;

      then 2 in ( Seg ( len q));

      then 2 in ( dom q) by FINSEQ_1:def 3;

      then

       A4: (q . 2) = (f . x2) by A2, FUNCT_1: 12;

      

       A5: (p . 3) = x3 by A1, FINSEQ_1: 45;

      

       A6: (p . 1) = x1 by A1, FINSEQ_1: 45;

      3 in ( Seg ( len q)) by A3;

      then 3 in ( dom q) by FINSEQ_1:def 3;

      then

       A7: (q . 3) = (f . x3) by A5, FUNCT_1: 12;

      1 in ( Seg ( len q)) by A3;

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

      then (q . 1) = (f . x1) by A6, FUNCT_1: 12;

      hence thesis by A3, A4, A7, FINSEQ_1: 45;

    end;

    theorem :: FINSEQ_2:38

    

     Th36: for f be Function of ( Seg i), ( Seg j) st (j = 0 implies i = 0 ) & j <= ( len p) holds (p * f) is FinSequence

    proof

      

       A0: i is Nat by TARSKI: 1;

      let f be Function of ( Seg i), ( Seg j);

      assume j = 0 implies i = 0 ;

      then ( Seg j) = {} implies ( Seg i) = {} ;

      then

       A1: ( dom f) = ( Seg i) by FUNCT_2:def 1;

      assume j <= ( len p);

      then ( rng f) c= ( Seg j) & ( Seg j) c= ( Seg ( len p)) by FINSEQ_1: 5, RELAT_1:def 19;

      then ( rng f) c= ( Seg ( len p));

      then ( rng f) c= ( dom p) by FINSEQ_1:def 3;

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

      hence thesis by A0, A1, FINSEQ_1:def 2;

    end;

    theorem :: FINSEQ_2:39

    for f be Function of ( Seg i), ( Seg i) st i <= ( len p) holds (p * f) is FinSequence by Th36;

    theorem :: FINSEQ_2:40

    for f be Function of ( dom p), ( dom p) holds (p * f) is FinSequence

    proof

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

      hence thesis by Th36;

    end;

    theorem :: FINSEQ_2:41

    

     Th39: for f be Function of ( Seg i), ( Seg i) st ( rng f) = ( Seg i) & i <= ( len p) & q = (p * f) holds ( len q) = i

    proof

      let f be Function of ( Seg i), ( Seg i);

      assume ( rng f) = ( Seg i) & i <= ( len p);

      then ( rng f) c= ( Seg ( len p)) by FINSEQ_1: 5;

      then ( rng f) c= ( dom p) by FINSEQ_1:def 3;

      then

       A1: ( dom (p * f)) = ( dom f) by RELAT_1: 27;

      i is Element of NAT & ( dom f) = ( Seg i) by FUNCT_2: 52, ORDINAL1:def 12;

      hence thesis by A1, FINSEQ_1:def 3;

    end;

    theorem :: FINSEQ_2:42

    

     Th40: for f be Function of ( dom p), ( dom p) st ( rng f) = ( dom p) & q = (p * f) holds ( len q) = ( len p)

    proof

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

      hence thesis by Th39;

    end;

    theorem :: FINSEQ_2:43

    

     Th41: for f be Permutation of ( Seg i) st i <= ( len p) & q = (p * f) holds ( len q) = i

    proof

      let f be Permutation of ( Seg i);

      ( rng f) = ( Seg i) by FUNCT_2:def 3;

      hence thesis by Th39;

    end;

    theorem :: FINSEQ_2:44

    for f be Permutation of ( dom p) st q = (p * f) holds ( len q) = ( len p)

    proof

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

      hence thesis by Th41;

    end;

    theorem :: FINSEQ_2:45

    

     Th43: for p be FinSequence of D holds for f be Function of ( Seg i), ( Seg j) st (j = 0 implies i = 0 ) & j <= ( len p) holds (p * f) is FinSequence of D

    proof

      let p be FinSequence of D;

      let f be Function of ( Seg i), ( Seg j) such that

       A1: (j = 0 implies i = 0 ) & j <= ( len p);

      set q = (p * f);

      ( rng p) c= D & ( rng q) c= ( rng p) by FINSEQ_1:def 4, RELAT_1: 26;

      then

       A2: ( rng q) c= D;

      q is FinSequence by A1, Th36;

      hence thesis by A2, FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_2:46

    for p be FinSequence of D holds for f be Function of ( Seg i), ( Seg i) st i <= ( len p) holds (p * f) is FinSequence of D by Th43;

    theorem :: FINSEQ_2:47

    

     Th45: for p be FinSequence of D holds for f be Function of ( dom p), ( dom p) holds (p * f) is FinSequence of D

    proof

      let p be FinSequence of D;

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

      hence thesis by Th43;

    end;

    theorem :: FINSEQ_2:48

    

     Th46: for k be natural Number holds ( id ( Seg k)) is FinSequence of NAT

    proof

      let k be natural Number;

      set I = ( id ( Seg k));

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

      ( dom I) = ( Seg k);

      then ( rng I) = ( Seg k) & I is FinSequence by FINSEQ_1:def 2;

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let i be natural Number;

      :: FINSEQ_2:def1

      func idseq i -> FinSequence equals ( id ( Seg i));

      coherence by Th46;

    end

    registration

      let k be natural Number;

      cluster ( idseq k) -> k -element;

      coherence

      proof

        k in NAT & ( dom ( idseq k)) = ( Seg k) by ORDINAL1:def 12;

        hence ( len ( idseq k)) = k by FINSEQ_1:def 3;

      end;

    end

    registration

      cluster ( idseq 0 ) -> empty;

      coherence ;

    end

    theorem :: FINSEQ_2:49

    for k be Element of ( Seg i) holds (( idseq i) . k) = k;

    theorem :: FINSEQ_2:50

    

     Th48: ( idseq 1) = <*1*>

    proof

      1 in ( Seg 1);

      then ( len ( idseq 1)) = 1 & (( idseq 1) . 1) = 1 by CARD_1:def 7, FUNCT_1: 18;

      hence thesis by FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:51

    

     Th49: ( idseq (i + 1)) = (( idseq i) ^ <*(i + 1)*>)

    proof

      set p = ( idseq (i + 1));

      consider q be FinSequence, a be object such that

       A1: p = (q ^ <*a*>) by FINSEQ_1: 46;

      

       A2: ( len p) = (i + 1) & ( len p) = (( len q) + 1) by A1, Th14, CARD_1:def 7;

      

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

      

       A4: for a be object st a in ( Seg i) holds (q . a) = a

      proof

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

        then

         A5: ( Seg i) c= ( Seg (i + 1)) by FINSEQ_1: 5;

        let a be object;

        assume

         A6: a in ( Seg i);

        then ex j be Nat st a = j & 1 <= j & j <= i;

        then

        reconsider j = a as Nat;

        (p . j) = (q . j) by A1, A2, A3, A6, FINSEQ_1:def 7;

        hence thesis by A6, A5, FUNCT_1: 18;

      end;

      (p . (i + 1)) = (i + 1) by FINSEQ_1: 4, FUNCT_1: 18;

      then a = (i + 1) by A1, A2, FINSEQ_1: 42;

      hence thesis by A1, A2, A3, A4, FUNCT_1: 17;

    end;

    theorem :: FINSEQ_2:52

    

     Th50: ( idseq 2) = <*1, 2*> by Th48, Th49;

    theorem :: FINSEQ_2:53

    ( idseq 3) = <*1, 2, 3*> by Th49, Th50;

    theorem :: FINSEQ_2:54

    

     Th52: ( len p) <= k implies (p * ( idseq k)) = p

    proof

      assume

       A1: ( len p) <= k;

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

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

      then ( dom p) c= ( Seg k) by A1, FINSEQ_1: 5;

      hence thesis by RELAT_1: 51;

    end;

    theorem :: FINSEQ_2:55

    ( idseq k) is Permutation of ( Seg k);

    theorem :: FINSEQ_2:56

    

     Th54: for k be natural Number holds (( Seg k) --> a) is FinSequence

    proof

      let k be natural Number;

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

      ( dom (( Seg k) --> a)) = ( Seg k);

      hence thesis by FINSEQ_1:def 2;

    end;

    registration

      let i be natural Number, a be object;

      cluster (( Seg i) --> a) -> FinSequence-like;

      coherence by Th54;

    end

    definition

      let i be natural Number, a be object;

      :: FINSEQ_2:def2

      func i |-> a -> FinSequence equals (( Seg i) --> a);

      coherence ;

    end

    registration

      let k be natural Number, a be object;

      cluster (k |-> a) -> k -element;

      coherence

      proof

        k in NAT & ( dom (k |-> a)) = ( Seg k) by ORDINAL1:def 12;

        hence ( len (k |-> a)) = k by FINSEQ_1:def 3;

      end;

    end

    theorem :: FINSEQ_2:57

    for d be object, w be set st w in ( Seg k) holds ((k |-> d) . w) = d by FUNCOP_1: 7;

    theorem :: FINSEQ_2:58

    for a be object holds ( 0 |-> a) = {} ;

    theorem :: FINSEQ_2:59

    

     Th57: for a be object holds (1 |-> a) = <*a*>

    proof

      let a be object;

      1 in ( Seg 1);

      then ( len (1 |-> a)) = 1 & ((1 |-> a) . 1) = a by CARD_1:def 7, FUNCOP_1: 7;

      hence thesis by FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:60

    

     Th58: for a be object holds ((i + 1) |-> a) = ((i |-> a) ^ <*a*>)

    proof

      let a be object;

      set p = ((i + 1) |-> a);

      consider q be FinSequence, x be object such that

       A1: p = (q ^ <*x*>) by FINSEQ_1: 46;

      

       A2: ( len p) = (i + 1) & ( len p) = (( len q) + 1) by A1, Th14, CARD_1:def 7;

       A3:

      now

        per cases ;

          suppose

           A4: i = 0 ;

          then q = {} by A2;

          hence q = (i |-> a) by A4;

        end;

          suppose

           A5: i <> 0 ;

          

           A6: ( rng q) c= ( rng p) & ( rng p) = {a} by A1, FINSEQ_1: 29, FUNCOP_1: 8;

          

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

          then i in ( dom q) by A2, A5, FINSEQ_1: 3;

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

          then ( rng q) = {a} by A6, ZFMISC_1: 33;

          hence q = (i |-> a) by A2, A7, FUNCOP_1: 9;

        end;

      end;

      (p . (i + 1)) = a by FINSEQ_1: 4, FUNCOP_1: 7;

      hence thesis by A1, A2, A3, FINSEQ_1: 42;

    end;

    theorem :: FINSEQ_2:61

    

     Th59: for a be object holds (2 |-> a) = <*a, a*>

    proof

      let a be object;

      

      thus (2 |-> a) = ((1 + 1) |-> a)

      .= ((1 |-> a) ^ <*a*>) by Th58

      .= <*a, a*> by Th57;

    end;

    theorem :: FINSEQ_2:62

    for a be object holds (3 |-> a) = <*a, a, a*>

    proof

      let a be object;

      

      thus (3 |-> a) = ((2 + 1) |-> a)

      .= ((2 |-> a) ^ <*a*>) by Th58

      .= ( <*a, a*> ^ <*a*>) by Th59

      .= <*a, a, a*>;

    end;

    theorem :: FINSEQ_2:63

    

     Th61: for k be natural Number holds (k |-> d) is FinSequence of D

    proof

      let k be natural Number;

      set s = (k |-> d);

      ( rng s) c= {d} by FUNCOP_1: 13;

      then ( rng s) c= D by XBOOLE_1: 1;

      hence thesis by FINSEQ_1:def 4;

    end;

    

     Lm3: for F be Function st [:( rng p), ( rng q):] c= ( dom F) & i = ( min (( len p),( len q))) holds ( dom (F .: (p,q))) = ( Seg i)

    proof

      let F be Function such that

       A1: [:( rng p), ( rng q):] c= ( dom F) and

       A2: i = ( min (( len p),( len q)));

      

       A3: ( rng <:p, q:>) c= [:( rng p), ( rng q):] & ( dom <:p, q:>) = (( dom p) /\ ( dom q)) by FUNCT_3: 51, FUNCT_3:def 7;

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

      then (( dom p) /\ ( dom q)) = ( Seg i) by A2, Th1;

      hence thesis by A1, A3, RELAT_1: 27, XBOOLE_1: 1;

    end;

    theorem :: FINSEQ_2:64

    

     Th62: for F be Function st [:( rng p), ( rng q):] c= ( dom F) holds (F .: (p,q)) is FinSequence

    proof

      let F be Function;

      reconsider k = ( min (( len p),( len q))) as Element of NAT by XXREAL_0: 15;

      assume [:( rng p), ( rng q):] c= ( dom F);

      then ( dom (F .: (p,q))) = ( Seg k) by Lm3;

      hence thesis by FINSEQ_1:def 2;

    end;

    theorem :: FINSEQ_2:65

    

     Th63: for F be Function st [:( rng p), ( rng q):] c= ( dom F) & r = (F .: (p,q)) holds ( len r) = ( min (( len p),( len q)))

    proof

      let F be Function;

      reconsider k = ( min (( len p),( len q))) as Element of NAT by XXREAL_0: 15;

      assume [:( rng p), ( rng q):] c= ( dom F);

      then ( dom (F .: (p,q))) = ( Seg k) by Lm3;

      hence thesis by FINSEQ_1:def 3;

    end;

    

     Lm4: for F be Function st [: {a}, ( rng p):] c= ( dom F) holds ( dom (F [;] (a,p))) = ( dom p)

    proof

      let F be Function such that

       A1: [: {a}, ( rng p):] c= ( dom F);

      set q = (( dom p) --> a);

      ( dom q) = ( dom p);

      then

       A2: ( dom <:q, p:>) = ( dom p) by FUNCT_3: 50;

      ( rng q) c= {a} by FUNCOP_1: 13;

      then ( rng <:q, p:>) c= [:( rng q), ( rng p):] & [:( rng q), ( rng p):] c= [: {a}, ( rng p):] by FUNCT_3: 51, ZFMISC_1: 95;

      then

       A3: ( rng <:q, p:>) c= [: {a}, ( rng p):];

      thus thesis by A1, A3, A2, RELAT_1: 27, XBOOLE_1: 1;

    end;

    theorem :: FINSEQ_2:66

    

     Th64: for F be Function st [: {a}, ( rng p):] c= ( dom F) holds (F [;] (a,p)) is FinSequence

    proof

      let F be Function;

      assume [: {a}, ( rng p):] c= ( dom F);

      then ( dom (F [;] (a,p))) = ( dom p) by Lm4;

      then ( dom (F [;] (a,p))) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 2;

    end;

    theorem :: FINSEQ_2:67

    

     Th65: for F be Function st [: {a}, ( rng p):] c= ( dom F) & r = (F [;] (a,p)) holds ( len r) = ( len p)

    proof

      let F be Function;

      assume [: {a}, ( rng p):] c= ( dom F);

      then ( dom (F [;] (a,p))) = ( dom p) by Lm4;

      then ( dom (F [;] (a,p))) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 3;

    end;

    

     Lm5: for F be Function st [:( rng p), {a}:] c= ( dom F) holds ( dom (F [:] (p,a))) = ( dom p)

    proof

      let F be Function such that

       A1: [:( rng p), {a}:] c= ( dom F);

      set q = (( dom p) --> a);

      ( dom q) = ( dom p);

      then

       A2: ( dom <:p, q:>) = ( dom p) by FUNCT_3: 50;

      ( rng q) c= {a} by FUNCOP_1: 13;

      then ( rng <:p, q:>) c= [:( rng p), ( rng q):] & [:( rng p), ( rng q):] c= [:( rng p), {a}:] by FUNCT_3: 51, ZFMISC_1: 95;

      then

       A3: ( rng <:p, q:>) c= [:( rng p), {a}:];

      thus thesis by A1, A3, A2, RELAT_1: 27, XBOOLE_1: 1;

    end;

    theorem :: FINSEQ_2:68

    

     Th66: for F be Function st [:( rng p), {a}:] c= ( dom F) holds (F [:] (p,a)) is FinSequence

    proof

      let F be Function;

      assume [:( rng p), {a}:] c= ( dom F);

      then ( dom (F [:] (p,a))) = ( dom p) by Lm5;

      then ( dom (F [:] (p,a))) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 2;

    end;

    theorem :: FINSEQ_2:69

    

     Th67: for F be Function st [:( rng p), {a}:] c= ( dom F) & r = (F [:] (p,a)) holds ( len r) = ( len p)

    proof

      let F be Function;

      assume [:( rng p), {a}:] c= ( dom F);

      then ( dom (F [:] (p,a))) = ( dom p) by Lm5;

      then ( dom (F [:] (p,a))) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: FINSEQ_2:70

    

     Th68: for F be Function of [:D, D9:], E holds for p be FinSequence of D holds for q be FinSequence of D9 holds (F .: (p,q)) is FinSequence of E

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      let q be FinSequence of D9;

      

       A1: ( rng (F .: (p,q))) c= ( rng F) by RELAT_1: 26;

      ( rng p) c= D & ( rng q) c= D9 by FINSEQ_1:def 4;

      then [:( rng p), ( rng q):] c= [:D, D9:] by ZFMISC_1: 96;

      then [:( rng p), ( rng q):] c= ( dom F) by FUNCT_2:def 1;

      then

       A2: (F .: (p,q)) is FinSequence by Th62;

      ( rng F) c= E by RELAT_1:def 19;

      then ( rng (F .: (p,q))) c= E by A1;

      hence thesis by A2, FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_2:71

    

     Th69: for F be Function of [:D, D9:], E holds for p be FinSequence of D holds for q be FinSequence of D9 st r = (F .: (p,q)) holds ( len r) = ( min (( len p),( len q)))

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      let q be FinSequence of D9;

      ( rng p) c= D & ( rng q) c= D9 by FINSEQ_1:def 4;

      then [:( rng p), ( rng q):] c= [:D, D9:] by ZFMISC_1: 96;

      then [:( rng p), ( rng q):] c= ( dom F) by FUNCT_2:def 1;

      hence thesis by Th63;

    end;

    theorem :: FINSEQ_2:72

    

     Th70: for F be Function of [:D, D9:], E holds for p be FinSequence of D holds for q be FinSequence of D9 st ( len p) = ( len q) & r = (F .: (p,q)) holds ( len r) = ( len p) & ( len r) = ( len q)

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      let q be FinSequence of D9;

      assume that

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

       A2: r = (F .: (p,q));

      ( len r) = ( min (( len p),( len q))) by A2, Th69;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_2:73

    for F be Function of [:D, D9:], E holds for p be FinSequence of D holds for p9 be FinSequence of D9 holds (F .: (( <*> D),p9)) = ( <*> E) & (F .: (p,( <*> D9))) = ( <*> E)

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      let p9 be FinSequence of D9;

      reconsider r = (F .: (( <*> D),p9)), r9 = (F .: (p,( <*> D9))) as FinSequence of E by Th68;

      ( len ( <*> D)) = 0 ;

      then ( len r) = ( min ( 0 ,( len p9))) & ( len r9) = ( min (( len p), 0 )) by Th69;

      hence thesis by XXREAL_0:def 9;

    end;

    theorem :: FINSEQ_2:74

    for F be Function of [:D, D9:], E holds for p be FinSequence of D holds for q be FinSequence of D9 st p = <*d1*> & q = <*d19*> holds (F .: (p,q)) = <*(F . (d1,d19))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      let q be FinSequence of D9 such that

       A1: p = <*d1*> & q = <*d19*>;

      

       A2: (p . 1) = d1 & (q . 1) = d19 by A1, FINSEQ_1: 40;

      reconsider r = (F .: (p,q)) as FinSequence of E by Th68;

      ( len p) = 1 & ( len q) = 1 by A1, FINSEQ_1: 39;

      then

       A3: ( len r) = 1 by Th70;

      then 1 in ( Seg ( len r));

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

      then (r . 1) = (F . (d1,d19)) by A2, FUNCOP_1: 22;

      hence thesis by A3, FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:75

    for F be Function of [:D, D9:], E holds for p be FinSequence of D holds for q be FinSequence of D9 st p = <*d1, d2*> & q = <*d19, d29*> holds (F .: (p,q)) = <*(F . (d1,d19)), (F . (d2,d29))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      let q be FinSequence of D9 such that

       A1: p = <*d1, d2*> & q = <*d19, d29*>;

      

       A2: (p . 2) = d2 & (q . 2) = d29 by A1, FINSEQ_1: 44;

      reconsider r = (F .: (p,q)) as FinSequence of E by Th68;

      ( len p) = 2 & ( len q) = 2 by A1, FINSEQ_1: 44;

      then

       A3: ( len r) = 2 by Th70;

      then 2 in ( Seg ( len r));

      then 2 in ( dom r) by FINSEQ_1:def 3;

      then

       A4: (r . 2) = (F . (d2,d29)) by A2, FUNCOP_1: 22;

      1 in ( Seg ( len r)) by A3;

      then

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

      (p . 1) = d1 & (q . 1) = d19 by A1, FINSEQ_1: 44;

      then (r . 1) = (F . (d1,d19)) by A5, FUNCOP_1: 22;

      hence thesis by A3, A4, FINSEQ_1: 44;

    end;

    theorem :: FINSEQ_2:76

    for F be Function of [:D, D9:], E holds for p be FinSequence of D holds for q be FinSequence of D9 st p = <*d1, d2, d3*> & q = <*d19, d29, d39*> holds (F .: (p,q)) = <*(F . (d1,d19)), (F . (d2,d29)), (F . (d3,d39))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      let q be FinSequence of D9 such that

       A1: p = <*d1, d2, d3*> & q = <*d19, d29, d39*>;

      

       A2: (p . 2) = d2 & (q . 2) = d29 by A1, FINSEQ_1: 45;

      reconsider r = (F .: (p,q)) as FinSequence of E by Th68;

      ( len p) = 3 & ( len q) = 3 by A1, FINSEQ_1: 45;

      then

       A3: ( len r) = 3 by Th70;

      then 2 in ( Seg ( len r));

      then 2 in ( dom r) by FINSEQ_1:def 3;

      then

       A4: (r . 2) = (F . (d2,d29)) by A2, FUNCOP_1: 22;

      

       A5: (p . 3) = d3 & (q . 3) = d39 by A1, FINSEQ_1: 45;

      

       A6: (p . 1) = d1 & (q . 1) = d19 by A1, FINSEQ_1: 45;

      3 in ( Seg ( len r)) by A3;

      then 3 in ( dom r) by FINSEQ_1:def 3;

      then

       A7: (r . 3) = (F . (d3,d39)) by A5, FUNCOP_1: 22;

      1 in ( Seg ( len r)) by A3;

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

      then (r . 1) = (F . (d1,d19)) by A6, FUNCOP_1: 22;

      hence thesis by A3, A4, A7, FINSEQ_1: 45;

    end;

    theorem :: FINSEQ_2:77

    

     Th75: for F be Function of [:D, D9:], E holds for p be FinSequence of D9 holds (F [;] (d,p)) is FinSequence of E

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D9;

      

       A1: ( rng (F [;] (d,p))) c= ( rng F) by RELAT_1: 26;

      ( rng p) c= D9 by FINSEQ_1:def 4;

      then [: {d}, ( rng p):] c= [:D, D9:] by ZFMISC_1: 96;

      then [: {d}, ( rng p):] c= ( dom F) by FUNCT_2:def 1;

      then

       A2: (F [;] (d,p)) is FinSequence by Th64;

      ( rng F) c= E by RELAT_1:def 19;

      then ( rng (F [;] (d,p))) c= E by A1;

      hence thesis by A2, FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_2:78

    

     Th76: for F be Function of [:D, D9:], E holds for p be FinSequence of D9 st r = (F [;] (d,p)) holds ( len r) = ( len p)

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D9;

      ( rng p) c= D9 by FINSEQ_1:def 4;

      then [: {d}, ( rng p):] c= [:D, D9:] by ZFMISC_1: 96;

      then [: {d}, ( rng p):] c= ( dom F) by FUNCT_2:def 1;

      hence thesis by Th65;

    end;

    theorem :: FINSEQ_2:79

    for F be Function of [:D, D9:], E holds (F [;] (d,( <*> D9))) = ( <*> E)

    proof

      let F be Function of [:D, D9:], E;

      reconsider r = (F [;] (d,( <*> D9))) as FinSequence of E by Th75;

      ( len ( <*> D9)) = 0 ;

      then ( len r) = 0 by Th76;

      hence thesis;

    end;

    theorem :: FINSEQ_2:80

    for F be Function of [:D, D9:], E holds for p be FinSequence of D9 st p = <*d19*> holds (F [;] (d,p)) = <*(F . (d,d19))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D9 such that

       A1: p = <*d19*>;

      

       A2: (p . 1) = d19 by A1, FINSEQ_1: 40;

      reconsider r = (F [;] (d,p)) as FinSequence of E by Th75;

      ( len p) = 1 by A1, FINSEQ_1: 39;

      then

       A3: ( len r) = 1 by Th76;

      then 1 in ( Seg ( len r));

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

      then (r . 1) = (F . (d,d19)) by A2, FUNCOP_1: 32;

      hence thesis by A3, FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:81

    for F be Function of [:D, D9:], E holds for p be FinSequence of D9 st p = <*d19, d29*> holds (F [;] (d,p)) = <*(F . (d,d19)), (F . (d,d29))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D9 such that

       A1: p = <*d19, d29*>;

      

       A2: (p . 2) = d29 by A1, FINSEQ_1: 44;

      reconsider r = (F [;] (d,p)) as FinSequence of E by Th75;

      ( len p) = 2 by A1, FINSEQ_1: 44;

      then

       A3: ( len r) = 2 by Th76;

      then 2 in ( Seg ( len r));

      then 2 in ( dom r) by FINSEQ_1:def 3;

      then

       A4: (r . 2) = (F . (d,d29)) by A2, FUNCOP_1: 32;

      1 in ( Seg ( len r)) by A3;

      then

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

      (p . 1) = d19 by A1, FINSEQ_1: 44;

      then (r . 1) = (F . (d,d19)) by A5, FUNCOP_1: 32;

      hence thesis by A3, A4, FINSEQ_1: 44;

    end;

    theorem :: FINSEQ_2:82

    for F be Function of [:D, D9:], E holds for p be FinSequence of D9 st p = <*d19, d29, d39*> holds (F [;] (d,p)) = <*(F . (d,d19)), (F . (d,d29)), (F . (d,d39))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D9 such that

       A1: p = <*d19, d29, d39*>;

      

       A2: (p . 2) = d29 by A1, FINSEQ_1: 45;

      reconsider r = (F [;] (d,p)) as FinSequence of E by Th75;

      ( len p) = 3 by A1, FINSEQ_1: 45;

      then

       A3: ( len r) = 3 by Th76;

      then 2 in ( Seg ( len r));

      then 2 in ( dom r) by FINSEQ_1:def 3;

      then

       A4: (r . 2) = (F . (d,d29)) by A2, FUNCOP_1: 32;

      

       A5: (p . 3) = d39 by A1, FINSEQ_1: 45;

      

       A6: (p . 1) = d19 by A1, FINSEQ_1: 45;

      3 in ( Seg ( len r)) by A3;

      then 3 in ( dom r) by FINSEQ_1:def 3;

      then

       A7: (r . 3) = (F . (d,d39)) by A5, FUNCOP_1: 32;

      1 in ( Seg ( len r)) by A3;

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

      then (r . 1) = (F . (d,d19)) by A6, FUNCOP_1: 32;

      hence thesis by A3, A4, A7, FINSEQ_1: 45;

    end;

    theorem :: FINSEQ_2:83

    

     Th81: for F be Function of [:D, D9:], E holds for p be FinSequence of D holds (F [:] (p,d9)) is FinSequence of E

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

      

       A1: ( rng (F [:] (p,d9))) c= ( rng F) by RELAT_1: 26;

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

      then [:( rng p), {d9}:] c= [:D, D9:] by ZFMISC_1: 96;

      then [:( rng p), {d9}:] c= ( dom F) by FUNCT_2:def 1;

      then

       A2: (F [:] (p,d9)) is FinSequence by Th66;

      ( rng F) c= E by RELAT_1:def 19;

      then ( rng (F [:] (p,d9))) c= E by A1;

      hence thesis by A2, FINSEQ_1:def 4;

    end;

    theorem :: FINSEQ_2:84

    

     Th82: for F be Function of [:D, D9:], E holds for p be FinSequence of D st r = (F [:] (p,d9)) holds ( len r) = ( len p)

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D;

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

      then [:( rng p), {d9}:] c= [:D, D9:] by ZFMISC_1: 96;

      then [:( rng p), {d9}:] c= ( dom F) by FUNCT_2:def 1;

      hence thesis by Th67;

    end;

    theorem :: FINSEQ_2:85

    for F be Function of [:D, D9:], E holds (F [:] (( <*> D),d9)) = ( <*> E)

    proof

      let F be Function of [:D, D9:], E;

      reconsider r = (F [:] (( <*> D),d9)) as FinSequence of E by Th81;

      ( len ( <*> D)) = 0 ;

      then ( len r) = 0 by Th82;

      hence thesis;

    end;

    theorem :: FINSEQ_2:86

    for F be Function of [:D, D9:], E holds for p be FinSequence of D st p = <*d1*> holds (F [:] (p,d9)) = <*(F . (d1,d9))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D such that

       A1: p = <*d1*>;

      

       A2: (p . 1) = d1 by A1, FINSEQ_1: 40;

      reconsider r = (F [:] (p,d9)) as FinSequence of E by Th81;

      ( len p) = 1 by A1, FINSEQ_1: 39;

      then

       A3: ( len r) = 1 by Th82;

      then 1 in ( Seg ( len r));

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

      then (r . 1) = (F . (d1,d9)) by A2, FUNCOP_1: 27;

      hence thesis by A3, FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:87

    for F be Function of [:D, D9:], E holds for p be FinSequence of D st p = <*d1, d2*> holds (F [:] (p,d9)) = <*(F . (d1,d9)), (F . (d2,d9))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D such that

       A1: p = <*d1, d2*>;

      

       A2: (p . 2) = d2 by A1, FINSEQ_1: 44;

      reconsider r = (F [:] (p,d9)) as FinSequence of E by Th81;

      ( len p) = 2 by A1, FINSEQ_1: 44;

      then

       A3: ( len r) = 2 by Th82;

      then 2 in ( Seg ( len r));

      then 2 in ( dom r) by FINSEQ_1:def 3;

      then

       A4: (r . 2) = (F . (d2,d9)) by A2, FUNCOP_1: 27;

      1 in ( Seg ( len r)) by A3;

      then

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

      (p . 1) = d1 by A1, FINSEQ_1: 44;

      then (r . 1) = (F . (d1,d9)) by A5, FUNCOP_1: 27;

      hence thesis by A3, A4, FINSEQ_1: 44;

    end;

    theorem :: FINSEQ_2:88

    for F be Function of [:D, D9:], E holds for p be FinSequence of D st p = <*d1, d2, d3*> holds (F [:] (p,d9)) = <*(F . (d1,d9)), (F . (d2,d9)), (F . (d3,d9))*>

    proof

      let F be Function of [:D, D9:], E;

      let p be FinSequence of D such that

       A1: p = <*d1, d2, d3*>;

      

       A2: (p . 2) = d2 by A1, FINSEQ_1: 45;

      reconsider r = (F [:] (p,d9)) as FinSequence of E by Th81;

      ( len p) = 3 by A1, FINSEQ_1: 45;

      then

       A3: ( len r) = 3 by Th82;

      then 2 in ( Seg ( len r));

      then 2 in ( dom r) by FINSEQ_1:def 3;

      then

       A4: (r . 2) = (F . (d2,d9)) by A2, FUNCOP_1: 27;

      

       A5: (p . 3) = d3 by A1, FINSEQ_1: 45;

      

       A6: (p . 1) = d1 by A1, FINSEQ_1: 45;

      3 in ( Seg ( len r)) by A3;

      then 3 in ( dom r) by FINSEQ_1:def 3;

      then

       A7: (r . 3) = (F . (d3,d9)) by A5, FUNCOP_1: 27;

      1 in ( Seg ( len r)) by A3;

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

      then (r . 1) = (F . (d1,d9)) by A6, FUNCOP_1: 27;

      hence thesis by A3, A4, A7, FINSEQ_1: 45;

    end;

    definition

      let D be set;

      :: FINSEQ_2:def3

      mode FinSequenceSet of D -> set means

      : Def3: a in it implies a is FinSequence of D;

      existence

      proof

        take (D * );

        thus thesis by FINSEQ_1:def 11;

      end;

    end

    definition

      let D be set, S be FinSequenceSet of D;

      :: original: Element

      redefine

      mode Element of S -> FinSequence of D ;

      coherence

      proof

        per cases ;

          suppose S is non empty;

          hence thesis by Def3;

        end;

          suppose S is empty;

          then S = ( <*> D);

          hence thesis by SUBSET_1:def 1;

        end;

      end;

    end

    registration

      let D be set;

      cluster non empty for FinSequenceSet of D;

      existence

      proof

         {( <*> D)} is FinSequenceSet of D

        proof

          let a;

          thus thesis by TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: FINSEQ_2:89

    

     Th87: for D be set holds (D * ) is FinSequenceSet of D

    proof

      let D be set;

      (D * ) is FinSequenceSet of D

      proof

        let a;

        thus thesis by FINSEQ_1:def 11;

      end;

      hence thesis;

    end;

    definition

      let D be set;

      :: original: *

      redefine

      func D * -> FinSequenceSet of D ;

      coherence by Th87;

    end

    theorem :: FINSEQ_2:90

    for D be set, D9 be FinSequenceSet of D holds D9 c= (D * )

    proof

      let D be set, D9 be FinSequenceSet of D;

      let a be object;

      assume a in D9;

      then a is FinSequence of D by Def3;

      hence thesis by FINSEQ_1:def 11;

    end;

    theorem :: FINSEQ_2:91

    for D9 be Subset of D, S be FinSequenceSet of D9 holds S is FinSequenceSet of D

    proof

      let D9 be Subset of D, S be FinSequenceSet of D9;

      S is FinSequenceSet of D

      proof

        let a;

        assume a in S;

        then

        reconsider p = a as FinSequence of D9 by Def3;

        ( rng p) c= D9 by FINSEQ_1:def 4;

        then ( rng p) c= D by XBOOLE_1: 1;

        hence thesis by FINSEQ_1:def 4;

      end;

      hence thesis;

    end;

    reserve s for Element of (D * );

    registration

      let i be natural Number, D;

      cluster i -element for FinSequence of D;

      existence

      proof

        take (i |-> the Element of D);

        thus thesis by Th61;

      end;

    end

    definition

      let i be natural Number, D be non empty set;

      mode Tuple of i,D is i -element FinSequence of D;

    end

    definition

      let i be natural Number;

      let D be set;

      :: FINSEQ_2:def4

      func i -tuples_on D -> FinSequenceSet of D equals { s where s be Element of (D * ) : ( len s) = i };

      coherence

      proof

        now

          let a;

          assume a in { s where s be Element of (D * ) : ( len s) = i };

          then ex s be Element of (D * ) st s = a & ( len s) = i;

          hence a is FinSequence of D;

        end;

        hence thesis by Def3;

      end;

    end

    registration

      let i be natural Number, D;

      cluster (i -tuples_on D) -> non empty;

      coherence

      proof

        set d = the Element of D;

        (i |-> d) is FinSequence of D by Th61;

        then

        reconsider S = (i |-> d) as Element of (D * ) by FINSEQ_1:def 11;

        ( len S) = i by CARD_1:def 7;

        then S in { s : ( len s) = i };

        hence thesis;

      end;

    end

    registration

      let D;

      let i be natural Number;

      cluster -> i -element for Element of (i -tuples_on D);

      coherence

      proof

        let z be Element of (i -tuples_on D);

        z in { p9 where p9 be Element of (D * ) : ( len p9) = i };

        then ex p9 be Element of (D * ) st p9 = z & ( len p9) = i;

        hence ( len z) = i;

      end;

    end

    theorem :: FINSEQ_2:92

    

     Th90: for D be set, z be FinSequence of D holds z is Element of (( len z) -tuples_on D)

    proof

      let D be set, z be FinSequence of D;

      z is Element of (D * ) by FINSEQ_1:def 11;

      then z in { z9 where z9 be Element of (D * ) : ( len z9) = ( len z) };

      hence thesis;

    end;

    theorem :: FINSEQ_2:93

    for D be set holds (i -tuples_on D) = ( Funcs (( Seg i),D))

    proof

      let D be set;

      now

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

        let z be object;

        thus z in (i -tuples_on D) implies z in ( Funcs (( Seg i),D))

        proof

          assume z in (i -tuples_on D);

          then

          consider s be Element of (D * ) such that

           A1: z = s and

           A2: ( len s) = i;

          

           A3: ( rng s) c= D by FINSEQ_1:def 4;

          ( dom s) = ( Seg i) by A2, FINSEQ_1:def 3;

          hence thesis by A1, A3, FUNCT_2:def 2;

        end;

        assume z in ( Funcs (( Seg i),D));

        then

        consider p be Function such that

         A4: z = p and

         A5: ( dom p) = ( Seg j) and

         A6: ( rng p) c= D by FUNCT_2:def 2;

        p is FinSequence by A5, FINSEQ_1:def 2;

        then p is FinSequence of D by A6, FINSEQ_1:def 4;

        then

        reconsider p as Element of (D * ) by FINSEQ_1:def 11;

        ( len p) = i by A5, FINSEQ_1:def 3;

        hence z in (i -tuples_on D) by A4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINSEQ_2:94

    for D be set holds ( 0 -tuples_on D) = {( <*> D)}

    proof

      let D be set;

      now

        let z be object;

        thus z in ( 0 -tuples_on D) implies z = ( <*> D)

        proof

          assume z in ( 0 -tuples_on D);

          then ex s be Element of (D * ) st z = s & ( len s) = 0 ;

          hence thesis;

        end;

        ( <*> D) is Element of (D * ) & ( len ( <*> D)) = 0 by FINSEQ_1:def 11;

        hence z = ( <*> D) implies z in ( 0 -tuples_on D);

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FINSEQ_2:95

    for z be Tuple of 0 , D holds for t be Tuple of i, D holds (z ^ t) = t & (t ^ z) = t by FINSEQ_1: 34;

    theorem :: FINSEQ_2:96

    

     Th94: (1 -tuples_on D) = the set of all <*d*>

    proof

      now

        let x be object;

        thus x in (1 -tuples_on D) implies x in the set of all <*d*>

        proof

          assume x in (1 -tuples_on D);

          then

          consider s such that

           A1: x = s and

           A2: ( len s) = 1;

          1 in ( Seg 1);

          then 1 in ( dom s) by A2, FINSEQ_1:def 3;

          then

          reconsider d1 = (s . 1) as Element of D by Th9;

          s = <*d1*> by A2, FINSEQ_1: 40;

          hence thesis by A1;

        end;

        assume x in the set of all <*d*>;

        then

        consider d such that

         A3: x = <*d*>;

        ( len <*d*>) = 1 & <*d*> is Element of (D * ) by FINSEQ_1: 40, FINSEQ_1:def 11;

        hence x in (1 -tuples_on D) by A3;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm6: for z be Tuple of i, D holds z in (i -tuples_on D)

    proof

      let z be Tuple of i, D;

      

       A1: z is Element of (D * ) by FINSEQ_1:def 11;

      ( len z) = i by CARD_1:def 7;

      hence z in (i -tuples_on D) by A1;

    end;

    theorem :: FINSEQ_2:97

    

     Th95: for z be Tuple of 1, D holds ex d st z = <*d*>

    proof

      let z be Tuple of 1, D;

      z in (1 -tuples_on D) by Lm6;

      then z in the set of all <*d*> by Th94;

      hence thesis;

    end;

    theorem :: FINSEQ_2:98

    

     Th96: <*d*> in (1 -tuples_on D)

    proof

       <*d*> in the set of all <*d1*>;

      hence thesis by Th94;

    end;

    theorem :: FINSEQ_2:99

    

     Th97: (2 -tuples_on D) = the set of all <*d1, d2*>

    proof

      now

        let x be object;

        thus x in (2 -tuples_on D) implies x in the set of all <*d1, d2*>

        proof

          assume x in (2 -tuples_on D);

          then

          consider s such that

           A1: x = s and

           A2: ( len s) = 2;

          2 in ( Seg 2);

          then

           A3: 2 in ( dom s) by A2, FINSEQ_1:def 3;

          1 in ( Seg 2);

          then 1 in ( dom s) by A2, FINSEQ_1:def 3;

          then

          reconsider d19 = (s . 1), d29 = (s . 2) as Element of D by A3, Th9;

          s = <*d19, d29*> by A2, FINSEQ_1: 44;

          hence thesis by A1;

        end;

        assume x in the set of all <*d1, d2*>;

        then

        consider d1, d2 such that

         A4: x = <*d1, d2*>;

         <*d1, d2*> is FinSequence of D by Th11;

        then ( len <*d1, d2*>) = 2 & <*d1, d2*> is Element of (D * ) by FINSEQ_1: 44, FINSEQ_1:def 11;

        hence x in (2 -tuples_on D) by A4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINSEQ_2:100

    for z be Tuple of 2, D holds ex d1, d2 st z = <*d1, d2*>

    proof

      let z be Tuple of 2, D;

      

       A1: z is Element of (D * ) by FINSEQ_1:def 11;

      ( len z) = 2 by CARD_1:def 7;

      then z in (2 -tuples_on D) by A1;

      then z in the set of all <*d1, d2*> by Th97;

      hence thesis;

    end;

    theorem :: FINSEQ_2:101

    

     Th99: <*d1, d2*> in (2 -tuples_on D)

    proof

       <*d1, d2*> in the set of all <*c1, c2*> where c1 be Element of D, c2 be Element of D;

      hence thesis by Th97;

    end;

    theorem :: FINSEQ_2:102

    

     Th100: (3 -tuples_on D) = the set of all <*d1, d2, d3*>

    proof

      now

        let x be object;

        thus x in (3 -tuples_on D) implies x in the set of all <*d1, d2, d3*>

        proof

          assume x in (3 -tuples_on D);

          then

          consider s such that

           A1: x = s and

           A2: ( len s) = 3;

          2 in ( Seg 3);

          then

           A3: 2 in ( dom s) by A2, FINSEQ_1:def 3;

          3 in ( Seg 3);

          then

           A4: 3 in ( dom s) by A2, FINSEQ_1:def 3;

          1 in ( Seg 3);

          then 1 in ( dom s) by A2, FINSEQ_1:def 3;

          then

          reconsider d19 = (s . 1), d29 = (s . 2), d39 = (s . 3) as Element of D by A3, A4, Th9;

          s = <*d19, d29, d39*> by A2, FINSEQ_1: 45;

          hence thesis by A1;

        end;

        assume x in the set of all <*d1, d2, d3*>;

        then

        consider d1, d2, d3 such that

         A5: x = <*d1, d2, d3*>;

         <*d1, d2, d3*> is FinSequence of D by Th12;

        then ( len <*d1, d2, d3*>) = 3 & <*d1, d2, d3*> is Element of (D * ) by FINSEQ_1: 45, FINSEQ_1:def 11;

        hence x in (3 -tuples_on D) by A5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINSEQ_2:103

    for z be Tuple of 3, D holds ex d1, d2, d3 st z = <*d1, d2, d3*>

    proof

      let z be Tuple of 3, D;

      

       A1: z is Element of (D * ) by FINSEQ_1:def 11;

      ( len z) = 3 by CARD_1:def 7;

      then z in (3 -tuples_on D) by A1;

      then z in the set of all <*d1, d2, d3*> by Th100;

      hence thesis;

    end;

    theorem :: FINSEQ_2:104

    

     Th102: <*d1, d2, d3*> in (3 -tuples_on D)

    proof

       <*d1, d2, d3*> in the set of all <*c1, c2, c3*> where c1 be Element of D, c2 be Element of D, c3 be Element of D;

      hence thesis by Th100;

    end;

    theorem :: FINSEQ_2:105

    

     Th103: ((i + j) -tuples_on D) = the set of all (z ^ t) where z be Tuple of i, D, t be Tuple of j, D

    proof

      set T = the set of all (z ^ t) where z be Tuple of i, D, t be Tuple of j, D;

      now

        let x be object;

        thus x in ((i + j) -tuples_on D) implies x in T

        proof

          assume x in ((i + j) -tuples_on D);

          then

          consider s such that

           A1: x = s and

           A2: ( len s) = (i + j);

          consider z,t be FinSequence of D such that

           A3: ( len z) = i & ( len t) = j and

           A4: s = (z ^ t) by A2, Th21;

          z is Tuple of i, D & t is Tuple of j, D by A3, CARD_1:def 7;

          hence thesis by A1, A4;

        end;

        assume x in T;

        then

        consider z be Tuple of i, D, t be Tuple of j, D such that

         A5: x = (z ^ t);

        ( len z) = i & ( len t) = j by CARD_1:def 7;

        then

         A6: ( len (z ^ t)) = (i + j) by FINSEQ_1: 22;

        (z ^ t) is Element of (D * ) by FINSEQ_1:def 11;

        hence x in ((i + j) -tuples_on D) by A5, A6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINSEQ_2:106

    

     Th104: for s be Tuple of (i + j), D holds ex z be Element of (i -tuples_on D), t be Element of (j -tuples_on D) st s = (z ^ t)

    proof

      let s be Tuple of (i + j), D;

      

       A1: s is Element of (D * ) by FINSEQ_1:def 11;

      ( len s) = (i + j) by CARD_1:def 7;

      then s in ((i + j) -tuples_on D) by A1;

      then s in the set of all (z ^ t) where z be Tuple of i, D, t be Tuple of j, D by Th103;

      then

      consider z be Tuple of i, D, t be Tuple of j, D such that

       A2: s = (z ^ t);

      reconsider z as Element of (i -tuples_on D) by Lm6;

      reconsider t as Element of (j -tuples_on D) by Lm6;

      s = (z ^ t) by A2;

      hence thesis;

    end;

    theorem :: FINSEQ_2:107

    for z be Tuple of i, D holds for t be Tuple of j, D holds (z ^ t) is Tuple of (i + j), D;

    theorem :: FINSEQ_2:108

    (D * ) = ( union the set of all (i -tuples_on D) where i be Nat)

    proof

      for a be object holds a in (D * ) iff a in ( union the set of all (i -tuples_on D) where i be Nat)

      proof

        let a be object;

        thus a in (D * ) implies a in ( union the set of all (i -tuples_on D) where i be Nat)

        proof

          assume a in (D * );

          then

          reconsider a as FinSequence of D by FINSEQ_1:def 11;

          a is Element of (( len a) -tuples_on D) & (( len a) -tuples_on D) in the set of all (i -tuples_on D) where i be Nat by Th90;

          hence thesis by TARSKI:def 4;

        end;

        assume a in ( union the set of all (i -tuples_on D) where i be Nat);

        then

        consider Z be set such that

         A1: a in Z and

         A2: Z in the set of all (i -tuples_on D) where i be Nat by TARSKI:def 4;

        consider i be Nat such that

         A3: Z = (i -tuples_on D) by A2;

        ex s be Element of (D * ) st s = a & ( len s) = i by A1, A3;

        hence thesis;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINSEQ_2:109

    for D9 be non empty Subset of D holds for z be Tuple of i, D9 holds z is Element of (i -tuples_on D)

    proof

      let D9 be non empty Subset of D;

      let z be Tuple of i, D9;

      z is Tuple of i, D by Th22;

      hence thesis by Lm6;

    end;

    

     Lm7: for x be object holds x in (i -tuples_on A) implies x is i -element FinSequence

    proof

      let x be object;

      assume x in (i -tuples_on A);

      then x in { s where s be Element of (A * ) : ( len s) = i };

      then ex s be Element of (A * ) st x = s & ( len s) = i;

      hence thesis by CARD_1:def 7;

    end;

    theorem :: FINSEQ_2:110

    (i -tuples_on D) = (j -tuples_on A) implies i = j

    proof

      set f = (i |-> the Element of D);

      f is Tuple of i, D by Th61;

      then

       A1: f in (i -tuples_on D) by Lm6;

      assume (i -tuples_on D) = (j -tuples_on A);

      then f in (j -tuples_on A) by A1;

      then f is j -element by Lm7;

      then ( len f) = j;

      hence thesis by CARD_1:def 7;

    end;

    theorem :: FINSEQ_2:111

    ( idseq i) is Element of (i -tuples_on NAT )

    proof

      ( idseq i) is FinSequence of NAT & ( len ( idseq i)) = i by Th46, CARD_1:def 7;

      hence thesis by Th90;

    end;

    theorem :: FINSEQ_2:112

    

     Th110: (i |-> d) is Element of (i -tuples_on D)

    proof

      (i |-> d) is FinSequence of D & ( len (i |-> d)) = i by Th61, CARD_1:def 7;

      hence thesis by Lm6;

    end;

    theorem :: FINSEQ_2:113

    for z be Tuple of i, D holds for f be Function of D, D9 holds (f * z) is Element of (i -tuples_on D9)

    proof

      let z be Tuple of i, D;

      let f be Function of D, D9;

      reconsider s = (f * z) as FinSequence of D9 by Th30;

      ( len z) = i by CARD_1:def 7;

      then ( len s) = i by Th31;

      hence thesis by Th90;

    end;

    theorem :: FINSEQ_2:114

    

     Th112: for z be Tuple of i, D holds for f be Function of ( Seg i), ( Seg i) st ( rng f) = ( Seg i) holds (z * f) is Element of (i -tuples_on D)

    proof

      let z be Tuple of i, D;

      let f be Function of ( Seg i), ( Seg i);

      

       A1: ( len z) = i by CARD_1:def 7;

      then

       A2: ( Seg i) = ( dom z) by FINSEQ_1:def 3;

      then

      reconsider t = (z * f) as FinSequence of D by Th45;

      assume ( rng f) = ( Seg i);

      then ( len t) = ( len z) by A2, Th40;

      hence thesis by A1, Th90;

    end;

    theorem :: FINSEQ_2:115

    for z be Tuple of i, D holds for f be Permutation of ( Seg i) holds (z * f) is Tuple of i, D

    proof

      let z be Tuple of i, D;

      let f be Permutation of ( Seg i);

      ( rng f) = ( Seg i) by FUNCT_2:def 3;

      hence thesis by Th112;

    end;

    theorem :: FINSEQ_2:116

    for z be Tuple of i, D holds for d holds ((z ^ <*d*>) . (i + 1)) = d

    proof

      let z be Tuple of i, D;

      let d;

      ( len z) = i by CARD_1:def 7;

      hence thesis by FINSEQ_1: 42;

    end;

    theorem :: FINSEQ_2:117

    for z be Tuple of (i + 1), D holds ex t be Element of (i -tuples_on D), d st z = (t ^ <*d*>)

    proof

      let z be Tuple of (i + 1), D;

      consider t be Element of (i -tuples_on D), s be Element of (1 -tuples_on D) such that

       A1: z = (t ^ s) by Th104;

      ex d st s = <*d*> by Th95;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_2:118

    for z be Tuple of i, D holds (z * ( idseq i)) = z

    proof

      let z be Tuple of i, D;

      ( len z) = i by CARD_1:def 7;

      hence thesis by Th52;

    end;

    theorem :: FINSEQ_2:119

    for z1,z2 be Tuple of i, D st for j be Nat st j in ( Seg i) holds (z1 . j) = (z2 . j) holds z1 = z2

    proof

      let z1,z2 be Tuple of i, D;

      ( len z2) = i by CARD_1:def 7;

      then

       A1: ( dom z2) = ( Seg i) by FINSEQ_1:def 3;

      ( len z1) = i by CARD_1:def 7;

      then ( dom z1) = ( Seg i) by FINSEQ_1:def 3;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_2:120

    for F be Function of [:D, D9:], E holds for z1 be Tuple of i, D holds for z2 be Tuple of i, D9 holds (F .: (z1,z2)) is Element of (i -tuples_on E)

    proof

      let F be Function of [:D, D9:], E;

      let z1 be Tuple of i, D;

      let z2 be Tuple of i, D9;

      reconsider r = (F .: (z1,z2)) as FinSequence of E by Th68;

      ( len z1) = i & ( len z2) = i by CARD_1:def 7;

      then ( len r) = i by Th70;

      hence thesis by Th90;

    end;

    theorem :: FINSEQ_2:121

    for F be Function of [:D, D9:], E holds for z be Tuple of i, D9 holds (F [;] (d,z)) is Element of (i -tuples_on E)

    proof

      let F be Function of [:D, D9:], E;

      let z be Tuple of i, D9;

      reconsider r = (F [;] (d,z)) as FinSequence of E by Th75;

      ( len z) = i by CARD_1:def 7;

      then ( len r) = i by Th76;

      hence thesis by Th90;

    end;

    theorem :: FINSEQ_2:122

    for F be Function of [:D, D9:], E holds for z be Tuple of i, D holds (F [:] (z,d9)) is Element of (i -tuples_on E)

    proof

      let F be Function of [:D, D9:], E;

      let z be Tuple of i, D;

      reconsider r = (F [:] (z,d9)) as FinSequence of E by Th81;

      ( len z) = i by CARD_1:def 7;

      then ( len r) = i by Th82;

      hence thesis by Th90;

    end;

    theorem :: FINSEQ_2:123

    ((i + j) |-> x) = ((i |-> x) ^ (j |-> x))

    proof

      

       A0: j is Nat by TARSKI: 1;

      defpred P[ Nat] means ((i + $1) |-> x) = ((i |-> x) ^ ($1 |-> x));

      

       A1: for j be Nat st P[j] holds P[(j + 1)]

      proof

        let j be Nat such that

         A2: ((i + j) |-> x) = ((i |-> x) ^ (j |-> x));

        

        thus ((i + (j + 1)) |-> x) = (((i + j) + 1) |-> x)

        .= (((i + j) |-> x) ^ <*x*>) by Th58

        .= ((i |-> x) ^ ((j |-> x) ^ <*x*>)) by A2, FINSEQ_1: 32

        .= ((i |-> x) ^ ((j + 1) |-> x)) by Th58;

      end;

      ((i + 0 ) |-> x) = ((i |-> x) ^ {} ) by FINSEQ_1: 34

      .= ((i |-> x) ^ ( 0 |-> x));

      then

       A3: P[ 0 ];

      for j be Nat holds P[j] from NAT_1:sch 2( A3, A1);

      hence thesis by A0;

    end;

    theorem :: FINSEQ_2:124

    for i be natural Number, x be Tuple of i, D holds ( dom x) = ( Seg i)

    proof

      let i be natural Number;

      let x be Tuple of i, D;

      ( len x) = i by CARD_1:def 7;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: FINSEQ_2:125

    for f be Function, x,y be set st x in ( dom f) & y in ( dom f) holds (f * <*x, y*>) = <*(f . x), (f . y)*>

    proof

      let f be Function;

      let x,y be set;

      assume that

       A1: x in ( dom f) and

       A2: y in ( dom f);

      reconsider D = ( dom f), E = ( rng f) as non empty set by A1, FUNCT_1: 3;

      ( rng <*x, y*>) = {x, y} by Lm1;

      then ( rng <*x, y*>) c= D by A1, A2, ZFMISC_1: 32;

      then

      reconsider p = <*x, y*> as FinSequence of D by FINSEQ_1:def 4;

      reconsider g = f as Function of D, E by FUNCT_2:def 1, RELSET_1: 4;

      

      thus (f * <*x, y*>) = (g * p)

      .= <*(f . x), (f . y)*> by Th34;

    end;

    theorem :: FINSEQ_2:126

    for f be Function, x,y,z be set st x in ( dom f) & y in ( dom f) & z in ( dom f) holds (f * <*x, y, z*>) = <*(f . x), (f . y), (f . z)*>

    proof

      let f be Function;

      let x,y,z be set;

      assume that

       A1: x in ( dom f) and

       A2: y in ( dom f) & z in ( dom f);

      reconsider D = ( dom f), E = ( rng f) as non empty set by A1, FUNCT_1: 3;

      ( rng <*x, y, z*>) = {x, y, z} by Lm2;

      then

       A3: ( rng <*x, y, z*>) = ( {x, y} \/ {z}) by ENUMSET1: 3;

       {x, y} c= D & {z} c= D by A1, A2, ZFMISC_1: 31, ZFMISC_1: 32;

      then ( rng <*x, y, z*>) c= D by A3, XBOOLE_1: 8;

      then

      reconsider p = <*x, y, z*> as FinSequence of D by FINSEQ_1:def 4;

      reconsider g = f as Function of D, E by FUNCT_2:def 1, RELSET_1: 4;

      

      thus (f * <*x, y, z*>) = (g * p)

      .= <*(f . x), (f . y), (f . z)*> by Th35;

    end;

    theorem :: FINSEQ_2:127

    ( rng <*x1, x2*>) = {x1, x2} by Lm1;

    theorem :: FINSEQ_2:128

    ( rng <*x1, x2, x3*>) = {x1, x2, x3} by Lm2;

    begin

    theorem :: FINSEQ_2:129

    for p1,p2,q be FinSequence st p1 c= q & p2 c= q & ( len p1) = ( len p2) holds p1 = p2

    proof

      let p1,p2,q be FinSequence;

      assume that

       A1: p1 c= q and

       A2: p2 c= q and

       A3: ( len p1) = ( len p2);

      reconsider i = ( len p1) as Element of NAT ;

      

       A4: ( dom p1) = ( Seg i) & ( dom p2) = ( Seg i) by A3, FINSEQ_1:def 3;

      now

        let j be Nat;

        assume

         A5: j in ( dom p1);

        

        hence (p1 . j) = (q . j) by A1, GRFUNC_1: 2

        .= (p2 . j) by A2, A4, A5, GRFUNC_1: 2;

      end;

      hence thesis by A4;

    end;

    reserve m,n for Nat,

s,w for FinSequence of NAT ;

    theorem :: FINSEQ_2:130

    for D be non empty set, s be FinSequence of D st s <> {} holds ex w be FinSequence of D, n be Element of D st s = ( <*n*> ^ w)

    proof

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

      defpred P[ FinSequence of D] means $1 <> {} implies ex w be FinSequence of D, n be Element of D st $1 = ( <*n*> ^ w);

      

       A1: for s be FinSequence of D holds for m be Element of D st P[s] holds P[(s ^ <*m*>)]

      proof

        let s be FinSequence of D;

        let m be Element of D such that

         A2: s <> {} implies ex w be FinSequence of D, n be Element of D st s = ( <*n*> ^ w);

        assume (s ^ <*m*>) <> {} ;

        per cases ;

          suppose

           A3: s = {} ;

          reconsider w = ( <*> D) as FinSequence of D;

          take w, n = m;

          

          thus (s ^ <*m*>) = <*m*> by A3, FINSEQ_1: 34

          .= ( <*n*> ^ w) by FINSEQ_1: 34;

        end;

          suppose s <> {} ;

          then

          consider w be FinSequence of D, n be Element of D such that

           A4: s = ( <*n*> ^ w) by A2;

          take (w ^ <*m*>), n;

          thus thesis by A4, FINSEQ_1: 32;

        end;

      end;

      

       A5: P[( <*> D)];

      for p be FinSequence of D holds P[p] from IndSeqD( A5, A1);

      hence thesis;

    end;

    registration

      let D be set;

      cluster -> functional for FinSequenceSet of D;

      coherence by Def3;

    end

    definition

      let D;

      let n be natural Number;

      let d;

      :: original: |->

      redefine

      func n |-> d -> Element of (n -tuples_on D) ;

      coherence by Th110;

    end

    theorem :: FINSEQ_2:131

    for z be set holds z is Tuple of i, D iff z in (i -tuples_on D)

    proof

      let z be set;

      thus z is Tuple of i, D implies z in (i -tuples_on D) by Lm6;

      assume z in (i -tuples_on D);

      then ex s be Element of (D * ) st z = s & ( len s) = i;

      hence z is Tuple of i, D by CARD_1:def 7;

    end;

    theorem :: FINSEQ_2:132

    

     Th130: for A be set, i be Element of NAT , p be FinSequence holds p in (i -tuples_on A) iff ( len p) = i & ( rng p) c= A

    proof

      let A be set, i be Element of NAT , p be FinSequence;

      hereby

        assume p in (i -tuples_on A);

        then ex q be Element of (A * ) st p = q & ( len q) = i;

        hence ( len p) = i & ( rng p) c= A by FINSEQ_1:def 4;

      end;

      assume

       A1: ( len p) = i;

      assume ( rng p) c= A;

      then p is FinSequence of A by FINSEQ_1:def 4;

      then p in (A * ) by FINSEQ_1:def 11;

      hence thesis by A1;

    end;

    theorem :: FINSEQ_2:133

    for A be set, i be Element of NAT , p be FinSequence of A holds p in (i -tuples_on A) iff ( len p) = i

    proof

      let A be set, i be Element of NAT , p be FinSequence of A;

      ( rng p) c= A by RELAT_1:def 19;

      hence thesis by Th130;

    end;

    theorem :: FINSEQ_2:134

    for A be set, i be Element of NAT holds (i -tuples_on A) c= (A * )

    proof

      let A be set, i be Element of NAT , x be object;

      assume x in (i -tuples_on A);

      then x is FinSequence of A by Def3;

      hence thesis by FINSEQ_1:def 11;

    end;

    theorem :: FINSEQ_2:135

    

     Th133: for A be set, x be object holds x in (1 -tuples_on A) iff ex a be set st a in A & x = <*a*>

    proof

      let A be set, x be object;

      hereby

        assume x in (1 -tuples_on A);

        then x in { s where s be Element of (A * ) : ( len s) = 1 };

        then

        consider s be Element of (A * ) such that

         A1: x = s and

         A2: ( len s) = 1;

        take a = (s . 1);

        

         A3: ( rng <*a*>) = {a} & a in {a} by FINSEQ_1: 39, TARSKI:def 1;

        

         A4: ( rng s) c= A by RELAT_1:def 19;

        x = <*a*> by A1, A2, FINSEQ_1: 40;

        hence a in A & x = <*a*> by A1, A3, A4;

      end;

      given a be set such that

       A5: a in A and

       A6: x = <*a*>;

      reconsider A as non empty set by A5;

      reconsider a as Element of A by A5;

       <*a*> is Element of (1 -tuples_on A) by Th96;

      hence thesis by A6;

    end;

    theorem :: FINSEQ_2:136

    for A be set, a be object st <*a*> in (1 -tuples_on A) holds a in A

    proof

      let A be set, a be object;

      assume <*a*> in (1 -tuples_on A);

      then

       A1: ex a9 be set st a9 in A & <*a*> = <*a9*> by Th133;

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

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: FINSEQ_2:137

    

     Th135: for A be set, x be object holds x in (2 -tuples_on A) iff ex a,b be object st a in A & b in A & x = <*a, b*>

    proof

      let A be set, x be object;

      hereby

        assume x in (2 -tuples_on A);

        then x in { s where s be Element of (A * ) : ( len s) = 2 };

        then

        consider s be Element of (A * ) such that

         A1: x = s and

         A2: ( len s) = 2;

        reconsider a = (s . 1), b = (s . 2) as object;

        take a, b;

        

         A3: ( rng <*a, b*>) = {a, b} & a in {a, b} by Lm1, TARSKI:def 2;

        

         A4: b in {a, b} & ( rng s) c= A by RELAT_1:def 19, TARSKI:def 2;

        x = <*a, b*> by A1, A2, FINSEQ_1: 44;

        hence a in A & b in A & x = <*a, b*> by A1, A3, A4;

      end;

      given a,b be object such that

       A5: a in A and

       A6: b in A and

       A7: x = <*a, b*>;

      reconsider A as non empty set by A5;

      reconsider a, b as Element of A by A5, A6;

       <*a, b*> is Element of (2 -tuples_on A) by Th99;

      hence thesis by A7;

    end;

    theorem :: FINSEQ_2:138

    for A be set, a,b be object st <*a, b*> in (2 -tuples_on A) holds a in A & b in A

    proof

      let A be set, a,b be object;

      assume <*a, b*> in (2 -tuples_on A);

      then

       A1: ex a9,b9 be object st a9 in A & b9 in A & <*a, b*> = <*a9, b9*> by Th135;

      ( <*a, b*> . 1) = a & ( <*a, b*> . 2) = b by FINSEQ_1: 44;

      hence thesis by A1, FINSEQ_1: 44;

    end;

    theorem :: FINSEQ_2:139

    

     Th137: for A be set, x be object holds x in (3 -tuples_on A) iff ex a,b,c be object st a in A & b in A & c in A & x = <*a, b, c*>

    proof

      let A be set, x be object;

      hereby

        assume x in (3 -tuples_on A);

        then x in { s where s be Element of (A * ) : ( len s) = 3 };

        then

        consider s be Element of (A * ) such that

         A1: x = s and

         A2: ( len s) = 3;

        reconsider a = (s . 1), b = (s . 2), c = (s . 3) as object;

        take a, b, c;

        

         A3: ( rng <*a, b, c*>) = {a, b, c} & a in {a, b, c} by Lm2, ENUMSET1:def 1;

        

         A4: ( rng s) c= A by RELAT_1:def 19;

        

         A5: b in {a, b, c} & c in {a, b, c} by ENUMSET1:def 1;

        x = <*a, b, c*> by A1, A2, FINSEQ_1: 45;

        hence a in A & b in A & c in A & x = <*a, b, c*> by A1, A3, A5, A4;

      end;

      given a,b,c be object such that

       A6: a in A and

       A7: b in A & c in A and

       A8: x = <*a, b, c*>;

      reconsider A as non empty set by A6;

      reconsider a, b, c as Element of A by A6, A7;

       <*a, b, c*> is Element of (3 -tuples_on A) by Th102;

      hence thesis by A8;

    end;

    theorem :: FINSEQ_2:140

    for A be set, a,b,c be object st <*a, b, c*> in (3 -tuples_on A) holds a in A & b in A & c in A

    proof

      let A be set, a,b,c be object;

      

       A1: ( <*a, b, c*> . 3) = c by FINSEQ_1: 45;

      assume <*a, b, c*> in (3 -tuples_on A);

      then

       A2: ex a9,b9,c9 be object st a9 in A & b9 in A & c9 in A & <*a, b, c*> = <*a9, b9, c9*> by Th137;

      ( <*a, b, c*> . 1) = a & ( <*a, b, c*> . 2) = b by FINSEQ_1: 45;

      hence thesis by A2, A1, FINSEQ_1: 45;

    end;

    theorem :: FINSEQ_2:141

    for x be object holds x in (i -tuples_on A) implies x is i -element FinSequence by Lm7;

    theorem :: FINSEQ_2:142

    for A be non empty set, n holds (n -tuples_on A) c= (A * )

    proof

      let A be non empty set, n;

      defpred P[ Element of (A * )] means ( len $1) = n;

      { s where s be Element of (A * ) : P[s] } c= (A * ) from FRAENKEL:sch 10;

      hence thesis;

    end;

    theorem :: FINSEQ_2:143

    (n |-> x) = (m |-> x) implies n = m

    proof

      ( len (n |-> x)) = n by CARD_1:def 7;

      hence thesis by CARD_1:def 7;

    end;

    reserve i,j,e,u for set,

n for Nat;

    definition

      let I be set;

      let M be ManySortedSet of I;

      :: FINSEQ_2:def5

      func M # -> ManySortedSet of (I * ) means

      : Def5: for i be Element of (I * ) holds (it . i) = ( product (M * i));

      existence

      proof

        defpred P[ object, object] means ex j be Element of (I * ) st j = $1 & $2 = ( product (M * j));

        

         A1: for i be object st i in (I * ) holds ex j be object st P[i, j]

        proof

          let i be object;

          assume i in (I * );

          then

          reconsider j = i as Element of (I * );

          reconsider e = ( product (M * j)) as set;

          take e, j;

          thus thesis;

        end;

        consider f be ManySortedSet of (I * ) such that

         A2: for i be object st i in (I * ) holds P[i, (f . i)] from PBOOLE:sch 3( A1);

        take f;

        let i be Element of (I * );

        ex j be Element of (I * ) st j = i & (f . i) = ( product (M * j)) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let N1,N2 be ManySortedSet of (I * ) such that

         A3: for i be Element of (I * ) holds (N1 . i) = ( product (M * i)) and

         A4: for i be Element of (I * ) holds (N2 . i) = ( product (M * i));

        now

          let i be object;

          assume i in (I * );

          then

          reconsider e = i as Element of (I * );

          

          thus (N1 . i) = ( product (M * e)) by A3

          .= (N2 . i) by A4;

        end;

        hence thesis;

      end;

    end

    registration

      let I be set;

      let M be non-empty ManySortedSet of I;

      cluster (M # ) -> non-empty;

      coherence

      proof

        (M # ) is non-empty

        proof

          let i be object;

          assume i in (I * );

          then

          reconsider f = i as Element of (I * );

          ( product (M * f)) <> {} ;

          hence thesis by Def5;

        end;

        hence thesis;

      end;

    end

    definition

      let a be set;

      :: FINSEQ_2:def6

      func *--> a -> sequence of ( {a} * ) means

      : Def6: for n be Nat holds (it . n) = (n |-> a);

      existence

      proof

        defpred P[ Element of NAT , set] means $2 = ($1 |-> a);

        

         A1: for x be Element of NAT holds ex y be Element of ( {a} * ) st P[x, y]

        proof

          let n be Element of NAT ;

          a is Element of {a} by TARSKI:def 1;

          then (n |-> a) is FinSequence of {a} by Th61;

          then

          reconsider u = (n |-> a) as Element of ( {a} * ) by FINSEQ_1:def 11;

          take u;

          thus thesis;

        end;

        consider f be sequence of ( {a} * ) such that

         A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let n be Nat;

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

         P[nn, (f . nn)] by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be sequence of ( {a} * ) such that

         A3: for n be Nat holds (f1 . n) = (n |-> a) and

         A4: for n be Nat holds (f2 . n) = (n |-> a);

        now

          let k be Element of NAT ;

          

          thus (f1 . k) = (k |-> a) by A3

          .= (f2 . k) by A4;

        end;

        hence f1 = f2;

      end;

    end

    theorem :: FINSEQ_2:144

    

     Th142: for a,b be set holds ((a .--> b) * (n |-> a)) = (n |-> b)

    proof

      let a,b be set;

       A1:

      now

        let x be object;

        hereby

          assume x in ( dom (n |-> b));

          then

           A2: x in ( Seg n);

          hence x in ( dom (n |-> a));

          ( dom (a .--> b)) = {a} & ((n |-> a) . x) = a by A2, FUNCOP_1: 7;

          hence ((n |-> a) . x) in ( dom (a .--> b)) by TARSKI:def 1;

        end;

        assume that

         A3: x in ( dom (n |-> a)) and ((n |-> a) . x) in ( dom (a .--> b));

        x in ( Seg n) by A3;

        hence x in ( dom (n |-> b));

      end;

      now

        let x be object;

        

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

        assume x in ( dom (n |-> b));

        then

         A5: x in ( Seg n);

        

        hence ((n |-> b) . x) = b by FUNCOP_1: 7

        .= ((a .--> b) . a) by A4, FUNCOP_1: 7

        .= ((a .--> b) . ((n |-> a) . x)) by A5, FUNCOP_1: 7;

      end;

      hence thesis by A1, FUNCT_1: 10;

    end;

    theorem :: FINSEQ_2:145

    for a be set holds for M be ManySortedSet of {a} st M = (a .--> D) holds (((M # ) * ( *--> a)) . n) = ( Funcs (( Seg n),D))

    proof

      let a be set;

      let M be ManySortedSet of {a} such that

       A1: M = (a .--> D);

      a is Element of {a} by TARSKI:def 1;

      then (n |-> a) is FinSequence of {a} by Th61;

      then

       A2: (n |-> a) in ( {a} * ) by FINSEQ_1:def 11;

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

      ( dom ( *--> a)) = NAT by FUNCT_2:def 1;

      

      hence (((M # ) * ( *--> a)) . n) = ((M # ) . (( *--> a) . nn)) by FUNCT_1: 13

      .= ((M # ) . (nn |-> a)) by Def6

      .= ( product ((a .--> D) * (n |-> a))) by A1, A2, Def5

      .= ( product (n |-> D)) by Th142

      .= ( Funcs (( Seg n),D)) by CARD_3: 11;

    end;

    registration

      let i be natural Number;

      cluster (i |-> 0 ) -> empty-yielding;

      coherence ;

    end

    registration

      let D be set;

      cluster -> FinSequence-membered for FinSequenceSet of D;

      coherence

      proof

        let A be FinSequenceSet of D;

        let x be object;

        thus thesis by Def3;

      end;

    end

    definition

      let D be set;

      let F be FinSequenceSet of D, f be sequence of F, n be natural Number;

      :: original: .

      redefine

      func f . n -> FinSequence of D ;

      coherence

      proof

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

        (f . n) is Element of F;

        hence thesis;

      end;

    end