funct_7.miz



    begin

    reserve a,x,y for object,

A,B for set,

l,m,n for Nat;

    theorem :: FUNCT_7:1

    for f be Function, X be set st ( rng f) c= X holds (( id X) * f) = f

    proof

      let f be Function, X be set;

      assume ( rng f) c= X;

      then

      reconsider g = f as Function of ( dom f), X by FUNCT_2: 2;

      (( id X) * g) = g by FUNCT_2: 17;

      hence thesis;

    end;

    theorem :: FUNCT_7:2

    for X be set, Y be non empty set, f be Function of X, Y st f is one-to-one holds for B be Subset of X, C be Subset of Y st C c= (f .: B) holds (f " C) c= B

    proof

      let X be set, Y be non empty set, f be Function of X, Y such that

       A1: f is one-to-one;

      let B be Subset of X, C be Subset of Y;

      assume C c= (f .: B);

      then

       A2: (f " C) c= (f " (f .: B)) by RELAT_1: 143;

      (f " (f .: B)) c= B by A1, FUNCT_1: 82;

      hence thesis by A2;

    end;

    theorem :: FUNCT_7:3

    

     Th3: for X,Y be non empty set, f be Function of X, Y st f is one-to-one holds for x be Element of X, A be Subset of X st (f . x) in (f .: A) holds x in A

    proof

      let X,Y be non empty set, f be Function of X, Y such that

       A1: f is one-to-one;

      let x be Element of X, A be Subset of X;

      assume (f . x) in (f .: A);

      then ex y be Element of X st y in A & (f . y) = (f . x) by FUNCT_2: 65;

      hence thesis by A1, FUNCT_2: 19;

    end;

    theorem :: FUNCT_7:4

    

     Th4: for X,Y be non empty set, f be Function of X, Y st f is one-to-one holds for x be Element of X, A be Subset of X, B be Subset of Y st (f . x) in ((f .: A) \ B) holds x in (A \ (f " B))

    proof

      let X,Y be non empty set, f be Function of X, Y such that

       A1: f is one-to-one;

      let x be Element of X, A be Subset of X, B be Subset of Y;

      assume

       A2: (f . x) in ((f .: A) \ B);

       A3:

      now

        assume x in (f " B);

        then (f . x) in B by FUNCT_1:def 7;

        hence contradiction by A2, XBOOLE_0:def 5;

      end;

      (f . x) in (f .: A) by A2, XBOOLE_0:def 5;

      then x in A by A1, Th3;

      hence thesis by A3, XBOOLE_0:def 5;

    end;

    theorem :: FUNCT_7:5

    for X,Y be non empty set, f be Function of X, Y st f is one-to-one holds for y be Element of Y, A be Subset of X, B be Subset of Y st y in ((f .: A) \ B) holds ((f " ) . y) in (A \ (f " B))

    proof

      let X,Y be non empty set, f be Function of X, Y such that

       A1: f is one-to-one;

      let y be Element of Y, A be Subset of X, B be Subset of Y;

      assume

       A2: y in ((f .: A) \ B);

      then

       A3: y in (f .: A) by XBOOLE_0:def 5;

      

       A4: (f .: A) c= ( rng f) by RELAT_1: 111;

      then ((f " ) . y) in ( dom f) by A1, A3, FUNCT_1: 32;

      then

      reconsider x = ((f " ) . y) as Element of X;

      y = (f . x) by A1, A3, A4, FUNCT_1: 35;

      hence thesis by A1, A2, Th4;

    end;

    theorem :: FUNCT_7:6

    

     Th6: for f be Function, a be set st a in ( dom f) holds (f | {a}) = (a .--> (f . a))

    proof

      let f be Function, a be set;

      assume a in ( dom f);

      

      hence (f | {a}) = { [a, (f . a)]} by GRFUNC_1: 28

      .= (a .--> (f . a)) by ZFMISC_1: 29;

    end;

    registration

      let x,y be object;

      cluster (x .--> y) -> non empty;

      coherence ;

    end

    registration

      let x,y,a,b be object;

      cluster ((x,y) --> (a,b)) -> non empty;

      coherence ;

    end

    theorem :: FUNCT_7:7

    

     Th7: for I be set, M be ManySortedSet of I holds for i be set st i in I holds (i .--> (M . i)) = (M | {i})

    proof

      let I be set, M be ManySortedSet of I, i be set;

      assume i in I;

      then i in ( dom M) by PARTFUN1:def 2;

      hence thesis by Th6;

    end;

    theorem :: FUNCT_7:8

    for I,J be set, M be ManySortedSet of [:I, J:] holds for i,j be set st i in I & j in J holds ((i,j) :-> (M . (i,j))) = (M | [: {i}, {j}:] qua set)

    proof

      let I,J be set, M be ManySortedSet of [:I, J:];

      let i,j be set;

      assume i in I & j in J;

      then

       A1: [i, j] in [:I, J:] by ZFMISC_1: 87;

      

      thus ((i,j) :-> (M . (i,j))) = ( [i, j] .--> (M . [i, j]))

      .= (M | { [i, j]} qua set) by A1, Th7

      .= (M | [: {i}, {j}:] qua set) by ZFMISC_1: 29;

    end;

    theorem :: FUNCT_7:9

    

     Th9: for f,g,h be Function st ( rng h) c= ( dom f) holds (f * (g +* h)) = ((f * g) +* (f * h))

    proof

      let f,g,h be Function such that

       A1: ( rng h) c= ( dom f);

      

       A2: ( dom h) c= ( dom (g +* h)) by FUNCT_4: 10;

      

       A3: ( dom g) c= ( dom (g +* h)) by FUNCT_4: 10;

      

       A4: ( dom (f * (g +* h))) = (( dom (f * g)) \/ ( dom (f * h)))

      proof

        thus ( dom (f * (g +* h))) c= (( dom (f * g)) \/ ( dom (f * h)))

        proof

          let x be object;

          assume

           A5: x in ( dom (f * (g +* h)));

          then

           A6: ((g +* h) . x) in ( dom f) by FUNCT_1: 11;

          x in ( dom (g +* h)) by A5, FUNCT_1: 11;

          then

           A7: x in (( dom g) \/ ( dom h)) by FUNCT_4:def 1;

          per cases ;

            suppose

             A8: x in ( dom h);

            then (h . x) in ( dom f) by A6, FUNCT_4: 13;

            then x in ( dom (f * h)) by A8, FUNCT_1: 11;

            hence thesis by XBOOLE_0:def 3;

          end;

            suppose not x in ( dom h);

            then (g . x) in ( dom f) & x in ( dom g) by A7, A6, FUNCT_4: 11, XBOOLE_0:def 3;

            then x in ( dom (f * g)) by FUNCT_1: 11;

            hence thesis by XBOOLE_0:def 3;

          end;

        end;

        let x be object;

        assume

         A9: x in (( dom (f * g)) \/ ( dom (f * h)));

        per cases ;

          suppose

           A10: x in ( dom (f * h));

          then

           A11: (h . x) in ( dom f) by FUNCT_1: 11;

          

           A12: x in ( dom h) by A10, FUNCT_1: 11;

          then ((g +* h) . x) = (h . x) by FUNCT_4: 13;

          hence thesis by A2, A12, A11, FUNCT_1: 11;

        end;

          suppose

           A13: not x in ( dom (f * h));

          x in ( dom h) implies (h . x) in ( dom f)

          proof

            assume x in ( dom h);

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

            hence thesis by A1;

          end;

          then not x in ( dom h) by A13, FUNCT_1: 11;

          then

           A14: ((g +* h) . x) = (g . x) by FUNCT_4: 11;

          x in ( dom (f * g)) by A9, A13, XBOOLE_0:def 3;

          then (g . x) in ( dom f) & x in ( dom g) by FUNCT_1: 11;

          hence thesis by A3, A14, FUNCT_1: 11;

        end;

      end;

      now

        let x be object;

        assume

         A15: x in (( dom (f * g)) \/ ( dom (f * h)));

        thus x in ( dom (f * h)) implies ((f * (g +* h)) . x) = ((f * h) . x)

        proof

          assume x in ( dom (f * h));

          then

           A16: x in ( dom h) by FUNCT_1: 11;

          

          hence ((f * (g +* h)) . x) = (f . ((g +* h) . x)) by A2, FUNCT_1: 13

          .= (f . (h . x)) by A16, FUNCT_4: 13

          .= ((f * h) . x) by A16, FUNCT_1: 13;

        end;

        assume

         A17: not x in ( dom (f * h));

        x in ( dom h) implies (h . x) in ( dom f)

        proof

          assume x in ( dom h);

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

          hence thesis by A1;

        end;

        then

         A18: not x in ( dom h) by A17, FUNCT_1: 11;

        x in ( dom (f * g)) by A15, A17, XBOOLE_0:def 3;

        then

         A19: x in ( dom g) by FUNCT_1: 11;

        

        hence ((f * (g +* h)) . x) = (f . ((g +* h) . x)) by A3, FUNCT_1: 13

        .= (f . (g . x)) by A18, FUNCT_4: 11

        .= ((f * g) . x) by A19, FUNCT_1: 13;

      end;

      hence thesis by A4, FUNCT_4:def 1;

    end;

    theorem :: FUNCT_7:10

    

     Th10: for f,g,h be Function holds ((g +* h) * f) = ((g * f) +* (h * f))

    proof

      let f,g,h be Function;

      

       A1: ( dom ((g +* h) * f)) = (( dom (g * f)) \/ ( dom (h * f)))

      proof

        thus ( dom ((g +* h) * f)) c= (( dom (g * f)) \/ ( dom (h * f)))

        proof

          let x be object;

          assume

           A2: x in ( dom ((g +* h) * f));

          then (f . x) in ( dom (g +* h)) by FUNCT_1: 11;

          then (f . x) in (( dom g) \/ ( dom h)) by FUNCT_4:def 1;

          then

           A3: (f . x) in ( dom g) or (f . x) in ( dom h) by XBOOLE_0:def 3;

          x in ( dom f) by A2, FUNCT_1: 11;

          then x in ( dom (g * f)) or x in ( dom (h * f)) by A3, FUNCT_1: 11;

          hence thesis by XBOOLE_0:def 3;

        end;

        let x be object;

        assume x in (( dom (g * f)) \/ ( dom (h * f)));

        then

         A4: x in ( dom (g * f)) or x in ( dom (h * f)) by XBOOLE_0:def 3;

        then (f . x) in ( dom g) or (f . x) in ( dom h) by FUNCT_1: 11;

        then (f . x) in (( dom g) \/ ( dom h)) by XBOOLE_0:def 3;

        then

         A5: (f . x) in ( dom (g +* h)) by FUNCT_4:def 1;

        x in ( dom f) by A4, FUNCT_1: 11;

        hence thesis by A5, FUNCT_1: 11;

      end;

      now

        let x be object;

        assume x in (( dom (g * f)) \/ ( dom (h * f)));

        then x in ( dom (g * f)) or x in ( dom (h * f)) by XBOOLE_0:def 3;

        then

         A6: x in ( dom f) by FUNCT_1: 11;

        hereby

          assume

           A7: x in ( dom (h * f));

          then

           A8: (f . x) in ( dom h) by FUNCT_1: 11;

          

          thus (((g +* h) * f) . x) = ((g +* h) . (f . x)) by A6, FUNCT_1: 13

          .= (h . (f . x)) by A8, FUNCT_4: 13

          .= ((h * f) . x) by A7, FUNCT_1: 12;

        end;

        assume not x in ( dom (h * f));

        then

         A9: not (f . x) in ( dom h) by A6, FUNCT_1: 11;

        

        thus (((g +* h) * f) . x) = ((g +* h) . (f . x)) by A6, FUNCT_1: 13

        .= (g . (f . x)) by A9, FUNCT_4: 11

        .= ((g * f) . x) by A6, FUNCT_1: 13;

      end;

      hence thesis by A1, FUNCT_4:def 1;

    end;

    theorem :: FUNCT_7:11

    for f,g,h be Function st ( rng f) misses ( dom g) holds ((h +* g) * f) = (h * f)

    proof

      let f,g,h be Function;

      assume

       A1: ( rng f) misses ( dom g);

      

      thus ((h +* g) * f) = ((h * f) +* (g * f)) by Th10

      .= ((h * f) +* {} ) by A1, RELAT_1: 44

      .= (h * f);

    end;

    theorem :: FUNCT_7:12

    

     Th12: for A,B be set, y be set st A meets ( rng (( id B) +* (A --> y))) holds y in A

    proof

      let A,B be set, y be set;

      assume A meets ( rng (( id B) +* (A --> y)));

      then

      consider x be object such that

       A1: x in A and

       A2: x in ( rng (( id B) +* (A --> y))) by XBOOLE_0: 3;

      consider z be object such that

       A3: z in ( dom (( id B) +* (A --> y))) and

       A4: ((( id B) +* (A --> y)) . z) = x by A2, FUNCT_1:def 3;

      

       A5: z in (( dom ( id B)) \/ ( dom (A --> y))) by A3, FUNCT_4:def 1;

      per cases ;

        suppose

         A6: z in ( dom (A --> y));

        

        then y = ((A --> y) . z) by FUNCOP_1: 7

        .= x by A4, A6, FUNCT_4: 13;

        hence thesis by A1;

      end;

        suppose

         A7: not z in ( dom (A --> y));

        then

         A8: z in ( dom ( id B)) by A5, XBOOLE_0:def 3;

        x = (( id B) . z) by A4, A7, FUNCT_4: 11

        .= z by A8, FUNCT_1: 18;

        hence thesis by A1, A7;

      end;

    end;

    theorem :: FUNCT_7:13

    for x,y be set, A be set st x <> y holds not x in ( rng (( id A) +* (x .--> y)))

    proof

      let x,y be set, A be set;

      assume x <> y;

      then not y in {x} by TARSKI:def 1;

      then {x} misses ( rng (( id A) +* ( {x} --> y))) by Th12;

      hence thesis by ZFMISC_1: 48;

    end;

    theorem :: FUNCT_7:14

    for X be set, a be set, f be Function st ( dom f) = (X \/ {a}) holds f = ((f | X) +* (a .--> (f . a)))

    proof

      let X be set, a be set, f be Function;

      assume

       A1: ( dom f) = (X \/ {a});

      a in {a} by TARSKI:def 1;

      then

       A2: a in ( dom f) by A1, XBOOLE_0:def 3;

      

      thus f = ((f | X) +* (f | {a})) by A1, FUNCT_4: 70

      .= ((f | X) +* (a .--> (f . a))) by A2, Th6;

    end;

    theorem :: FUNCT_7:15

    for f be Function, X,y,z be set holds ((f +* (X --> y)) +* (X --> z)) = (f +* (X --> z))

    proof

      let f be Function, X,y,z be set;

      

       A1: ( dom (X --> z)) = X;

      

       A2: ( dom (X --> y)) = X;

      then ( dom (f +* (X --> y))) = (( dom f) \/ X) by FUNCT_4:def 1;

      

      then

       A3: ( dom ((f +* (X --> y)) +* (X --> z))) = ((( dom f) \/ X) \/ X) by A1, FUNCT_4:def 1

      .= (( dom f) \/ (X \/ X)) by XBOOLE_1: 4

      .= (( dom f) \/ X);

       A4:

      now

        let x be object;

        assume x in (( dom f) \/ X);

        per cases ;

          suppose

           A5: x in X;

          then (((f +* (X --> y)) +* (X --> z)) . x) = ((X --> z) . x) by A1, FUNCT_4: 13;

          hence (((f +* (X --> y)) +* (X --> z)) . x) = ((f +* (X --> z)) . x) by A1, A5, FUNCT_4: 13;

        end;

          suppose

           A6: not x in X;

          then (((f +* (X --> y)) +* (X --> z)) . x) = ((f +* (X --> y)) . x) by A1, FUNCT_4: 11;

          then (((f +* (X --> y)) +* (X --> z)) . x) = (f . x) by A2, A6, FUNCT_4: 11;

          hence (((f +* (X --> y)) +* (X --> z)) . x) = ((f +* (X --> z)) . x) by A1, A6, FUNCT_4: 11;

        end;

      end;

      ( dom (f +* (X --> z))) = (( dom f) \/ X) by A1, FUNCT_4:def 1;

      hence thesis by A3, A4;

    end;

    theorem :: FUNCT_7:16

     INT <> ( INT * )

    proof

      now

        

         A1: {} in 1 by CARD_1: 49, TARSKI:def 1;

        assume 1 in ( INT * );

        then ex x,y be object st {} = [x, y] by A1, RELAT_1:def 1;

        hence contradiction;

      end;

      hence thesis by INT_1:def 2;

    end;

    theorem :: FUNCT_7:17

    ( {} * ) = { {} }

    proof

      thus ( {} * ) c= { {} }

      proof

        let x be object;

        assume x in ( {} * );

        then

        reconsider f = x as FinSequence of {} by FINSEQ_1:def 11;

        now

          assume x <> {} ;

          then ex x st x in ( dom f);

          hence contradiction;

        end;

        hence thesis by ZFMISC_1: 31;

      end;

      let x be object;

      assume x in { {} };

      then

       A1: x = {} by TARSKI:def 1;

      ( rng {} ) = {} ;

      then x is FinSequence of {} by A1, FINSEQ_1:def 4;

      hence thesis by FINSEQ_1:def 11;

    end;

    theorem :: FUNCT_7:18

    

     Th18: for x be object holds <*x*> in (A * ) iff x in A

    proof

      let x be object;

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

      then {x} c= A iff <*x*> is FinSequence of A by FINSEQ_1:def 4;

      hence thesis by FINSEQ_1:def 11, ZFMISC_1: 31;

    end;

    theorem :: FUNCT_7:19

    (A * ) c= (B * ) implies A c= B

    proof

      assume

       A1: (A * ) c= (B * );

      let x be object;

      assume x in A;

      then <*x*> in (A * ) by Th18;

      hence thesis by A1, Th18;

    end;

    theorem :: FUNCT_7:20

    for A be Subset of NAT st for n, m st n in A & m < n holds m in A holds A is Cardinal

    proof

      let A be Subset of NAT such that

       A1: for n, m st n in A & m < n holds m in A;

      per cases ;

        suppose A = {} ;

        hence thesis;

      end;

        suppose that

         A2: A <> {} and

         A3: ex m be Nat st for n be Nat st n in A holds n <= m;

        defpred P[ set] means $1 in A;

        consider M be Nat such that

         A4: for n be Nat st P[n] holds n <= M by A3;

        ex m be Element of NAT st P[m] by A2, SUBSET_1: 4;

        then

         A5: ex m be Nat st P[m];

        consider m be Nat such that

         A6: P[m] and

         A7: for n be Nat st P[n] holds n <= m from NAT_1:sch 6( A4, A5);

        A = { l where l be Nat : l < (m + 1) }

        proof

          thus A c= { l where l be Nat : l < (m + 1) }

          proof

            let x be object;

            assume

             A8: x in A;

            then

            reconsider l = x as Nat;

            l <= m by A7, A8;

            then l < (m + 1) by NAT_1: 13;

            hence thesis;

          end;

          let x be object;

          assume x in { l where l be Nat : l < (m + 1) };

          then

          consider l be Nat such that

           A9: x = l and

           A10: l < (m + 1);

          reconsider l as Nat;

          l <= m by A10, NAT_1: 13;

          then l < m or l = m by XXREAL_0: 1;

          hence thesis by A1, A6, A9;

        end;

        hence thesis by AXIOMS: 4;

      end;

        suppose

         A11: for m be Nat holds ex n be Nat st n in A & n > m;

         NAT c= A

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider m = x as Nat;

          ex n be Nat st n in A & n > m by A11;

          hence thesis by A1;

        end;

        hence thesis by XBOOLE_0:def 10;

      end;

    end;

    theorem :: FUNCT_7:21

    for A be finite set, X be non empty Subset-Family of A holds ex C be Element of X st for B be Element of X holds B c= C implies B = C

    proof

      let A be finite set, X be non empty Subset-Family of A;

      reconsider D = ( COMPLEMENT X) as non empty Subset-Family of A by SETFAM_1: 32;

      consider x be set such that

       A1: x in D and

       A2: for B be set st B in D holds x c= B implies B = x by FINSET_1: 6;

      reconsider x as Subset of A by A1;

      reconsider C = (x ` ) as Element of X by A1, SETFAM_1:def 7;

      take C;

      let B be Element of X such that

       A3: B c= C;

      ((B ` ) ` ) = B;

      then (B ` ) in D by SETFAM_1:def 7;

      then (B ` ) = x by A2, A3, SUBSET_1: 16;

      hence thesis;

    end;

    theorem :: FUNCT_7:22

    

     Th22: for p,q be FinSequence st ( len p) = (( len q) + 1) holds for i be Nat holds i in ( dom q) iff i in ( dom p) & (i + 1) in ( dom p)

    proof

      let p,q be FinSequence;

      assume

       A1: ( len p) = (( len q) + 1);

      let i be Nat;

      hereby

        assume

         A2: i in ( dom q);

        then

         A3: i >= 1 by FINSEQ_3: 25;

        

         A4: i <= ( len q) by A2, FINSEQ_3: 25;

        ( len q) <= ( len p) by A1, NAT_1: 11;

        then

         A5: (i + 1) >= 1 & i <= ( len p) by A4, NAT_1: 11, XXREAL_0: 2;

        (i + 1) <= ( len p) by A1, A4, XREAL_1: 6;

        hence i in ( dom p) & (i + 1) in ( dom p) by A3, A5, FINSEQ_3: 25;

      end;

      assume that

       A6: i in ( dom p) and

       A7: (i + 1) in ( dom p);

      (i + 1) <= ( len p) by A7, FINSEQ_3: 25;

      then

       A8: i <= ( len q) by A1, XREAL_1: 6;

      i >= 1 by A6, FINSEQ_3: 25;

      hence thesis by A8, FINSEQ_3: 25;

    end;

    registration

      cluster Function-yielding non empty non-empty for FinSequence;

      existence

      proof

        take p = <* <* 0 qua set*>*>;

        

         A1: ( dom p) = {1} & (p . 1) = <* 0 *> by FINSEQ_1: 2, FINSEQ_1: 38, FINSEQ_1: 40;

        thus p is Function-yielding;

        thus p is non empty;

        let x be object;

        assume x in ( dom p);

        hence thesis by A1, TARSKI:def 1;

      end;

    end

    registration

      cluster empty -> Function-yielding for Function;

      coherence ;

    end

    registration

      let n be Nat, f be Function;

      cluster (n |-> f) -> Function-yielding;

      coherence ;

    end

    registration

      let p,q be Function-yielding FinSequence;

      cluster (p ^ q) -> Function-yielding;

      coherence

      proof

        let x be object;

        assume

         A1: x in ( dom (p ^ q));

        then

        reconsider i = x as Nat;

        per cases ;

          suppose i in ( dom p);

          then (p . i) = ((p ^ q) . i) by FINSEQ_1:def 7;

          hence thesis;

        end;

          suppose not i in ( dom p);

          then

          consider j be Nat such that

           A2: j in ( dom q) & i = (( len p) + j) by A1, FINSEQ_1: 25;

          (q . j) = ((p ^ q) . i) by A2, FINSEQ_1:def 7;

          hence thesis;

        end;

      end;

    end

    theorem :: FUNCT_7:23

    

     Th23: for p,q be FinSequence st (p ^ q) is Function-yielding holds p is Function-yielding & q is Function-yielding

    proof

      let p,q be FinSequence;

      assume

       A1: for x be object st x in ( dom (p ^ q)) holds ((p ^ q) . x) is Function;

      hereby

        let x be object;

        assume

         A2: x in ( dom p);

        then ((p ^ q) . x) = (p . x) by FINSEQ_1:def 7;

        hence (p . x) is Function by A1, A2, FINSEQ_3: 22;

      end;

      let x be object;

      assume

       A3: x in ( dom q);

      then

      reconsider i = x as Nat;

      ((p ^ q) . (( len p) + i)) = (q . x) by A3, FINSEQ_1:def 7;

      hence thesis by A1, A3, FINSEQ_1: 28;

    end;

    begin

    scheme :: FUNCT_7:sch1

    Kappa2D { X,Y,Z() -> non empty set , F( Element of X(), Element of Y()) -> object } :

ex f be Function of [:X(), Y():], Z() st for x be Element of X(), y be Element of Y() holds (f . (x,y)) = F(x,y)

      provided

       A1: for x be Element of X(), y be Element of Y() holds F(x,y) in Z();

      deffunc G( Element of [:X(), Y():]) = F(`1,`2);

      

       A2: for p be Element of [:X(), Y():] holds G(p) in Z() by A1;

      consider f be Function of [:X(), Y():], Z() such that

       A3: for p be Element of [:X(), Y():] holds (f . p) = G(p) from FUNCT_2:sch 8( A2);

      take f;

      let x be Element of X(), y be Element of Y();

      ( [x, y] `1 ) = x & ( [x, y] `2 ) = y;

      hence thesis by A3;

    end;

    scheme :: FUNCT_7:sch2

    FinMono { A() -> set , D() -> non empty set , F,G( object) -> object } :

{ F(d) where d be Element of D() : G(d) in A() } is finite

      provided

       A1: A() is finite

       and

       A2: for d1,d2 be Element of D() st G(d1) = G(d2) holds d1 = d2;

      per cases ;

        suppose

         A3: A() = {} ;

        now

          set a = the Element of { F(d) where d be Element of D() : G(d) in A() };

          assume { F(d) where d be Element of D() : G(d) in A() } <> {} ;

          then a in { F(d) where d be Element of D() : G(d) in A() };

          then ex d be Element of D() st a = F(d) & G(d) in A();

          hence contradiction by A3;

        end;

        hence thesis;

      end;

        suppose A() <> {} ;

        then

        reconsider D = A() as non empty set;

        defpred R[ set] means ex d be Element of D() st $1 = G(d);

        set B = { d where d be Element of D() : G(d) in D }, C = { a where a be Element of D : R[a] };

        

         A4: { F(d) where d be Element of D() : G(d) in A() } = { F(d) where d be Element of D() : d in B }

        proof

          thus { F(d) where d be Element of D() : G(d) in A() } c= { F(d) where d be Element of D() : d in B }

          proof

            let x be object;

            assume x in { F(d) where d be Element of D() : G(d) in A() };

            then

            consider d9 be Element of D() such that

             A5: x = F(d9) and

             A6: G(d9) in A();

            d9 in B by A6;

            hence thesis by A5;

          end;

          let x be object;

          assume x in { F(d) where d be Element of D() : d in B };

          then

          consider d1 be Element of D() such that

           A7: x = F(d1) and

           A8: d1 in B;

          ex d3 be Element of D() st d3 = d1 & G(d3) in D by A8;

          hence thesis by A7;

        end;

        

         A9: (C,B) are_equipotent

        proof

          take Z = the set of all [G(d), d] where d be Element of D();

          hereby

            let x be object;

            assume x in C;

            then

            consider a be Element of D such that

             A10: a = x and

             A11: ex d be Element of D() st a = G(d);

            consider d be Element of D() such that

             A12: a = G(d) by A11;

            reconsider d as object;

            take d;

            thus d in B & [x, d] in Z by A10, A12;

          end;

          hereby

            let y be object;

            assume y in B;

            then

            consider d be Element of D() such that

             A13: d = y & G(d) in D;

            reconsider x = G(d) as object;

            take x;

            thus x in C & [x, y] in Z by A13;

          end;

          let x,y,z,u be object;

          assume [x, y] in Z;

          then

          consider d1 be Element of D() such that

           A14: [x, y] = [G(d1), d1];

          assume [z, u] in Z;

          then

          consider d2 be Element of D() such that

           A15: [z, u] = [G(d2), d2];

          

           A16: z = G(d2) & u = d2 by A15, XTUPLE_0: 1;

          x = G(d1) & y = d1 by A14, XTUPLE_0: 1;

          hence thesis by A2, A16;

        end;

        C is Subset of D from DOMAIN_1:sch 7;

        then C is finite by A1, FINSET_1: 1;

        then

         A17: B is finite by A9, CARD_1: 38;

        { F(d) where d be Element of D() : d in B } is finite from FRAENKEL:sch 21( A17);

        hence thesis by A4;

      end;

    end;

    scheme :: FUNCT_7:sch3

    CardMono { A() -> set , D() -> non empty set , G( object) -> object } :

(A(),{ d where d be Element of D() : G(d) in A() }) are_equipotent

      provided

       A1: for x be set st x in A() holds ex d be Element of D() st x = G(d)

       and

       A2: for d1,d2 be Element of D() st G(d1) = G(d2) holds d1 = d2;

      set D = { d where d be Element of D() : G(d) in A() };

      per cases ;

        suppose

         A3: A() = {} ;

        now

          set a = the Element of D;

          assume D <> {} ;

          then a in D;

          then ex d be Element of D() st a = d & G(d) in A();

          hence contradiction by A3;

        end;

        hence thesis by A3;

      end;

        suppose A() <> {} ;

        then

        reconsider A = A() as non empty set;

        (A,D) are_equipotent

        proof

          take Z = the set of all [G(d), d] where d be Element of D();

          hereby

            let x be object;

            assume

             A4: x in A;

            then

            consider d be Element of D() such that

             A5: x = G(d) by A1;

            reconsider d as object;

            take d;

            thus d in D by A4, A5;

            thus [x, d] in Z by A5;

          end;

          hereby

            let y be object;

            assume y in D;

            then

            consider d be Element of D() such that

             A6: d = y & G(d) in A;

            reconsider x = G(d) as object;

            take x;

            thus x in A & [x, y] in Z by A6;

          end;

          let x,y,z,u be object;

          assume [x, y] in Z;

          then

          consider d1 be Element of D() such that

           A7: [x, y] = [G(d1), d1];

          assume [z, u] in Z;

          then

          consider d2 be Element of D() such that

           A8: [z, u] = [G(d2), d2];

          

           A9: z = G(d2) & u = d2 by A8, XTUPLE_0: 1;

          x = G(d1) & y = d1 by A7, XTUPLE_0: 1;

          hence thesis by A2, A9;

        end;

        hence thesis;

      end;

    end;

    scheme :: FUNCT_7:sch4

    CardMono9 { A() -> set , D() -> non empty set , G( object) -> object } :

(A(),{ G(d) where d be Element of D() : d in A() }) are_equipotent

      provided

       A1: A() c= D()

       and

       A2: for d1,d2 be Element of D() st G(d1) = G(d2) holds d1 = d2;

      per cases ;

        suppose

         A3: A() = {} ;

        now

          set a = the Element of { G(d) where d be Element of D() : d in A() };

          assume { G(d) where d be Element of D() : d in A() } <> {} ;

          then a in { G(d) where d be Element of D() : d in A() };

          then ex d be Element of D() st a = G(d) & d in A();

          hence contradiction by A3;

        end;

        hence thesis by A3;

      end;

        suppose A() <> {} ;

        then

        reconsider A = A() as non empty set;

        set D = { G(d) where d be Element of D() : d in A };

        (A,D) are_equipotent

        proof

          take Z = the set of all [d, G(d)] where d be Element of D();

          hereby

            let x be object;

            assume

             A4: x in A;

            then

            reconsider d = x as Element of D() by A1;

            reconsider y = G(d) as object;

            take y;

            thus y in D by A4;

            thus [x, y] in Z;

          end;

          hereby

            let y be object;

            assume y in D;

            then

            consider d be Element of D() such that

             A5: G(d) = y & d in A;

            reconsider d as object;

            take d;

            thus d in A & [d, y] in Z by A5;

          end;

          let x,y,z,u be object;

          assume [x, y] in Z;

          then

          consider d1 be Element of D() such that

           A6: [x, y] = [d1, G(d1)];

          assume [z, u] in Z;

          then

          consider d2 be Element of D() such that

           A7: [z, u] = [d2, G(d2)];

          

           A8: z = d2 & u = G(d2) by A7, XTUPLE_0: 1;

          x = d1 & y = G(d1) by A6, XTUPLE_0: 1;

          hence thesis by A2, A8;

        end;

        hence thesis;

      end;

    end;

    scheme :: FUNCT_7:sch5

    FuncSeqInd { P[ object] } :

for p be Function-yielding FinSequence holds P[p]

      provided

       A1: P[ {} ]

       and

       A2: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)];

      defpred R[ FinSequence] means $1 is Function-yielding implies P[$1];

      

       A3: for p be FinSequence, x be object st R[p] holds R[(p ^ <*x*>)]

      proof

        let p be FinSequence, x be object such that

         A4: p is Function-yielding implies P[p] and

         A5: (p ^ <*x*>) is Function-yielding;

        

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

        p is Function-yielding & <*x*> is Function-yielding by A5, Th23;

        hence thesis by A2, A4, A6;

      end;

      

       A7: R[ {} ] by A1;

      for p be FinSequence holds R[p] from FINSEQ_1:sch 3( A7, A3);

      hence thesis;

    end;

    begin

    definition

      ::$Canceled

      let f,g be Function;

      let A be set;

      :: FUNCT_7:def2

      pred f,g equal_outside A means (f | (( dom f) \ A)) = (g | (( dom g) \ A));

    end

    ::$Canceled

    theorem :: FUNCT_7:25

    for f be Function, A be set holds (f,f) equal_outside A;

    theorem :: FUNCT_7:26

    

     Th25: for f,g be Function, A be set st (f,g) equal_outside A holds (g,f) equal_outside A;

    theorem :: FUNCT_7:27

    for f,g,h be Function, A be set st (f,g) equal_outside A & (g,h) equal_outside A holds (f,h) equal_outside A;

    theorem :: FUNCT_7:28

    

     Th27: for f,g be Function, A be set st (f,g) equal_outside A holds (( dom f) \ A) = (( dom g) \ A)

    proof

      let f,g be Function, A be set;

      assume

       A1: (f | (( dom f) \ A)) = (g | (( dom g) \ A));

      

      thus (( dom f) \ A) = (( dom f) /\ (( dom f) \ A)) by XBOOLE_1: 28

      .= ( dom (f | (( dom f) \ A))) by RELAT_1: 61

      .= (( dom g) /\ (( dom g) \ A)) by A1, RELAT_1: 61

      .= (( dom g) \ A) by XBOOLE_1: 28;

    end;

    theorem :: FUNCT_7:29

    

     Th28: for f,g be Function, A be set st ( dom g) c= A holds (f,(f +* g)) equal_outside A

    proof

      let f,g be Function, A be set;

      assume

       A1: ( dom g) c= A;

      

       A2: (( dom (f +* g)) \ A) = ((( dom f) \/ ( dom g)) \ A) by FUNCT_4:def 1

      .= ((( dom f) \ A) \/ (( dom g) \ A)) by XBOOLE_1: 42

      .= ((( dom f) \ A) \/ {} ) by A1, XBOOLE_1: 37

      .= (( dom f) \ A);

      (( dom f) \ A) misses A by XBOOLE_1: 79;

      then (( dom f) \ A) misses ( dom g) by A1, XBOOLE_1: 63;

      hence (f | (( dom f) \ A)) = ((f +* g) | (( dom (f +* g)) \ A)) by A2, FUNCT_4: 72;

    end;

    definition

      let f be Function, i,x be object;

      :: FUNCT_7:def3

      func f +* (i,x) -> Function equals

      : Def2: (f +* (i .--> x)) if i in ( dom f)

      otherwise f;

      correctness ;

    end

    theorem :: FUNCT_7:30

    

     Th29: for f be Function, d,i be object holds ( dom (f +* (i,d))) = ( dom f)

    proof

      let f be Function, x,i be object;

      per cases ;

        suppose

         A1: i in ( dom f);

        then

         A2: {i} c= ( dom f) by ZFMISC_1: 31;

        

        thus ( dom (f +* (i,x))) = ( dom (f +* (i .--> x))) by A1, Def2

        .= (( dom f) \/ ( dom (i .--> x))) by FUNCT_4:def 1

        .= (( dom f) \/ {i})

        .= ( dom f) by A2, XBOOLE_1: 12;

      end;

        suppose not i in ( dom f);

        hence thesis by Def2;

      end;

    end;

    registration

      let f be empty Function, i,x be object;

      cluster (f +* (i,x)) -> empty;

      coherence

      proof

        ( dom f) is empty;

        then ( dom (f +* (i,x))) is empty by Th29;

        hence thesis;

      end;

    end

    registration

      let f be non empty Function, i,x be object;

      cluster (f +* (i,x)) -> non empty;

      coherence

      proof

        ( dom f) is non empty;

        then ( dom (f +* (i,x))) is non empty by Th29;

        hence thesis;

      end;

    end

    theorem :: FUNCT_7:31

    

     Th30: for f be Function, d,i be object st i in ( dom f) holds ((f +* (i,d)) . i) = d

    proof

      let f be Function, d,i be object;

      

       A1: i in ( dom (i .--> d)) by TARSKI:def 1;

      assume i in ( dom f);

      

      hence ((f +* (i,d)) . i) = ((f +* (i .--> d)) . i) by Def2

      .= ((i .--> d) . i) by A1, FUNCT_4: 13

      .= d by FUNCOP_1: 72;

    end;

    theorem :: FUNCT_7:32

    

     Th31: for f be Function, d,i,j be object st i <> j holds ((f +* (i,d)) . j) = (f . j)

    proof

      let f be Function, d,i,j be object such that

       A1: i <> j;

      

       A2: not j in ( dom (i .--> d)) by A1, TARSKI:def 1;

      per cases ;

        suppose i in ( dom f);

        

        hence ((f +* (i,d)) . j) = ((f +* (i .--> d)) . j) by Def2

        .= (f . j) by A2, FUNCT_4: 11;

      end;

        suppose not i in ( dom f);

        hence thesis by Def2;

      end;

    end;

    theorem :: FUNCT_7:33

    for f be Function, d,e,i,j be set st i <> j holds ((f +* (i,d)) +* (j,e)) = ((f +* (j,e)) +* (i,d))

    proof

      let f be Function, d,e,i,j be set such that

       A1: i <> j;

      per cases ;

        suppose that

         A2: i in ( dom f) and

         A3: j in ( dom f);

        

         A4: i in ( dom (f +* (j,e))) by A2, Th29;

        

         A5: ( dom (i .--> d)) = {i} & ( dom (j .--> e)) = {j};

        j in ( dom (f +* (i,d))) by A3, Th29;

        

        hence ((f +* (i,d)) +* (j,e)) = ((f +* (i,d)) +* (j .--> e)) by Def2

        .= ((f +* (i .--> d)) +* (j .--> e)) by A2, Def2

        .= (f +* ((i .--> d) +* (j .--> e))) by FUNCT_4: 14

        .= (f +* ((j .--> e) +* (i .--> d))) by A1, A5, FUNCT_4: 35, ZFMISC_1: 11

        .= ((f +* (j .--> e)) +* (i .--> d)) by FUNCT_4: 14

        .= ((f +* (j,e)) +* (i .--> d)) by A3, Def2

        .= ((f +* (j,e)) +* (i,d)) by A4, Def2;

      end;

        suppose that i in ( dom f) and

         A6: not j in ( dom f);

         not j in ( dom (f +* (i,d))) by A6, Th29;

        

        hence ((f +* (i,d)) +* (j,e)) = (f +* (i,d)) by Def2

        .= ((f +* (j,e)) +* (i,d)) by A6, Def2;

      end;

        suppose that

         A7: not i in ( dom f) and j in ( dom f);

        

         A8: not i in ( dom (f +* (j,e))) by A7, Th29;

        

        thus ((f +* (i,d)) +* (j,e)) = (f +* (j,e)) by A7, Def2

        .= ((f +* (j,e)) +* (i,d)) by A8, Def2;

      end;

        suppose that

         A9: not i in ( dom f) and

         A10: not j in ( dom f);

        

         A11: not i in ( dom (f +* (j,e))) by A9, Th29;

         not j in ( dom (f +* (i,d))) by A10, Th29;

        

        hence ((f +* (i,d)) +* (j,e)) = (f +* (i,d)) by Def2

        .= f by A9, Def2

        .= (f +* (j,e)) by A10, Def2

        .= ((f +* (j,e)) +* (i,d)) by A11, Def2;

      end;

    end;

    theorem :: FUNCT_7:34

    for f be Function, d,e,i be set holds ((f +* (i,d)) +* (i,e)) = (f +* (i,e))

    proof

      let f be Function, d,e,i be set;

      

       A1: ( dom (i .--> d)) = {i}

      .= ( dom (i .--> e));

      per cases ;

        suppose

         A2: i in ( dom f);

        then i in ( dom (f +* (i,d))) by Th29;

        

        hence ((f +* (i,d)) +* (i,e)) = ((f +* (i,d)) +* (i .--> e)) by Def2

        .= ((f +* (i .--> d)) +* (i .--> e)) by A2, Def2

        .= (f +* ((i .--> d) +* (i .--> e))) by FUNCT_4: 14

        .= (f +* (i .--> e)) by A1, FUNCT_4: 19

        .= (f +* (i,e)) by A2, Def2;

      end;

        suppose not i in ( dom f);

        hence thesis by Def2;

      end;

    end;

    theorem :: FUNCT_7:35

    

     Th34: for f be Function, i be set holds (f +* (i,(f . i))) = f

    proof

      let f be Function, i be set;

      per cases ;

        suppose

         A1: i in ( dom f);

        then

         A2: (i .--> (f . i)) = (f | {i}) by Th6;

        

        thus (f +* (i,(f . i))) = (f +* (i .--> (f . i))) by A1, Def2

        .= f by A2, FUNCT_4: 75;

      end;

        suppose not i in ( dom f);

        hence thesis by Def2;

      end;

    end;

    registration

      let f be FinSequence, i,x be object;

      cluster (f +* (i,x)) -> FinSequence-like;

      coherence

      proof

        ( dom (f +* (i,x))) = ( dom f) by Th29

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

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    definition

      let D be set, f be FinSequence of D, i be Nat, d be Element of D;

      :: original: +*

      redefine

      func f +* (i,d) -> FinSequence of D ;

      coherence

      proof

        per cases ;

          suppose

           A1: i in ( dom f);

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

          then {d} c= D by ZFMISC_1: 31;

          then

           A2: (( rng f) \/ ( rng (i .--> d))) = (( rng f) \/ {d}) & (( rng f) \/ {d}) c= D by FUNCOP_1: 8, XBOOLE_1: 8;

          (f +* (i,d)) = (f +* (i .--> d)) by A1, Def2;

          then ( rng (f +* (i,d))) c= (( rng f) \/ ( rng (i .--> d))) by FUNCT_4: 17;

          then ( rng (f +* (i,d))) c= D by A2;

          hence thesis by FINSEQ_1:def 4;

        end;

          suppose not i in ( dom f);

          hence thesis by Def2;

        end;

      end;

    end

    theorem :: FUNCT_7:36

    for D be non empty set, f be FinSequence of D, d be Element of D, i be Nat st i in ( dom f) holds ((f +* (i,d)) /. i) = d

    proof

      let D be non empty set, f be FinSequence of D, d be Element of D, i be Nat;

      assume

       A1: i in ( dom f);

      then i in ( dom (f +* (i,d))) by Th29;

      

      hence ((f +* (i,d)) /. i) = ((f +* (i,d)) . i) by PARTFUN1:def 6

      .= d by A1, Th30;

    end;

    theorem :: FUNCT_7:37

    for D be non empty set, f be FinSequence of D, d be Element of D, i,j be Nat st i <> j & j in ( dom f) holds ((f +* (i,d)) /. j) = (f /. j)

    proof

      let D be non empty set, f be FinSequence of D, d be Element of D, i,j be Nat such that

       A1: i <> j and

       A2: j in ( dom f);

      j in ( dom (f +* (i,d))) by A2, Th29;

      

      hence ((f +* (i,d)) /. j) = ((f +* (i,d)) . j) by PARTFUN1:def 6

      .= (f . j) by A1, Th31

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

    end;

    theorem :: FUNCT_7:38

    for D be non empty set, f be FinSequence of D, d,e be Element of D, i be Nat holds (f +* (i,(f /. i))) = f

    proof

      let D be non empty set, f be FinSequence of D, d,e be Element of D, i be Nat;

      per cases ;

        suppose i in ( dom f);

        

        hence (f +* (i,(f /. i))) = (f +* (i,(f . i))) by PARTFUN1:def 6

        .= f by Th34;

      end;

        suppose not i in ( dom f);

        hence thesis by Def2;

      end;

    end;

    begin

    definition

      let X be set;

      let p be Function-yielding FinSequence;

      :: FUNCT_7:def4

      func compose (p,X) -> Function means

      : Def3: ex f be ManySortedFunction of NAT st it = (f . ( len p)) & (f . 0 ) = ( id X) & for i be Nat st (i + 1) in ( dom p) holds for g,h be Function st g = (f . i) & h = (p . (i + 1)) holds (f . (i + 1)) = (h * g);

      uniqueness

      proof

        let g1,g2 be Function;

        given f1 be ManySortedFunction of NAT such that

         A1: g1 = (f1 . ( len p)) and

         A2: (f1 . 0 ) = ( id X) and

         A3: for i be Nat st (i + 1) in ( dom p) holds for g,h be Function st g = (f1 . i) & h = (p . (i + 1)) holds (f1 . (i + 1)) = (h * g);

        given f2 be ManySortedFunction of NAT such that

         A4: g2 = (f2 . ( len p)) and

         A5: (f2 . 0 ) = ( id X) and

         A6: for i be Nat st (i + 1) in ( dom p) holds for g,h be Function st g = (f2 . i) & h = (p . (i + 1)) holds (f2 . (i + 1)) = (h * g);

        defpred R[ Nat] means $1 <= ( len p) implies (f1 . $1) = (f2 . $1) & (f1 . $1) is Function;

        

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

        proof

          let i be Nat such that

           A8: i <= ( len p) implies (f1 . i) = (f2 . i) & (f1 . i) is Function and

           A9: (i + 1) <= ( len p);

          reconsider h = (p . (i + 1)) as Function;

          reconsider g = (f1 . i) as Function;

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

          then

           A10: (i + 1) in ( dom p) by A9, FINSEQ_3: 25;

          then (f1 . (i + 1)) = (h * g) by A3;

          hence thesis by A6, A8, A9, A10, NAT_1: 13;

        end;

        

         A11: R[ 0 ] by A2, A5;

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

        hence thesis by A1, A4;

      end;

      correctness

      proof

        reconsider e = 0 as Function;

        defpred P[ Nat, set, set] means not $2 is Function & $3 = e or $2 is Function & for g,h be Function st g = $2 & h = (p . ($1 + 1)) holds $3 = (h * g);

        

         A12: for n be Nat holds for x be set holds ex y be set st P[n, x, y]

        proof

          let n be Nat, x be set;

          reconsider h = (p . (n + 1)) as Function;

          per cases ;

            suppose x is Function;

            then

            reconsider g = x as Function;

            take (h * g);

            thus thesis;

          end;

            suppose

             A13: not x is Function;

            take 0 ;

            thus thesis by A13;

          end;

        end;

        consider f be Function such that

         A14: ( dom f) = NAT & (f . 0 ) = ( id X) and

         A15: for n be Nat holds P[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 1( A12);

        defpred P[ Nat] means (f . $1) is Function;

        

         A16: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat;

          reconsider h = (p . (i + 1)) as Function;

          assume (f . i) is Function;

          then

          reconsider g = (f . i) as Function;

          (f . (i + 1)) = (h * g) by A15;

          hence thesis;

        end;

        

         A17: P[ 0 ] by A14;

        

         A18: for i be Nat holds P[i] from NAT_1:sch 2( A17, A16);

        then

        reconsider F = (f . ( len p)) as Function;

        f is Function-yielding by A14, A18;

        then

        reconsider f as ManySortedFunction of NAT by A14, PARTFUN1:def 2, RELAT_1:def 18;

        take F;

        take f;

        thus F = (f . ( len p)) & (f . 0 ) = ( id X) by A14;

        let i be Nat;

        thus thesis by A15;

      end;

    end

    definition

      let p be Function-yielding FinSequence;

      let x be object;

      :: FUNCT_7:def5

      func apply (p,x) -> FinSequence means

      : Def4: ( len it ) = (( len p) + 1) & (it . 1) = x & for i be Nat, f be Function st i in ( dom p) & f = (p . i) holds (it . (i + 1)) = (f . (it . i));

      existence

      proof

        defpred P[ Nat, set, set] means ex f be Function st f = (p . $1) & $3 = (f . $2);

        

         A1: for i be Nat st 1 <= i & i < (( len p) + 1) holds for x be set holds ex y be set st P[i, x, y]

        proof

          let i be Nat;

          assume 1 <= i;

          assume i < (( len p) + 1);

          reconsider f = (p . i) as Function;

          let x be set;

          take (f . x), f;

          thus thesis;

        end;

        consider q be FinSequence such that

         A2: ( len q) = (( len p) + 1) & ((q . 1) = x or (( len p) + 1) = 0 ) and

         A3: for i be Nat st 1 <= i & i < (( len p) + 1) holds P[i, (q . i), (q . (i + 1))] from RECDEF_1:sch 3( A1);

        take q;

        thus ( len q) = (( len p) + 1) & (q . 1) = x by A2;

        let i be Nat, f be Function;

        assume

         A4: i in ( dom p);

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

        then

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

        i >= 1 by A4, FINSEQ_3: 25;

        then ex f be Function st f = (p . i) & (q . (i + 1)) = (f . (q . i)) by A3, A5;

        hence thesis;

      end;

      correctness

      proof

        let q1,q2 be FinSequence such that

         A6: ( len q1) = (( len p) + 1) and

         A7: (q1 . 1) = x and

         A8: for i be Nat, f be Function st i in ( dom p) & f = (p . i) holds (q1 . (i + 1)) = (f . (q1 . i)) and

         A9: ( len q2) = (( len p) + 1) and

         A10: (q2 . 1) = x and

         A11: for i be Nat, f be Function st i in ( dom p) & f = (p . i) holds (q2 . (i + 1)) = (f . (q2 . i));

        defpred P[ Nat] means $1 in ( dom q1) implies (q1 . $1) = (q2 . $1);

        

         A12: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat such that

           A13: i in ( dom q1) implies (q1 . i) = (q2 . i) and

           A14: (i + 1) in ( dom q1);

          (i + 1) <= ( len q1) by A14, FINSEQ_3: 25;

          then

           A15: i <= ( len p) by A6, XREAL_1: 6;

          per cases ;

            suppose i = 0 ;

            hence thesis by A7, A10;

          end;

            suppose

             A16: i > 0 ;

            reconsider f = (p . i) as Function;

            i >= ( 0 + 1) by A16, NAT_1: 13;

            then

             A17: i in ( dom p) by A15, FINSEQ_3: 25;

            

            hence (q1 . (i + 1)) = (f . (q2 . i)) by A6, A8, A13, Th22

            .= (q2 . (i + 1)) by A11, A17;

          end;

        end;

        

         A18: P[ 0 ] by FINSEQ_3: 25;

        

         A19: for i be Nat holds P[i] from NAT_1:sch 2( A18, A12);

        ( dom q1) = ( dom q2) by A6, A9, FINSEQ_3: 29;

        hence thesis by A19;

      end;

    end

    reserve X,Y for set,

x for object,

p,q for Function-yielding FinSequence,

f,g,h for Function;

    theorem :: FUNCT_7:39

    

     Th38: ( compose ( {} ,X)) = ( id X)

    proof

      ex f be ManySortedFunction of NAT st ( compose ( {} ,X)) = (f . 0 ) & (f . 0 ) = ( id X) & for i be Nat st (i + 1) in ( dom {} ) holds for g,h be Function st g = (f . i) & h = ( {} . (i + 1)) holds (f . (i + 1)) = (h * g) by Def3, CARD_1: 27;

      hence thesis;

    end;

    theorem :: FUNCT_7:40

    

     Th39: ( apply ( {} ,x)) = <*x*>

    proof

      ( len ( apply ( {} ,x))) = ( 0 + 1) & (( apply ( {} ,x)) . 1) = x by Def4, CARD_1: 27;

      hence thesis by FINSEQ_1: 40;

    end;

    theorem :: FUNCT_7:41

    

     Th40: ( compose ((p ^ <*f*>),X)) = (f * ( compose (p,X)))

    proof

      

       A1: f = ((p ^ <*f*>) . (( len p) + 1)) by FINSEQ_1: 42;

      ( len <*f*>) = 1 by FINSEQ_1: 40;

      then

       A2: ( len (p ^ <*f*>)) = (( len p) + 1) by FINSEQ_1: 22;

      consider ff be ManySortedFunction of NAT such that

       A3: ( compose ((p ^ <*f*>),X)) = (ff . ( len (p ^ <*f*>))) and

       A4: (ff . 0 ) = ( id X) and

       A5: for i be Nat st (i + 1) in ( dom (p ^ <*f*>)) holds for g,h be Function st g = (ff . i) & h = ((p ^ <*f*>) . (i + 1)) holds (ff . (i + 1)) = (h * g) by Def3;

      reconsider g = (ff . ( len p)) as Function;

      

       A6: ( dom p) c= ( dom (p ^ <*f*>)) by FINSEQ_1: 26;

      now

        let i be Nat;

        assume

         A7: (i + 1) in ( dom p);

        let g,h be Function;

        assume that

         A8: g = (ff . i) and

         A9: h = (p . (i + 1));

        h = ((p ^ <*f*>) . (i + 1)) by A7, A9, FINSEQ_1:def 7;

        hence (ff . (i + 1)) = (h * g) by A5, A6, A7, A8;

      end;

      then

       A10: g = ( compose (p,X)) by A4, Def3;

      1 in ( Seg 1) & ( dom <*f*>) = ( Seg 1) by FINSEQ_1: 2, FINSEQ_1: 38, TARSKI:def 1;

      hence thesis by A3, A5, A10, A2, A1, FINSEQ_1: 28;

    end;

    theorem :: FUNCT_7:42

    

     Th41: ( apply ((p ^ <*f*>),x)) = (( apply (p,x)) ^ <*(f . (( apply (p,x)) . (( len p) + 1)))*>)

    proof

      defpred P[ Nat] means $1 in ( dom ( apply (p,x))) implies (( apply ((p ^ <*f*>),x)) . $1) = (( apply (p,x)) . $1);

      

       A1: ( len ( apply (p,x))) = (( len p) + 1) by Def4;

      

       A2: (( apply (p,x)) . 1) = x by Def4;

      

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

      proof

        let i be Nat such that

         A4: i in ( dom ( apply (p,x))) implies (( apply ((p ^ <*f*>),x)) . i) = (( apply (p,x)) . i) and

         A5: (i + 1) in ( dom ( apply (p,x)));

        

         A6: (i + 1) <= ( len ( apply (p,x))) by A5, FINSEQ_3: 25;

        then

         A7: i <= ( len ( apply (p,x))) by NAT_1: 13;

        

         A8: i <= ( len p) by A1, A6, XREAL_1: 6;

        per cases ;

          suppose i = 0 ;

          hence thesis by A2, Def4;

        end;

          suppose

           A9: i > 0 ;

          reconsider g = (p . i) as Function;

          

           A10: i >= ( 0 + 1) by A9, NAT_1: 13;

          then

           A11: i in ( dom p) by A8, FINSEQ_3: 25;

          then ( dom p) c= ( dom (p ^ <*f*>)) & g = ((p ^ <*f*>) . i) by FINSEQ_1: 26, FINSEQ_1:def 7;

          then (( apply ((p ^ <*f*>),x)) . (i + 1)) = (g . (( apply ((p ^ <*f*>),x)) . i)) by A11, Def4;

          hence thesis by A4, A7, A10, A11, Def4, FINSEQ_3: 25;

        end;

      end;

      

       A12: P[ 0 ] by FINSEQ_3: 25;

      

       A13: for i be Nat holds P[i] from NAT_1:sch 2( A12, A3);

      ( len <*f*>) = 1 by FINSEQ_1: 40;

      then

       A14: ( len (p ^ <*f*>)) = (( len p) + 1) by FINSEQ_1: 22;

      

       A15: (( len p) + 1) >= 1 by NAT_1: 11;

      then

       A16: ((p ^ <*f*>) . (( len p) + 1)) = f & (( len p) + 1) in ( dom (p ^ <*f*>)) by A14, FINSEQ_1: 42, FINSEQ_3: 25;

      

       A17: (( len p) + 1) in ( dom ( apply (p,x))) by A1, A15, FINSEQ_3: 25;

       A18:

      now

        let i be Nat;

        assume i in ( dom <*(f . (( apply (p,x)) . (( len p) + 1)))*>);

        then i in ( Seg 1) by FINSEQ_1: 38;

        then

         A19: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

        then (f . (( apply ((p ^ <*f*>),x)) . (( len p) + i))) = (( apply ((p ^ <*f*>),x)) . (( len ( apply (p,x))) + i)) & (( apply ((p ^ <*f*>),x)) . (( len p) + i)) = (( apply (p,x)) . (( len p) + i)) by A1, A16, A17, A13, Def4;

        hence (( apply ((p ^ <*f*>),x)) . (( len ( apply (p,x))) + i)) = ( <*(f . (( apply (p,x)) . (( len p) + 1)))*> . i) by A19, FINSEQ_1: 40;

      end;

      ( len ( apply ((p ^ <*f*>),x))) = (( len (p ^ <*f*>)) + 1) by Def4;

      then ( len <*(f . (( apply (p,x)) . (( len p) + 1)))*>) = 1 & ( dom ( apply ((p ^ <*f*>),x))) = ( Seg (( len ( apply (p,x))) + 1)) by A1, A14, FINSEQ_1: 40, FINSEQ_1:def 3;

      hence thesis by A13, A18, FINSEQ_1:def 7;

    end;

    theorem :: FUNCT_7:43

    ( compose (( <*f*> ^ p),X)) = (( compose (p,(f .: X))) * (f | X))

    proof

      defpred R[ Function-yielding FinSequence] means ( compose (( <*f*> ^ $1),X)) = (( compose ($1,(f .: X))) * (f | X));

      

       A1: for p be Function-yielding FinSequence st R[p] holds for f be Function holds R[(p ^ <*f*>)]

      proof

        let p be Function-yielding FinSequence such that

         A2: ( compose (( <*f*> ^ p),X)) = (( compose (p,(f .: X))) * (f | X));

        let g be Function;

        

        thus ( compose (( <*f*> ^ (p ^ <*g*>)),X)) = ( compose ((( <*f*> ^ p) ^ <*g*>),X)) by FINSEQ_1: 32

        .= (g * ( compose (( <*f*> ^ p),X))) by Th40

        .= ((g * ( compose (p,(f .: X)))) * (f | X)) by A2, RELAT_1: 36

        .= (( compose ((p ^ <*g*>),(f .: X))) * (f | X)) by Th40;

      end;

      ( <*f*> ^ {} ) = <*f*> & ( {} ^ <*f*>) = <*f*> by FINSEQ_1: 34;

      

      then ( compose (( <*f*> ^ {} ),X)) = (f * ( compose ( {} ,X))) by Th40

      .= (f * ( id X)) by Th38

      .= (f | X) by RELAT_1: 65

      .= (( id ( rng (f | X))) * (f | X)) by RELAT_1: 54

      .= (( id (f .: X)) * (f | X)) by RELAT_1: 115

      .= (( compose ( {} ,(f .: X))) * (f | X)) by Th38;

      then

       A3: R[ {} ];

      for p holds R[p] from FuncSeqInd( A3, A1);

      hence thesis;

    end;

    theorem :: FUNCT_7:44

    ( apply (( <*f*> ^ p),x)) = ( <*x*> ^ ( apply (p,(f . x))))

    proof

      defpred P[ Function-yielding FinSequence] means ( apply (( <*f*> ^ $1),x)) = ( <*x*> ^ ( apply ($1,(f . x))));

      

       A1: ( len {} ) = 0 ;

      

       A2: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)]

      proof

        let p such that

         A3: ( apply (( <*f*> ^ p),x)) = ( <*x*> ^ ( apply (p,(f . x))));

        let g be Function;

        set p9 = ( <*f*> ^ p);

        

         A4: ( len ( apply (p,(f . x)))) = (( len p) + 1) by Def4;

        ( len <*f*>) = 1 by FINSEQ_1: 40;

        then

         A5: ( len p9) = (( len p) + 1) by FINSEQ_1: 22;

        then ( len p9) >= 1 by NAT_1: 11;

        then ( len <*x*>) = 1 & ( len p9) in ( dom ( apply (p,(f . x)))) by A4, A5, FINSEQ_1: 40, FINSEQ_3: 25;

        then

         A6: (( apply (p9,x)) . (1 + ( len p9))) = (( apply (p,(f . x))) . (( len p) + 1)) by A3, A5, FINSEQ_1:def 7;

        ( apply ((p9 ^ <*g*>),x)) = (( apply (p9,x)) ^ <*(g . (( apply (p9,x)) . (( len p9) + 1)))*>) by Th41;

        

        hence ( apply (( <*f*> ^ (p ^ <*g*>)),x)) = (( <*x*> ^ ( apply (p,(f . x)))) ^ <*(g . (( apply (p,(f . x))) . (( len p) + 1)))*>) by A3, A6, FINSEQ_1: 32

        .= ( <*x*> ^ (( apply (p,(f . x))) ^ <*(g . (( apply (p,(f . x))) . (( len p) + 1)))*>)) by FINSEQ_1: 32

        .= ( <*x*> ^ ( apply ((p ^ <*g*>),(f . x)))) by Th41;

      end;

      ( <*f*> ^ {} ) = <*f*> & ( {} ^ <*f*>) = <*f*> by FINSEQ_1: 34;

      

      then ( apply (( <*f*> ^ {} ),x)) = (( apply ( {} ,x)) ^ <*(f . (( apply ( {} ,x)) . ( 0 + 1)))*>) by A1, Th41

      .= ( <*x*> ^ <*(f . (( apply ( {} ,x)) . 1))*>) by Th39

      .= ( <*x*> ^ <*(f . ( <*x*> . 1))*>) by Th39

      .= ( <*x*> ^ <*(f . x)*>) by FINSEQ_1: 40

      .= ( <*x*> ^ ( apply ( {} ,(f . x)))) by Th39;

      then

       A7: P[ {} ];

      for p holds P[p] from FuncSeqInd( A7, A2);

      hence thesis;

    end;

    theorem :: FUNCT_7:45

    

     Th44: ( compose ( <*f*>,X)) = (f * ( id X))

    proof

       <*f*> = ( {} ^ <*f*>) by FINSEQ_1: 34;

      

      hence ( compose ( <*f*>,X)) = (f * ( compose ( {} ,X))) by Th40

      .= (f * ( id X)) by Th38;

    end;

    theorem :: FUNCT_7:46

    ( dom f) c= X implies ( compose ( <*f*>,X)) = f

    proof

      ( compose ( <*f*>,X)) = (f * ( id X)) by Th44;

      hence thesis by RELAT_1: 51;

    end;

    theorem :: FUNCT_7:47

    

     Th46: ( apply ( <*f*>,x)) = <*x, (f . x)*>

    proof

      

       A1: ( <*x*> . ( 0 + 1)) = x by FINSEQ_1: 40;

      

       A2: ( apply ( {} ,x)) = <*x*> & ( len {} ) = 0 by Th39;

      

      thus ( apply ( <*f*>,x)) = ( apply (( {} ^ <*f*>),x)) by FINSEQ_1: 34

      .= ( <*x*> ^ <*(f . x)*>) by A2, A1, Th41

      .= <*x, (f . x)*> by FINSEQ_1:def 9;

    end;

    theorem :: FUNCT_7:48

    ( rng ( compose (p,X))) c= Y implies ( compose ((p ^ q),X)) = (( compose (q,Y)) * ( compose (p,X)))

    proof

      assume

       A1: ( rng ( compose (p,X))) c= Y;

      defpred P[ Function-yielding FinSequence] means ( compose ((p ^ $1),X)) = (( compose ($1,Y)) * ( compose (p,X)));

      

       A2: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)]

      proof

        let q such that

         A3: ( compose ((p ^ q),X)) = (( compose (q,Y)) * ( compose (p,X)));

        let f;

        

        thus ( compose ((p ^ (q ^ <*f*>)),X)) = ( compose (((p ^ q) ^ <*f*>),X)) by FINSEQ_1: 32

        .= (f * ( compose ((p ^ q),X))) by Th40

        .= ((f * ( compose (q,Y))) * ( compose (p,X))) by A3, RELAT_1: 36

        .= (( compose ((q ^ <*f*>),Y)) * ( compose (p,X))) by Th40;

      end;

      ( compose ((p ^ {} ),X)) = ( compose (p,X)) by FINSEQ_1: 34

      .= (( id Y) * ( compose (p,X))) by A1, RELAT_1: 53

      .= (( compose ( {} ,Y)) * ( compose (p,X))) by Th38;

      then

       A4: P[ {} ];

      for q holds P[q] from FuncSeqInd( A4, A2);

      hence thesis;

    end;

    theorem :: FUNCT_7:49

    

     Th48: (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1)) = (( apply (q,(( apply (p,x)) . (( len p) + 1)))) . (( len q) + 1))

    proof

      defpred P[ Function-yielding FinSequence] means (( apply ((p ^ $1),x)) . (( len (p ^ $1)) + 1)) = (( apply ($1,(( apply (p,x)) . (( len p) + 1)))) . (( len $1) + 1));

      

       A1: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)]

      proof

        set y = (( apply (p,x)) . (( len p) + 1));

        let q such that

         A2: (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1)) = (( apply (q,(( apply (p,x)) . (( len p) + 1)))) . (( len q) + 1));

        let f be Function;

        

         A3: ( len <*f*>) = 1 by FINSEQ_1: 40;

        then

         A4: ( len ((p ^ q) ^ <*f*>)) = (( len (p ^ q)) + 1) by FINSEQ_1: 22;

        

         A5: ( len (q ^ <*f*>)) = (( len q) + 1) by A3, FINSEQ_1: 22;

        

         A6: ( apply ((q ^ <*f*>),y)) = (( apply (q,y)) ^ <*(f . (( apply (q,y)) . (( len q) + 1)))*>) & ( len ( apply (q,y))) = (( len q) + 1) by Def4, Th41;

        

         A7: ( len ( apply ((p ^ q),x))) = (( len (p ^ q)) + 1) by Def4;

        (p ^ (q ^ <*f*>)) = ((p ^ q) ^ <*f*>) & ( apply (((p ^ q) ^ <*f*>),x)) = (( apply ((p ^ q),x)) ^ <*(f . (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1)))*>) by Th41, FINSEQ_1: 32;

        

        hence (( apply ((p ^ (q ^ <*f*>)),x)) . (( len (p ^ (q ^ <*f*>))) + 1)) = (f . (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1))) by A7, A4, FINSEQ_1: 42

        .= (( apply ((q ^ <*f*>),(( apply (p,x)) . (( len p) + 1)))) . (( len (q ^ <*f*>)) + 1)) by A2, A6, A5, FINSEQ_1: 42;

      end;

      ( apply ( {} ,(( apply (p,x)) . (( len p) + 1)))) = <*(( apply (p,x)) . (( len p) + 1))*> & (p ^ {} ) = p by Th39, FINSEQ_1: 34;

      then

       A8: P[ {} ] by FINSEQ_1: 40;

      for q holds P[q] from FuncSeqInd( A8, A1);

      hence thesis;

    end;

    theorem :: FUNCT_7:50

    ( apply ((p ^ q),x)) = (( apply (p,x)) $^ ( apply (q,(( apply (p,x)) . (( len p) + 1)))))

    proof

      defpred P[ Function-yielding FinSequence] means ( apply ((p ^ $1),x)) = (( apply (p,x)) $^ ( apply ($1,(( apply (p,x)) . (( len p) + 1)))));

      

       A1: ( len ( apply (p,x))) = (( len p) + 1) by Def4;

      then

      consider r be FinSequence, y be object such that

       A2: ( apply (p,x)) = (r ^ <*y*>) by CARD_1: 27, FINSEQ_1: 46;

      

       A3: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)]

      proof

        let q such that

         A4: ( apply ((p ^ q),x)) = (( apply (p,x)) $^ ( apply (q,(( apply (p,x)) . (( len p) + 1)))));

        

         A5: (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1)) = (( apply (q,(( apply (p,x)) . (( len p) + 1)))) . (( len q) + 1)) by Th48;

        let f;

        

         A6: ( len ( apply (q,(( apply (p,x)) . (( len p) + 1))))) = (( len q) + 1) by Def4;

        

         A7: ( len ( apply ((q ^ <*f*>),(( apply (p,x)) . (( len p) + 1))))) = (( len (q ^ <*f*>)) + 1) by Def4;

        

        thus ( apply ((p ^ (q ^ <*f*>)),x)) = ( apply (((p ^ q) ^ <*f*>),x)) by FINSEQ_1: 32

        .= (( apply ((p ^ q),x)) ^ <*(f . (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1)))*>) by Th41

        .= ((r ^ ( apply (q,(( apply (p,x)) . (( len p) + 1))))) ^ <*(f . (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1)))*>) by A2, A4, A6, CARD_1: 27, REWRITE1: 2

        .= (r ^ (( apply (q,(( apply (p,x)) . (( len p) + 1)))) ^ <*(f . (( apply ((p ^ q),x)) . (( len (p ^ q)) + 1)))*>)) by FINSEQ_1: 32

        .= (r ^ ( apply ((q ^ <*f*>),(( apply (p,x)) . (( len p) + 1))))) by A5, Th41

        .= (( apply (p,x)) $^ ( apply ((q ^ <*f*>),(( apply (p,x)) . (( len p) + 1))))) by A2, A7, CARD_1: 27, REWRITE1: 2;

      end;

      ( len <*y*>) = 1 by FINSEQ_1: 40;

      then (( len p) + 1) = (( len r) + 1) by A1, A2, FINSEQ_1: 22;

      then

       A8: (( apply (p,x)) . (( len p) + 1)) = y by A2, FINSEQ_1: 42;

      ( apply ((p ^ {} ),x)) = ( apply (p,x)) by FINSEQ_1: 34

      .= (( apply (p,x)) $^ <*(( apply (p,x)) . (( len p) + 1))*>) by A2, A8, REWRITE1: 2

      .= (( apply (p,x)) $^ ( apply ( {} ,(( apply (p,x)) . (( len p) + 1))))) by Th39;

      then

       A9: P[ {} ];

      for q holds P[q] from FuncSeqInd( A9, A3);

      hence thesis;

    end;

    theorem :: FUNCT_7:51

    

     Th50: ( compose ( <*f, g*>,X)) = ((g * f) * ( id X))

    proof

       <*f, g*> = ( <*f*> ^ <*g*>) by FINSEQ_1:def 9;

      

      hence ( compose ( <*f, g*>,X)) = (g * ( compose ( <*f*>,X))) by Th40

      .= (g * (f * ( id X))) by Th44

      .= ((g * f) * ( id X)) by RELAT_1: 36;

    end;

    theorem :: FUNCT_7:52

    ( dom f) c= X or ( dom (g * f)) c= X implies ( compose ( <*f, g*>,X)) = (g * f)

    proof

      ( compose ( <*f, g*>,X)) = ((g * f) * ( id X)) & ((g * f) * ( id X)) = (g * (f * ( id X))) by Th50, RELAT_1: 36;

      hence thesis by RELAT_1: 51;

    end;

    theorem :: FUNCT_7:53

    

     Th52: ( apply ( <*f, g*>,x)) = <*x, (f . x), (g . (f . x))*>

    proof

      

       A1: ( apply ( <*f*>,x)) = <*x, (f . x)*> & ( len <*f*>) = 1 by Th46, FINSEQ_1: 40;

      

      thus ( apply ( <*f, g*>,x)) = ( apply (( <*f*> ^ <*g*>),x)) by FINSEQ_1:def 9

      .= ( <*x, (f . x)*> ^ <*(g . ( <*x, (f . x)*> . (1 + 1)))*>) by A1, Th41

      .= ( <*x, (f . x)*> ^ <*(g . (f . x))*>) by FINSEQ_1: 44

      .= <*x, (f . x), (g . (f . x))*> by FINSEQ_1: 43;

    end;

    theorem :: FUNCT_7:54

    

     Th53: ( compose ( <*f, g, h*>,X)) = (((h * g) * f) * ( id X))

    proof

       <*f, g, h*> = ( <*f, g*> ^ <*h*>) by FINSEQ_1: 43;

      

      hence ( compose ( <*f, g, h*>,X)) = (h * ( compose ( <*f, g*>,X))) by Th40

      .= (h * ((g * f) * ( id X))) by Th50

      .= ((h * (g * f)) * ( id X)) by RELAT_1: 36

      .= (((h * g) * f) * ( id X)) by RELAT_1: 36;

    end;

    theorem :: FUNCT_7:55

    ( dom f) c= X or ( dom (g * f)) c= X or ( dom ((h * g) * f)) c= X implies ( compose ( <*f, g, h*>,X)) = ((h * g) * f)

    proof

      

       A1: ((h * g) * (f * ( id X))) = (h * (g * (f * ( id X)))) & (g * (f * ( id X))) = ((g * f) * ( id X)) by RELAT_1: 36;

      

       A2: (h * (g * f)) = ((h * g) * f) by RELAT_1: 36;

      ( compose ( <*f, g, h*>,X)) = (((h * g) * f) * ( id X)) & (((h * g) * f) * ( id X)) = ((h * g) * (f * ( id X))) by Th53, RELAT_1: 36;

      hence thesis by A1, A2, RELAT_1: 51;

    end;

    theorem :: FUNCT_7:56

    ( apply ( <*f, g, h*>,x)) = ( <*x*> ^ <*(f . x), (g . (f . x)), (h . (g . (f . x)))*>)

    proof

      

       A1: ( apply ( <*f, g*>,x)) = <*x, (f . x), (g . (f . x))*> & ( len <*f, g*>) = 2 by Th52, FINSEQ_1: 44;

      

      thus ( apply ( <*f, g, h*>,x)) = ( apply (( <*f, g*> ^ <*h*>),x)) by FINSEQ_1: 43

      .= ( <*x, (f . x), (g . (f . x))*> ^ <*(h . ( <*x, (f . x), (g . (f . x))*> . (2 + 1)))*>) by A1, Th41

      .= ( <*x, (f . x), (g . (f . x))*> ^ <*(h . (g . (f . x)))*>) by FINSEQ_1: 45

      .= (( <*x*> ^ <*(f . x), (g . (f . x))*>) ^ <*(h . (g . (f . x)))*>) by FINSEQ_1: 43

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

      .= ( <*x*> ^ <*(f . x), (g . (f . x)), (h . (g . (f . x)))*>) by FINSEQ_1: 43;

    end;

    definition

      let F be FinSequence;

      :: FUNCT_7:def6

      func firstdom F -> set means

      : Def5: it is empty if F is empty

      otherwise it = ( proj1 (F . 1));

      correctness ;

      :: FUNCT_7:def7

      func lastrng F -> set means

      : Def6: it is empty if F is empty

      otherwise it = ( proj2 (F . ( len F)));

      correctness ;

    end

    theorem :: FUNCT_7:57

    

     Th56: ( firstdom {} ) = {} & ( lastrng {} ) = {} by Def5, Def6;

    theorem :: FUNCT_7:58

    

     Th57: for p be FinSequence holds ( firstdom ( <*f*> ^ p)) = ( dom f) & ( lastrng (p ^ <*f*>)) = ( rng f)

    proof

      let p be FinSequence;

      

      thus ( firstdom ( <*f*> ^ p)) = ( proj1 (( <*f*> ^ p) . 1)) by Def5

      .= ( dom f) by FINSEQ_1: 41;

      ( len <*f*>) = 1 by FINSEQ_1: 40;

      then ( len (p ^ <*f*>)) = (( len p) + 1) by FINSEQ_1: 22;

      

      hence ( lastrng (p ^ <*f*>)) = ( proj2 ((p ^ <*f*>) . (( len p) + 1))) by Def6

      .= ( rng f) by FINSEQ_1: 42;

    end;

    theorem :: FUNCT_7:59

    

     Th58: for p be Function-yielding FinSequence st p <> {} holds ( rng ( compose (p,X))) c= ( lastrng p)

    proof

      defpred P[ Function-yielding FinSequence] means $1 <> {} implies ( rng ( compose ($1,X))) c= ( lastrng $1);

      

       A1: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)]

      proof

        let q;

        assume q <> {} implies ( rng ( compose (q,X))) c= ( lastrng q);

        let f;

        assume (q ^ <*f*>) <> {} ;

        ( compose ((q ^ <*f*>),X)) = (f * ( compose (q,X))) by Th40;

        then ( rng ( compose ((q ^ <*f*>),X))) c= ( rng f) by RELAT_1: 26;

        hence thesis by Th57;

      end;

      

       A2: P[ {} ];

      thus for p holds P[p] from FuncSeqInd( A2, A1);

    end;

    definition

      let IT be FinSequence;

      :: FUNCT_7:def8

      attr IT is FuncSeq-like means

      : Def7: ex p be FinSequence st ( len p) = (( len IT) + 1) & for i be Nat st i in ( dom IT) holds (IT . i) in ( Funcs ((p . i),(p . (i + 1))));

    end

    theorem :: FUNCT_7:60

    

     Th59: for p,q be FinSequence st (p ^ q) is FuncSeq-like holds p is FuncSeq-like & q is FuncSeq-like

    proof

      let p,q be FinSequence;

      given pq be FinSequence such that

       A1: ( len pq) = (( len (p ^ q)) + 1) and

       A2: for i be Nat st i in ( dom (p ^ q)) holds ((p ^ q) . i) in ( Funcs ((pq . i),(pq . (i + 1))));

      reconsider p1 = (pq | ( Seg (( len p) + 1))), p2 = (pq | ( Seg ( len p))) as FinSequence by FINSEQ_1: 15;

      

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

      then

       A4: ( len p) <= ( len (p ^ q)) by NAT_1: 11;

      ( len (p ^ q)) <= ( len pq) by A1, NAT_1: 11;

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

      then

       A5: ( len p2) = ( len p) by FINSEQ_1: 17;

      hereby

        take p1;

        ( len p) <= ( len (p ^ q)) by A3, NAT_1: 11;

        then (( len p) + 1) <= ( len pq) by A1, XREAL_1: 6;

        hence

         A6: ( len p1) = (( len p) + 1) by FINSEQ_1: 17;

        let i be Nat;

        assume

         A7: i in ( dom p);

        then ((p ^ q) . i) = (p . i) by FINSEQ_1:def 7;

        then

         A8: (p . i) in ( Funcs ((pq . i),(pq . (i + 1)))) by A2, A7, FINSEQ_3: 22;

        i in ( dom p1) by A6, A7, Th22;

        then

         A9: (pq . i) = (p1 . i) by FUNCT_1: 47;

        (i + 1) in ( dom p1) by A6, A7, Th22;

        hence (p . i) in ( Funcs ((p1 . i),(p1 . (i + 1)))) by A8, A9, FUNCT_1: 47;

      end;

      consider q2 be FinSequence such that

       A10: pq = (p2 ^ q2) by FINSEQ_1: 80;

      take q2;

      ( len pq) = (( len p2) + ( len q2)) by A10, FINSEQ_1: 22;

      hence ( len q2) = (( len q) + 1) by A1, A3, A5;

      let x be Nat;

      assume

       A11: x in ( dom q);

      then ((p ^ q) . (( len p) + x)) = (q . x) by FINSEQ_1:def 7;

      then

       A12: (q . x) in ( Funcs ((pq . (( len p) + x)),(pq . ((( len p) + x) + 1)))) by A2, A11, FINSEQ_1: 28;

      

       A13: (( len p) + (( len q) + 1)) = (( len p) + ( len q2)) by A1, A3, A10, A5, FINSEQ_1: 22;

      then (x + 1) in ( dom q2) by A11, Th22;

      then

       A14: (q2 . (x + 1)) = (pq . (( len p) + (x + 1))) by A10, A5, FINSEQ_1:def 7;

      x in ( dom q2) by A13, A11, Th22;

      hence thesis by A10, A5, A12, A14, FINSEQ_1:def 7;

    end;

    registration

      cluster FuncSeq-like -> Function-yielding for FinSequence;

      coherence

      proof

        let q be FinSequence;

        given p be FinSequence such that ( len p) = (( len q) + 1) and

         A1: for i be Nat st i in ( dom q) holds (q . i) in ( Funcs ((p . i),(p . (i + 1))));

        let i be object;

        assume

         A2: i in ( dom q);

        then

        reconsider i as Nat;

        (q . i) in ( Funcs ((p . i),(p . (i + 1)))) by A1, A2;

        hence thesis;

      end;

    end

    registration

      cluster empty -> FuncSeq-like for FinSequence;

      coherence

      proof

        let p be FinSequence;

        assume

         A1: p is empty;

        take q = <* {} *>;

        thus ( len q) = (( len p) + 1) by A1, FINSEQ_1: 40;

        thus thesis by A1;

      end;

    end

    registration

      let f be Function;

      cluster <*f*> -> FuncSeq-like;

      coherence

      proof

        take q = <*( dom f), ( rng f)*>;

        set p = <*f*>;

        

        thus ( len q) = (1 + 1) by FINSEQ_1: 44

        .= (( len p) + 1) by FINSEQ_1: 40;

        let i be Nat;

        assume i in ( dom p);

        then i in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then

         A1: i = 1 by TARSKI:def 1;

        then

         A2: (q . (i + 1)) = ( rng f) by FINSEQ_1: 44;

        (p . i) = f & (q . i) = ( dom f) by A1, FINSEQ_1: 40, FINSEQ_1: 44;

        hence thesis by A2, FUNCT_2:def 2;

      end;

    end

    registration

      cluster FuncSeq-like non empty non-empty for FinSequence;

      existence

      proof

        set f = the non empty Function;

        take p = <*f*>;

        thus p is FuncSeq-like;

        thus p is non empty;

        let x be object;

        assume x in ( dom p);

        then x in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

        then x = 1 by TARSKI:def 1;

        hence thesis by FINSEQ_1: 40;

      end;

    end

    definition

      mode FuncSequence is FuncSeq-like FinSequence;

    end

    theorem :: FUNCT_7:61

    

     Th60: for p be FuncSequence st p <> {} holds ( dom ( compose (p,X))) = (( firstdom p) /\ X)

    proof

      defpred P[ Function-yielding FinSequence] means $1 is FuncSequence & $1 <> {} implies ( dom ( compose ($1,X))) = (( firstdom $1) /\ X);

      

       A1: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)]

      proof

        let q;

        assume

         A2: q is FuncSequence & q <> {} implies ( dom ( compose (q,X))) = (( firstdom q) /\ X);

        let f;

        assume that

         A3: (q ^ <*f*>) is FuncSequence and (q ^ <*f*>) <> {} ;

        

         A4: ( compose ((q ^ <*f*>),X)) = (f * ( compose (q,X))) by Th40;

        per cases ;

          suppose q = {} ;

          then

           A5: (q ^ <*f*>) = <*f*> by FINSEQ_1: 34;

          then

           A6: ( compose ((q ^ <*f*>),X)) = (f * ( id X)) by Th44;

          ( <*f*> ^ {} ) = <*f*> by FINSEQ_1: 34;

          then ( firstdom (q ^ <*f*>)) = ( dom f) by A5, Th57;

          hence thesis by A6, FUNCT_1: 19;

        end;

          suppose

           A7: q <> {} ;

          then

          consider y be object, s be FinSequence such that

           A8: q = ( <*y*> ^ s) and

           A9: ( len q) = (( len s) + 1) by REWRITE1: 5;

          reconsider y as set by TARSKI: 1;

          (q . 1) = y by A8, FINSEQ_1: 41;

          then

           A10: ( firstdom q) = ( proj1 y) by A8, Def5;

          

           A11: ( len q) >= 1 by A9, NAT_1: 11;

          then ( len q) in ( dom q) by FINSEQ_3: 25;

          then

           A12: ((q ^ <*f*>) . ( len q)) = (q . ( len q)) by FINSEQ_1:def 7;

          

           A13: ( rng ( compose (q,X))) c= ( lastrng q) by A7, Th58;

          consider p be FinSequence such that ( len p) = (( len (q ^ <*f*>)) + 1) and

           A14: for i be Nat st i in ( dom (q ^ <*f*>)) holds ((q ^ <*f*>) . i) in ( Funcs ((p . i),(p . (i + 1)))) by A3, Def7;

          consider r be FinSequence, x be object such that

           A15: q = (r ^ <*x*>) by A7, FINSEQ_1: 46;

          ( len <*f*>) = 1 by FINSEQ_1: 40;

          then

           A16: ( len (q ^ <*f*>)) = (( len q) + 1) by FINSEQ_1: 22;

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

          then ( len q) in ( dom (q ^ <*f*>)) by A11, FINSEQ_3: 25;

          then

           A17: ((q ^ <*f*>) . ( len q)) in ( Funcs ((p . ( len q)),(p . (( len q) + 1)))) by A14;

          ( len <*x*>) = 1 by FINSEQ_1: 40;

          then ( len q) = (( len r) + 1) by A15, FINSEQ_1: 22;

          then (q . ( len q)) = x by A15, FINSEQ_1: 42;

          then

          consider g be Function such that

           A18: x = g and ( dom g) = (p . ( len q)) and

           A19: ( rng g) c= (p . (( len q) + 1)) by A17, A12, FUNCT_2:def 2;

          

           A20: (( <*y*> ^ (s ^ <*f*>)) . 1) = y by FINSEQ_1: 41;

          (( len q) + 1) >= 1 by NAT_1: 11;

          then (( len q) + 1) in ( dom (q ^ <*f*>)) by A16, FINSEQ_3: 25;

          then

           A21: ((q ^ <*f*>) . (( len q) + 1)) in ( Funcs ((p . (( len q) + 1)),(p . ((( len q) + 1) + 1)))) by A14;

          ((q ^ <*f*>) . (( len q) + 1)) = f by FINSEQ_1: 42;

          then

           A22: ex g be Function st f = g & ( dom g) = (p . (( len q) + 1)) & ( rng g) c= (p . ((( len q) + 1) + 1)) by A21, FUNCT_2:def 2;

          (q ^ <*f*>) = ( <*y*> ^ (s ^ <*f*>)) by A8, FINSEQ_1: 32;

          then

           A23: ( firstdom (q ^ <*f*>)) = ( proj1 y) by A20, Def5;

          ( lastrng q) = ( rng g) by A15, A18, Th57;

          hence thesis by A2, A3, A4, A7, A23, A10, A19, A22, A13, Th59, RELAT_1: 27, XBOOLE_1: 1;

        end;

      end;

      

       A24: P[ {} ];

      for p be Function-yielding FinSequence holds P[p] from FuncSeqInd( A24, A1);

      hence thesis;

    end;

    theorem :: FUNCT_7:62

    

     Th61: for p be FuncSequence holds ( dom ( compose (p,( firstdom p)))) = ( firstdom p)

    proof

      let p be FuncSequence;

      per cases ;

        suppose p = {} ;

        then ( compose (p,( firstdom p))) = ( id ( firstdom p)) by Th38;

        hence thesis;

      end;

        suppose p <> {} ;

        then ( dom ( compose (p,( firstdom p)))) = (( firstdom p) /\ ( firstdom p)) by Th60;

        hence thesis;

      end;

    end;

    theorem :: FUNCT_7:63

    for p be FuncSequence, f be Function st ( rng f) c= ( firstdom p) holds ( <*f*> ^ p) is FuncSequence

    proof

      let p be FuncSequence, f be Function such that

       A1: ( rng f) c= ( firstdom p);

      consider q be FinSequence such that

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

       A3: for i be Nat st i in ( dom p) holds (p . i) in ( Funcs ((q . i),(q . (i + 1)))) by Def7;

      set r = ( <*( dom f)*> ^ q);

      

       A4: ( len <*( dom f)*>) = 1 by FINSEQ_1: 40;

      

       A5: ( len <*f*>) = 1 by FINSEQ_1: 40;

      then

       A6: ( len ( <*f*> ^ p)) = (( len p) + 1) by FINSEQ_1: 22;

       A7:

      now

        assume

         A8: p <> {} ;

        then ( len p) >= ( 0 + 1) by NAT_1: 13;

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

        then (p . 1) in ( Funcs ((q . 1),(q . (1 + 1)))) by A3;

        then ex g be Function st (p . 1) = g & ( dom g) = (q . 1) & ( rng g) c= (q . 2) by FUNCT_2:def 2;

        hence ( rng f) c= (q . 1) by A1, A8, Def5;

      end;

      ( <*f*> ^ p) is FuncSeq-like

      proof

        take r;

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

        then

         A9: 1 in ( dom q) by FINSEQ_3: 25;

        thus ( len r) = (( len ( <*f*> ^ p)) + 1) by A2, A4, A6, FINSEQ_1: 22;

        let i be Nat;

        assume

         A10: i in ( dom ( <*f*> ^ p));

        then

         A11: i >= 1 by FINSEQ_3: 25;

        

         A12: ( rng f) c= (q . 1) by A1, A7, Th56;

        

         A13: i <= (( len p) + 1) by A6, A10, FINSEQ_3: 25;

        per cases ;

          suppose

           A14: i = 1;

          then

           A15: (r . i) = ( dom f) & (( <*f*> ^ p) . i) = f by FINSEQ_1: 41;

          (r . (i + 1)) = (q . 1) by A4, A9, A14, FINSEQ_1:def 7;

          hence thesis by A12, A15, FUNCT_2:def 2;

        end;

          suppose i <> 1;

          then i > 1 by A11, XXREAL_0: 1;

          then i >= (1 + 1) by NAT_1: 13;

          then

          consider j be Nat such that

           A16: i = ((1 + 1) + j) by NAT_1: 10;

          

           A17: i = ((j + 1) + 1) by A16;

          then (j + 1) >= 1 & (j + 1) <= ( len p) by A13, NAT_1: 11, XREAL_1: 6;

          then

           A18: (j + 1) in ( dom p) by FINSEQ_3: 25;

          then

           A19: (p . (j + 1)) = (( <*f*> ^ p) . i) by A5, A17, FINSEQ_1:def 7;

          

           A20: ((j + 1) + 1) in ( dom q) by A2, A18, Th22;

          

           A21: (p . (j + 1)) in ( Funcs ((q . (j + 1)),(q . ((j + 1) + 1)))) by A3, A18;

          (j + 1) in ( dom q) by A2, A18, Th22;

          then (r . i) = (q . (j + 1)) by A4, A16, A21, FINSEQ_1:def 7;

          hence thesis by A4, A16, A21, A20, A19, FINSEQ_1:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_7:64

    for p be FuncSequence, f be Function st ( lastrng p) c= ( dom f) holds (p ^ <*f*>) is FuncSequence

    proof

      let p be FuncSequence, f be Function such that

       A1: ( lastrng p) c= ( dom f);

      consider q be FinSequence such that

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

       A3: for i be Nat st i in ( dom p) holds (p . i) in ( Funcs ((q . i),(q . (i + 1)))) by Def7;

      consider q9 be FinSequence, x be object such that

       A4: q = (q9 ^ <*x*>) by A2, CARD_1: 27, FINSEQ_1: 46;

       A5:

      now

        assume

         A6: ( len p) in ( dom p);

        then (p . ( len p)) in ( Funcs ((q . ( len p)),(q . (( len p) + 1)))) by A3;

        then

        consider g be Function such that

         A7: (p . ( len p)) = g and

         A8: ( dom g) = (q . ( len p)) and ( rng g) c= (q . (( len p) + 1)) by FUNCT_2:def 2;

        ( lastrng p) = ( rng g) by A6, A7, Def6, RELAT_1: 38;

        hence (p . ( len p)) in ( Funcs ((q . ( len p)),( dom f))) by A1, A7, A8, FUNCT_2:def 2;

      end;

      

       A9: ( <*( dom f), ( rng f)*> . 1) = ( dom f) by FINSEQ_1: 44;

      

       A10: ( <*( dom f), ( rng f)*> . 2) = ( rng f) by FINSEQ_1: 44;

      ( len <*f*>) = 1 by FINSEQ_1: 40;

      then

       A11: ( len (p ^ <*f*>)) = (( len p) + 1) by FINSEQ_1: 22;

      set r = (q9 ^ <*( dom f), ( rng f)*>);

      ( len <*( dom f), ( rng f)*>) = 2 by FINSEQ_1: 44;

      then

       A12: ( len r) = (( len q9) + (1 + 1)) by FINSEQ_1: 22;

      

       A13: ( dom <*( dom f), ( rng f)*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A14: 1 in ( dom <*( dom f), ( rng f)*>) by FINSEQ_1: 2, TARSKI:def 2;

      ( len <*x*>) = 1 by FINSEQ_1: 40;

      then

       A15: ( len q) = (( len q9) + 1) by A4, FINSEQ_1: 22;

      

       A16: 2 in ( dom <*( dom f), ( rng f)*>) by A13, FINSEQ_1: 2, TARSKI:def 2;

      (p ^ <*f*>) is FuncSeq-like

      proof

        take r;

        thus ( len r) = (( len (p ^ <*f*>)) + 1) by A2, A15, A11, A12;

        let i be Nat;

        assume

         A17: i in ( dom (p ^ <*f*>));

        then

         A18: i >= 1 by FINSEQ_3: 25;

        i <= (( len p) + 1) by A11, A17, FINSEQ_3: 25;

        then

         A19: i = (( len p) + 1) or ( len p) >= i by NAT_1: 8;

        per cases by A19, XXREAL_0: 1;

          suppose

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

          then

           A21: (r . i) = ( dom f) & ((p ^ <*f*>) . i) = f by A2, A15, A14, A9, FINSEQ_1: 42, FINSEQ_1:def 7;

          (r . (i + 1)) = ( rng f) by A2, A15, A12, A16, A10, A20, FINSEQ_1:def 7;

          hence thesis by A21, FUNCT_2:def 2;

        end;

          suppose

           A22: i = ( len p);

          then i in ( dom q9) by A2, A15, A18, FINSEQ_3: 25;

          then

           A23: (r . i) = (q9 . i) & (q9 . i) = (q . i) by A4, FINSEQ_1:def 7;

          ( len p) in ( dom p) & (r . (i + 1)) = ( dom f) by A2, A15, A14, A9, A18, A22, FINSEQ_1:def 7, FINSEQ_3: 25;

          hence thesis by A5, A22, A23, FINSEQ_1:def 7;

        end;

          suppose

           A24: i < ( len p);

          then i in ( dom q9) by A2, A15, A18, FINSEQ_3: 25;

          then

           A25: (q . i) = (q9 . i) & (q9 . i) = (r . i) by A4, FINSEQ_1:def 7;

          

           A26: (i + 1) >= 1 by NAT_1: 11;

          i in ( dom p) by A18, A24, FINSEQ_3: 25;

          then

           A27: (p . i) in ( Funcs ((q . i),(q . (i + 1)))) & (p . i) = ((p ^ <*f*>) . i) by A3, FINSEQ_1:def 7;

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

          then

           A28: (i + 1) in ( dom q9) by A2, A15, A26, FINSEQ_3: 25;

          then (q . (i + 1)) = (q9 . (i + 1)) by A4, FINSEQ_1:def 7;

          hence thesis by A28, A25, A27, FINSEQ_1:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_7:65

    for p be FuncSequence st x in ( firstdom p) & x in X holds (( apply (p,x)) . (( len p) + 1)) = (( compose (p,X)) . x)

    proof

      defpred P[ Function-yielding FinSequence] means $1 is FuncSequence & x in ( firstdom $1) & x in X implies (( apply ($1,x)) . (( len $1) + 1)) = (( compose ($1,X)) . x);

      

       A1: for p be Function-yielding FinSequence st P[p] holds for f be Function holds P[(p ^ <*f*>)]

      proof

        

         A2: ( dom ( id X)) = X;

        let p such that

         A3: p is FuncSequence & x in ( firstdom p) & x in X implies (( apply (p,x)) . (( len p) + 1)) = (( compose (p,X)) . x);

        let f;

        assume that

         A4: (p ^ <*f*>) is FuncSequence and

         A5: x in ( firstdom (p ^ <*f*>)) and

         A6: x in X;

        

         A7: p is FuncSequence by A4, Th59;

        (( id X) . x) = x by A6, FUNCT_1: 17;

        then

         A8: ((f * ( id X)) . x) = (f . x) by A6, A2, FUNCT_1: 13;

        

         A9: ( len <*f*>) = 1 by FINSEQ_1: 40;

        

         A10: ( compose ((p ^ <*f*>),X)) = (f * ( compose (p,X))) by Th40;

        

         A11: ( apply ( <*f*>,x)) = <*x, (f . x)*> & ( compose ( <*f*>,X)) = (f * ( id X)) by Th44, Th46;

        

         A12: ( apply ((p ^ <*f*>),x)) = (( apply (p,x)) ^ <*(f . (( apply (p,x)) . (( len p) + 1)))*>) by Th41;

        per cases ;

          suppose p = {} ;

          then (p ^ <*f*>) = <*f*> by FINSEQ_1: 34;

          hence thesis by A9, A11, A8, FINSEQ_1: 44;

        end;

          suppose

           A13: p <> {} ;

          then

           A14: ( dom ( compose (p,X))) = (( firstdom p) /\ X) by A7, Th60;

          

           A15: ( firstdom (p ^ <*f*>)) = ( proj1 ((p ^ <*f*>) . 1)) by Def5;

          

           A16: ( firstdom p) = ( proj1 (p . 1)) by A13, Def5;

          ( len p) >= ( 0 + 1) by A13, NAT_1: 13;

          then

           A17: 1 in ( dom p) by FINSEQ_3: 25;

          then (p . 1) = ((p ^ <*f*>) . 1) by FINSEQ_1:def 7;

          then

           A18: x in (( firstdom p) /\ X) by A5, A6, A16, A15, XBOOLE_0:def 4;

          ( len ( apply (p,x))) = (( len p) + 1) & ( len (p ^ <*f*>)) = (( len p) + 1) by A9, Def4, FINSEQ_1: 22;

          

          hence (( apply ((p ^ <*f*>),x)) . (( len (p ^ <*f*>)) + 1)) = (f . (( compose (p,X)) . x)) by A3, A4, A5, A6, A12, A16, A15, A17, Th59, FINSEQ_1: 42, FINSEQ_1:def 7

          .= (( compose ((p ^ <*f*>),X)) . x) by A10, A14, A18, FUNCT_1: 13;

        end;

      end;

      

       A19: P[ {} ] by Def5;

      for p holds P[p] from FuncSeqInd( A19, A1);

      hence thesis;

    end;

    definition

      let X,Y be set;

      :: FUNCT_7:def9

      mode FuncSequence of X,Y -> FuncSequence means

      : Def8: ( firstdom it ) = X & ( lastrng it ) c= Y;

      existence

      proof

        set f = the Function of X, Y;

        take p = <*f*>;

        

         A2: (p ^ {} ) = p & ( {} ^ p) = p by FINSEQ_1: 34;

        ( dom f) = X & ( rng f) c= Y by A1, FUNCT_2:def 1;

        hence thesis by A2, Th57;

      end;

    end

    definition

      let Y be non empty set, X be set;

      let F be FuncSequence of X, Y;

      :: original: compose

      redefine

      func compose (F,X) -> Function of X, Y ;

      coherence

      proof

        

         A1: ( firstdom F) = X by Def8;

        now

          assume F = {} ;

          then X = {} & ( compose (F,X)) = ( id X) by A1, Def5, Th38;

          hence ( rng ( compose (F,X))) = {} ;

        end;

        then

         A2: ( rng ( compose (F,X))) c= ( lastrng F) by Th58;

        ( lastrng F) c= Y by Def8;

        then

         A3: ( rng ( compose (F,X))) c= Y by A2;

        ( dom ( compose (F,X))) = X by A1, Th61;

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

      end;

    end

    definition

      let q be non-empty non empty FinSequence;

      :: FUNCT_7:def10

      mode FuncSequence of q -> FinSequence means

      : Def9: (( len it ) + 1) = ( len q) & for i be Nat st i in ( dom it ) holds (it . i) in ( Funcs ((q . i),(q . (i + 1))));

      existence

      proof

        defpred P[ object, object] means ex i be Nat st i = $1 & $2 in ( Funcs ((q . i),(q . (i + 1))));

        consider n be Nat such that

         A1: ( len q) = (n + 1) by NAT_1: 6;

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

        

         A2: for x be object st x in ( Seg n) holds ex y be object st P[x, y]

        proof

          let x be object;

          assume

           A3: x in ( Seg n);

          then

          reconsider i = x as Nat;

          

           A4: i <= n by A3, FINSEQ_1: 1;

          then (i + 1) >= 1 & (i + 1) <= (n + 1) by NAT_1: 11, XREAL_1: 6;

          then

           A5: (i + 1) in ( dom q) by A1, FINSEQ_3: 25;

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

          then

           A6: i <= (n + 1) by A4, XXREAL_0: 2;

          i >= 1 by A3, FINSEQ_1: 1;

          then i in ( dom q) by A1, A6, FINSEQ_3: 25;

          then

          reconsider X = (q . i), Y = (q . (i + 1)) as non empty set by A5;

          set y = the Function of X, Y;

          take y, i;

          thus thesis by FUNCT_2: 8;

        end;

        consider f be Function such that

         A7: ( dom f) = ( Seg n) and

         A8: for x be object st x in ( Seg n) holds P[x, (f . x)] from CLASSES1:sch 1( A2);

        reconsider f as FinSequence by A7, FINSEQ_1:def 2;

        take f;

        thus (( len f) + 1) = ( len q) by A1, A7, FINSEQ_1:def 3;

        let i be Nat;

        assume i in ( dom f);

        then ex j be Nat st j = i & (f . i) in ( Funcs ((q . j),(q . (j + 1)))) by A7, A8;

        hence thesis;

      end;

    end

    registration

      let q be non-empty non empty FinSequence;

      cluster -> FuncSeq-like non-empty for FuncSequence of q;

      coherence

      proof

        let p be FuncSequence of q;

        thus p is FuncSeq-like

        proof

          take q;

          thus thesis by Def9;

        end;

        let x be object;

        assume

         A1: x in ( dom p);

        then

        reconsider i = x as Nat;

        ( len q) = (( len p) + 1) by Def9;

        then i in ( dom q) & (i + 1) in ( dom q) by A1, Th22;

        then

        reconsider X = (q . i), Y = (q . (i + 1)) as non empty set;

        (p . i) in ( Funcs (X,Y)) by A1, Def9;

        then ex f st (p . x) = f & ( dom f) = X & ( rng f) c= Y by FUNCT_2:def 2;

        hence thesis;

      end;

    end

    theorem :: FUNCT_7:66

    

     Th65: for q be non-empty non empty FinSequence, p be FuncSequence of q st p <> {} holds ( firstdom p) = (q . 1) & ( lastrng p) c= (q . ( len q))

    proof

      let q be non-empty non empty FinSequence;

      let p be FuncSequence of q;

      assume

       A1: p <> {} ;

      then 1 in ( dom p) by FINSEQ_5: 6;

      then (p . 1) in ( Funcs ((q . 1),(q . (1 + 1)))) by Def9;

      then ex f be Function st (p . 1) = f & ( dom f) = (q . 1) & ( rng f) c= (q . 2) by FUNCT_2:def 2;

      hence ( firstdom p) = (q . 1) by A1, Def5;

      ( len p) in ( dom p) by A1, FINSEQ_5: 6;

      then (p . ( len p)) in ( Funcs ((q . ( len p)),(q . (( len p) + 1)))) by Def9;

      then

       A2: ex g be Function st (p . ( len p)) = g & ( dom g) = (q . ( len p)) & ( rng g) c= (q . (( len p) + 1)) by FUNCT_2:def 2;

      (( len p) + 1) = ( len q) by Def9;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: FUNCT_7:67

    for q be non-empty non empty FinSequence, p be FuncSequence of q holds ( dom ( compose (p,(q . 1)))) = (q . 1) & ( rng ( compose (p,(q . 1)))) c= (q . ( len q))

    proof

      let q be non-empty non empty FinSequence;

      let p be FuncSequence of q;

      per cases ;

        suppose

         A1: p = {} ;

        

         A2: ( len q) = (( len p) + 1) by Def9;

        ( compose (p,(q . 1))) = ( id (q . 1)) & ( len p) = 0 by A1, Th38;

        hence thesis by A2;

      end;

        suppose

         A3: p <> {} ;

        then

         A4: ( lastrng p) c= (q . ( len q)) by Th65;

        ( firstdom p) = (q . 1) & ( rng ( compose (p,(q . 1)))) c= ( lastrng p) by A3, Th58, Th65;

        hence thesis by A4, Th61;

      end;

    end;

    registration

      let X be set;

      let f be sequence of ( bool [:X, X:]);

      let n be Nat;

      cluster (f . n) -> Relation-like;

      coherence

      proof

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

        (f . n) is Element of ( bool [:X, X:]);

        hence thesis;

      end;

    end

    

     Lm1: for f be Function of X, X holds ( rng f) c= ( dom f)

    proof

      let f be Function of X, X;

      ( dom f) = X by FUNCT_2: 52;

      hence thesis;

    end;

    

     Lm2: for f be Relation holds for n be Nat holds for p1,p2 be sequence of ( bool [:( field f), ( field f):]) st (p1 . 0 ) = ( id ( field f)) & (for k be Nat holds (p1 . (k + 1)) = (f * (p1 . k))) & (p2 . 0 ) = ( id ( field f)) & (for k be Nat holds (p2 . (k + 1)) = (f * (p2 . k))) holds p1 = p2

    proof

      let f be Relation;

      let n be Nat;

      let p1,p2 be sequence of ( bool [:( field f), ( field f):]) such that

       A1: (p1 . 0 ) = ( id ( field f)) and

       A2: for k be Nat holds (p1 . (k + 1)) = (f * (p1 . k)) and

       A3: (p2 . 0 ) = ( id ( field f)) and

       A4: for k be Nat holds (p2 . (k + 1)) = (f * (p2 . k));

      defpred P[ Nat, Relation, set] means $3 = (f * $2);

      

       A5: for k be Nat holds P[k, (p1 . k), (p1 . (k + 1))] by A2;

      set FX = ( bool [:( field f), ( field f):]);

      reconsider ID = ( id ( field f)) as Element of FX;

      

       A6: (p2 . 0 ) = ID by A3;

      

       A7: for k be Nat holds for x,y1,y2 be Element of FX st P[k, x, y1] & P[k, x, y2] holds y1 = y2;

      

       A8: for k be Nat holds P[k, (p2 . k), (p2 . (k + 1))] by A4;

      

       A9: (p1 . 0 ) = ID by A1;

      p1 = p2 from NAT_1:sch 14( A9, A5, A6, A8, A7);

      hence thesis;

    end;

    definition

      let f be Relation;

      let n be Nat;

      :: FUNCT_7:def11

      func iter (f,n) -> Relation means

      : Def10: ex p be sequence of ( bool [:( field f), ( field f):]) st it = (p . n) & (p . 0 ) = ( id ( field f)) & for k be Nat holds (p . (k + 1)) = (f * (p . k));

      existence

      proof

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        defpred P[ Nat, Relation, set] means $3 = (f * $2);

        set FX = ( bool [:( field f), ( field f):]);

        reconsider ID = ( id ( field f)) as Element of FX;

        

         A1: for n be Nat holds for x be Element of FX holds ex y be Element of FX st P[n, x, y]

        proof

          ( dom f) c= ( field f) & ( rng f) c= ( field f) by XBOOLE_1: 7;

          then

          reconsider h = f as Relation of ( field f), ( field f) by RELSET_1: 4;

          let n be Nat;

          let x be Element of FX;

          reconsider g = x as Relation of ( field f), ( field f);

          (h * g) is Element of FX;

          hence thesis;

        end;

        consider p be sequence of FX such that

         A2: (p . 0 ) = ID & for n be Nat holds P[n, (p . n), (p . (n + 1))] from RECDEF_1:sch 2( A1);

        (p . n9) is Relation of ( field f), ( field f);

        hence thesis by A2;

      end;

      uniqueness by Lm2;

    end

    registration

      let f be Function;

      let n be Nat;

      cluster ( iter (f,n)) -> Function-like;

      coherence

      proof

        consider p be sequence of ( bool [:( field f), ( field f):]) such that

         A1: (p . n) = ( iter (f,n)) & (p . 0 ) = ( id ( field f)) and

         A2: for k be Nat holds (p . (k + 1)) = (f * (p . k)) by Def10;

        defpred P[ Nat] means (p . $1) is Function;

        

         A3: P[ 0 ] by A1;

        

         A4: for m be Nat holds P[m] implies P[(m + 1)]

        proof

          let m be Nat;

          assume P[m];

          then

          reconsider g = (p . m) as Function;

          (p . (m + 1)) = (g * f) by A2;

          hence thesis;

        end;

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

        hence thesis by A1;

      end;

    end

    reserve m,n,k for Nat,

R for Relation;

    

     Lm3: (( id ( field R)) * R) = R & (R * ( id ( field R))) = R by RELAT_1: 51, RELAT_1: 53, XBOOLE_1: 7;

    theorem :: FUNCT_7:68

    

     Th67: ( iter (R, 0 )) = ( id ( field R))

    proof

      ex p be sequence of ( bool [:( field R), ( field R):]) st ( iter (R, 0 )) = (p . 0 ) & (p . 0 ) = ( id ( field R)) & for k be Nat holds (p . (k + 1)) = (R * (p . k)) by Def10;

      hence thesis;

    end;

    

     Lm4: ( rng R) c= ( dom R) implies ( iter (R, 0 )) = ( id ( dom R))

    proof

      assume ( rng R) c= ( dom R);

      then ( field R) = ( dom R) by XBOOLE_1: 12;

      hence thesis by Th67;

    end;

    theorem :: FUNCT_7:69

    

     Th68: for n be Nat holds ( iter (R,(n + 1))) = (R * ( iter (R,n)))

    proof

      let n be Nat;

      consider p be sequence of ( bool [:( field R), ( field R):]) such that

       A1: (p . (n + 1)) = ( iter (R,(n + 1))) & (p . 0 ) = ( id ( field R)) and

       A2: for k be Nat holds (p . (k + 1)) = (R * (p . k)) by Def10;

      (p . (n + 1)) = (R * (p . n)) by A2;

      hence thesis by A1, A2, Def10;

    end;

    theorem :: FUNCT_7:70

    

     Th69: ( iter (R,1)) = R

    proof

      

      thus ( iter (R,1)) = ( iter (R,( 0 + 1)))

      .= (R * ( iter (R, 0 ))) by Th68

      .= (R * ( id ( field R))) by Th67

      .= R by Lm3;

    end;

    theorem :: FUNCT_7:71

    

     Th70: for n be Nat holds ( iter (R,(n + 1))) = (( iter (R,n)) * R)

    proof

      let n be Nat;

      defpred P[ Nat] means ( iter (R,($1 + 1))) = (( iter (R,$1)) * R);

      

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

      proof

        let k be Nat;

        assume

         A2: ( iter (R,(k + 1))) = (( iter (R,k)) * R);

        

        thus (( iter (R,(k + 1))) * R) = ((R * ( iter (R,k))) * R) by Th68

        .= (R * (( iter (R,k)) * R)) by RELAT_1: 36

        .= ( iter (R,((k + 1) + 1))) by A2, Th68;

      end;

      ( iter (R,( 0 + 1))) = R by Th69

      .= (( id ( field R)) * R) by Lm3

      .= (( iter (R, 0 )) * R) by Th67;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FUNCT_7:72

    

     Th71: ( dom ( iter (R,n))) c= ( field R) & ( rng ( iter (R,n))) c= ( field R)

    proof

      defpred P[ Nat] means ( dom ( iter (R,$1))) c= ( field R) & ( rng ( iter (R,$1))) c= ( field R);

      

       A1: P[k] implies P[(k + 1)]

      proof

        ( iter (R,(k + 1))) = (( iter (R,k)) * R) by Th70;

        then

         A2: ( dom ( iter (R,(k + 1)))) c= ( dom ( iter (R,k))) by RELAT_1: 25;

        ( iter (R,(k + 1))) = (R * ( iter (R,k))) by Th68;

        then

         A3: ( rng ( iter (R,(k + 1)))) c= ( rng ( iter (R,k))) by RELAT_1: 26;

        assume ( dom ( iter (R,k))) c= ( field R) & ( rng ( iter (R,k))) c= ( field R);

        hence thesis by A2, A3, XBOOLE_1: 1;

      end;

      ( iter (R, 0 )) = ( id ( field R)) by Th67;

      then

       A4: P[ 0 ];

       P[k] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    theorem :: FUNCT_7:73

    n <> 0 implies ( dom ( iter (R,n))) c= ( dom R) & ( rng ( iter (R,n))) c= ( rng R)

    proof

      defpred P[ Nat] means ( dom ( iter (R,($1 + 1)))) c= ( dom R) & ( rng ( iter (R,($1 + 1)))) c= ( rng R);

      assume n <> 0 ;

      then

       A1: ex k be Nat st n = (k + 1) by NAT_1: 6;

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume that ( dom ( iter (R,(k + 1)))) c= ( dom R) and ( rng ( iter (R,(k + 1)))) c= ( rng R);

        ( iter (R,((k + 1) + 1))) = (R * ( iter (R,(k + 1)))) & ( iter (R,((k + 1) + 1))) = (( iter (R,(k + 1))) * R) by Th68, Th70;

        hence thesis by RELAT_1: 25, RELAT_1: 26;

      end;

      

       A3: P[ 0 ] by Th69;

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

      hence thesis by A1;

    end;

    theorem :: FUNCT_7:74

    

     Th73: for n be Nat st ( rng R) c= ( dom R) holds ( dom ( iter (R,n))) = ( dom R) & ( rng ( iter (R,n))) c= ( dom R)

    proof

      let n be Nat;

      defpred P[ Nat] means ( dom ( iter (R,$1))) = ( dom R) & ( rng ( iter (R,$1))) c= ( dom R);

      

       A1: for k be Nat holds P[k] implies P[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: ( dom ( iter (R,k))) = ( dom R) & ( rng ( iter (R,k))) c= ( dom R);

        ( iter (R,(k + 1))) = (R * ( iter (R,k))) by Th68;

        then

         A3: ( rng ( iter (R,(k + 1)))) c= ( rng ( iter (R,k))) by RELAT_1: 26;

        ( iter (R,(k + 1))) = (( iter (R,k)) * R) by Th70;

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

      end;

      assume ( rng R) c= ( dom R);

      then ( iter (R, 0 )) = ( id ( dom R)) by Lm4;

      then

       A4: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: FUNCT_7:75

    

     Th74: (( id ( field R)) * ( iter (R,n))) = ( iter (R,n))

    proof

      ( dom ( iter (R,n))) c= ( field R) by Th71;

      hence thesis by RELAT_1: 51;

    end;

    theorem :: FUNCT_7:76

    (( iter (R,n)) * ( id ( field R))) = ( iter (R,n))

    proof

      ( rng ( iter (R,n))) c= ( field R) by Th71;

      hence thesis by RELAT_1: 53;

    end;

    theorem :: FUNCT_7:77

    

     Th76: (( iter (R,m)) * ( iter (R,n))) = ( iter (R,(n + m)))

    proof

      defpred P[ Nat] means (( iter (R,$1)) * ( iter (R,n))) = ( iter (R,(n + $1)));

      

       A1: P[k] implies P[(k + 1)]

      proof

        assume

         A2: (( iter (R,k)) * ( iter (R,n))) = ( iter (R,(n + k)));

        

        thus (( iter (R,(k + 1))) * ( iter (R,n))) = ((R * ( iter (R,k))) * ( iter (R,n))) by Th68

        .= (R * (( iter (R,k)) * ( iter (R,n)))) by RELAT_1: 36

        .= ( iter (R,((n + k) + 1))) by A2, Th68

        .= ( iter (R,(n + (k + 1))));

      end;

      (( iter (R, 0 )) * ( iter (R,n))) = (( id ( field R)) * ( iter (R,n))) by Th67

      .= ( iter (R,(n + 0 ))) by Th74;

      then

       A3: P[ 0 ];

       P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm5: ( iter (( iter (R,m)),k)) = ( iter (R,(m * k))) implies ( iter (( iter (R,m)),(k + 1))) = ( iter (R,(m * (k + 1))))

    proof

      assume

       A1: ( iter (( iter (R,m)),k)) = ( iter (R,(m * k)));

      

      thus ( iter (( iter (R,m)),(k + 1))) = (( iter (R,m)) * ( iter (( iter (R,m)),k))) by Th68

      .= ( iter (R,((m * k) + (m * 1)))) by A1, Th76

      .= ( iter (R,(m * (k + 1))));

    end;

    theorem :: FUNCT_7:78

    n <> 0 implies ( iter (( iter (R,m)),n)) = ( iter (R,(m * n)))

    proof

      defpred P[ Nat] means ( iter (( iter (R,m)),($1 + 1))) = ( iter (R,(m * ($1 + 1))));

      

       A1: P[k] implies P[(k + 1)] by Lm5;

      

       A2: P[ 0 ] by Th69;

      

       A3: P[k] from NAT_1:sch 2( A2, A1);

      assume n <> 0 ;

      then

      consider k be Nat such that

       A4: n = (k + 1) by NAT_1: 6;

      reconsider k as Nat;

      n = (k + 1) by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_7:79

    

     Th78: ( rng R) c= ( dom R) implies ( iter (( iter (R,m)),n)) = ( iter (R,(m * n)))

    proof

      defpred P[ Nat] means ( iter (( iter (R,m)),$1)) = ( iter (R,(m * $1)));

      assume

       A1: ( rng R) c= ( dom R);

      then ( dom ( iter (R,m))) = ( dom R) by Th73;

      then ( field ( iter (R,m))) = ( dom R) by A1, Th73, XBOOLE_1: 12;

      

      then ( iter (( iter (R,m)), 0 )) = ( id ( dom R)) by Th67

      .= ( id ( field R)) by A1, XBOOLE_1: 12

      .= ( iter (R,(m * 0 ))) by Th67;

      then

       A2: P[ 0 ];

      

       A3: P[k] implies P[(k + 1)] by Lm5;

       P[k] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: FUNCT_7:80

    ( iter ( {} ,n)) = {}

    proof

      defpred P[ Nat] means ( iter ( {} ,$1)) = {} ;

      

       A1: P[k] implies P[(k + 1)]

      proof

        assume ( iter ( {} ,k)) = {} ;

        

        thus ( iter ( {} ,(k + 1))) = (( iter ( {} ,k)) * {} ) by Th68

        .= {} ;

      end;

      ( iter ( {} , 0 )) = ( id ( field {} )) by Th67

      .= {} ;

      then

       A2: P[ 0 ];

       P[k] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: FUNCT_7:81

    ( iter (( id X),n)) = ( id X)

    proof

      defpred P[ Nat] means ( iter (( id X),$1)) = ( id X);

      

       A1: P[k] implies P[(k + 1)]

      proof

        assume

         A2: P[k];

        

        thus ( iter (( id X),(k + 1))) = (( iter (( id X),k)) * ( id X)) by Th68

        .= ( id X) by A2, FUNCT_2: 17;

      end;

      ( id ( field ( id X))) = ( id X);

      then

       A3: P[ 0 ] by Th67;

       P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: FUNCT_7:82

    ( rng R) misses ( dom R) implies ( iter (R,2)) = {}

    proof

      assume

       A1: ( rng R) misses ( dom R);

      

      thus ( iter (R,2)) = ( iter (R,(1 + 1)))

      .= (( iter (R,1)) * R) by Th70

      .= (R * R) by Th69

      .= {} by A1, RELAT_1: 44;

    end;

    theorem :: FUNCT_7:83

    for n be Nat holds for f be Function of X, X holds ( iter (f,n)) is Function of X, X

    proof

      let n be Nat;

      let f be Function of X, X;

      

       A1: X = {} implies X = {} ;

      then

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

      

       A3: ( rng f) c= X;

      then ( dom ( iter (f,n))) = X & ( rng ( iter (f,n))) c= X by A2, Th73;

      then

      reconsider R = ( iter (f,n)) as Relation of X, X by RELSET_1: 4;

      ( dom R) = X by A2, A3, Th73;

      hence thesis by A1, FUNCT_2:def 1;

    end;

    theorem :: FUNCT_7:84

    for f be Function of X, X holds ( iter (f, 0 )) = ( id X)

    proof

      let f be Function of X, X;

      ( iter (f, 0 )) = ( id ( field f)) & ( field f) = ( dom f) by Lm1, Th67, XBOOLE_1: 12;

      hence thesis by FUNCT_2: 52;

    end;

    theorem :: FUNCT_7:85

    for f be Function of X, X holds ( iter (( iter (f,m)),n)) = ( iter (f,(m * n)))

    proof

      let f be Function of X, X;

      ( rng f) c= ( dom f) by Lm1;

      hence thesis by Th78;

    end;

    theorem :: FUNCT_7:86

    for f be PartFunc of X, X holds ( iter (f,n)) is PartFunc of X, X

    proof

      let f be PartFunc of X, X;

      

       A1: ( field f) = (( dom f) \/ ( rng f));

      ( rng ( iter (f,n))) c= ( field f) by Th71;

      then

       A2: ( rng ( iter (f,n))) c= X by A1, XBOOLE_1: 1;

      ( dom ( iter (f,n))) c= ( field f) by Th71;

      then ( dom ( iter (f,n))) c= X by A1, XBOOLE_1: 1;

      hence thesis by A2, RELSET_1: 4;

    end;

    theorem :: FUNCT_7:87

    n <> 0 & a in X & f = (X --> a) implies ( iter (f,n)) = f

    proof

      assume that

       A1: n <> 0 and

       A2: a in X and

       A3: f = (X --> a);

      defpred P[ Nat] means ( iter (f,($1 + 1))) = f;

       A4:

      now

        

         A5: ( dom f) = X by A3;

        let k such that

         A6: P[k];

         A7:

        now

          let x be object;

          assume

           A8: x in ( dom f);

          then

           A9: (f . x) = a by A3, FUNCOP_1: 7;

          

          thus (( iter (f,((k + 1) + 1))) . x) = ((f * f) . x) by A6, Th70

          .= (f . (f . x)) by A8, FUNCT_1: 13

          .= (f . x) by A2, A3, A9, FUNCOP_1: 7;

        end;

        ( rng f) = {a} by A2, A3, FUNCOP_1: 8;

        then ( rng f) c= ( dom f) by A2, A5, ZFMISC_1: 31;

        then ( dom ( iter (f,((k + 1) + 1)))) = ( dom f) by Th73;

        hence P[(k + 1)] by A7, FUNCT_1: 2;

      end;

      

       A10: P[ 0 ] by Th69;

      

       A11: P[k] from NAT_1:sch 2( A10, A4);

      consider k be Nat such that

       A12: n = (k + 1) by A1, NAT_1: 6;

      reconsider k as Nat;

      n = (k + 1) by A12;

      hence thesis by A11;

    end;

    theorem :: FUNCT_7:88

    for f be Function, n be Nat holds ( iter (f,n)) = ( compose ((n |-> f),( field f)))

    proof

      let f be Function;

      defpred P[ Nat] means ( iter (f,$1)) = ( compose (($1 |-> f),( field f)));

       A1:

      now

        let n be Nat;

        assume P[n];

        

        then ( iter (f,(n + 1))) = (f * ( compose ((n |-> f),( field f)))) by Th70

        .= ( compose (((n |-> f) ^ <*f*>),( field f))) by Th40

        .= ( compose (((n + 1) |-> f),( field f))) by FINSEQ_2: 60;

        hence P[(n + 1)];

      end;

      ( iter (f, 0 )) = ( id ( field f)) by Th67

      .= ( compose ( {} ,( field f))) by Th38

      .= ( compose (( 0 |-> f),( field f)));

      then

       A2: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A2, A1);

    end;

    begin

    theorem :: FUNCT_7:89

    for f,g be Function, x,y be set st g c= f & not x in ( dom g) holds g c= (f +* (x,y))

    proof

      let f,g be Function, x,y be set such that

       A1: g c= f and

       A2: not x in ( dom g);

       A3:

      now

        let z be object;

        assume

         A4: z in ( dom g);

        

        hence (g . z) = (f . z) by A1, GRFUNC_1: 2

        .= ((f +* (x,y)) . z) by A2, A4, Th31;

      end;

      ( dom g) c= ( dom f) by A1, GRFUNC_1: 2;

      then ( dom g) c= ( dom (f +* (x,y))) by Th29;

      hence thesis by A3, GRFUNC_1: 2;

    end;

    theorem :: FUNCT_7:90

    for f,g be Function, A be set st (f | A) = (g | A) & (f,g) equal_outside A holds f = g

    proof

      let f,g be Function, A be set such that

       A1: (f | A) = (g | A) & (f,g) equal_outside A;

      

      thus f = (f | (( dom f) \/ A)) by RELAT_1: 68, XBOOLE_1: 7

      .= (f | ((( dom f) \ A) \/ A)) by XBOOLE_1: 39

      .= ((f | (( dom f) \ A)) \/ (f | A)) by RELAT_1: 78

      .= ((g | (( dom g) \ A)) \/ (g | A)) by A1

      .= (g | ((( dom g) \ A) \/ A)) by RELAT_1: 78

      .= (g | (( dom g) \/ A)) by XBOOLE_1: 39

      .= g by RELAT_1: 68, XBOOLE_1: 7;

    end;

    theorem :: FUNCT_7:91

    for f be Function, a,b,A be set st a in A holds (f,(f +* (a,b))) equal_outside A

    proof

      let f be Function, a,b,A be set;

      per cases ;

        suppose

         A1: a in ( dom f);

        assume a in A;

        then {a} c= A by ZFMISC_1: 31;

        then

         A2: ( dom (a .--> b)) c= A;

        (f +* (a,b)) = (f +* (a .--> b)) by A1, Def2;

        hence thesis by A2, Th28;

      end;

        suppose not a in ( dom f);

        then (f +* (a,b)) = f by Def2;

        hence thesis;

      end;

    end;

    theorem :: FUNCT_7:92

    

     Th91: for f be Function, a,b be object, A be set holds a in A or ((f +* (a,b)) | A) = (f | A)

    proof

      let f be Function, a,b be object, A be set;

      per cases ;

        suppose

         A1: a in ( dom f);

        assume not a in A;

        then {a} misses A by ZFMISC_1: 50;

        then

         A2: ( dom (a .--> b)) misses A;

        

        thus ((f +* (a,b)) | A) = ((f +* (a .--> b)) | A) by A1, Def2

        .= (f | A) by A2, FUNCT_4: 72;

      end;

        suppose not a in ( dom f);

        hence thesis by Def2;

      end;

    end;

    theorem :: FUNCT_7:93

    for f,g be Function, a,b be object, A be set st (f | A) = (g | A) holds ((f +* (a,b)) | A) = ((g +* (a,b)) | A)

    proof

      let f,g be Function, a,b be object, A be set such that

       A1: (f | A) = (g | A);

      per cases ;

        suppose that

         A2: a in A and

         A3: a in ( dom g);

        now

          assume not a in ( dom f);

          then not a in (( dom f) /\ A) by XBOOLE_0:def 4;

          then not a in ( dom (g | A)) by A1, RELAT_1: 61;

          then not a in (( dom g) /\ A) by RELAT_1: 61;

          hence contradiction by A2, A3, XBOOLE_0:def 4;

        end;

        

        hence ((f +* (a,b)) | A) = ((f +* (a .--> b)) | A) by Def2

        .= ((g | A) +* ((a .--> b) | A)) by A1, FUNCT_4: 71

        .= ((g +* (a .--> b)) | A) by FUNCT_4: 71

        .= ((g +* (a,b)) | A) by A3, Def2;

      end;

        suppose that

         A4: a in A and

         A5: not a in ( dom g);

        now

          assume a in ( dom f);

          then a in (( dom f) /\ A) by A4, XBOOLE_0:def 4;

          then a in ( dom (g | A)) by A1, RELAT_1: 61;

          then a in (( dom g) /\ A) by RELAT_1: 61;

          hence contradiction by A5, XBOOLE_0:def 4;

        end;

        

        hence ((f +* (a,b)) | A) = (g | A) by A1, Def2

        .= ((g +* (a,b)) | A) by A5, Def2;

      end;

        suppose

         A6: not a in A;

        

        hence ((f +* (a,b)) | A) = (f | A) by Th91

        .= ((g +* (a,b)) | A) by A1, A6, Th91;

      end;

    end;

    theorem :: FUNCT_7:94

    

     Th93: for f be Function, a,b be object holds ((f +* (a .--> b)) . a) = b

    proof

      let f be Function, a,b be object;

      a in ( dom (a .--> b)) by TARSKI:def 1;

      

      hence ((f +* (a .--> b)) . a) = ((a .--> b) . a) by FUNCT_4: 13

      .= b by FUNCOP_1: 72;

    end;

    theorem :: FUNCT_7:95

    for a,b be set holds ( <*a*> +* (1,b)) = <*b*>

    proof

      let a,b be set;

      

       A1: ( dom <*b*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      

       A2: ( dom <*a*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      then 1 in ( dom <*a*>) by TARSKI:def 1;

      then

       A3: ( <*a*> +* (1,b)) = ( <*a*> +* (1 .--> b)) by Def2;

      

       A4: for x be object st x in {1} holds (( <*a*> +* (1,b)) . x) = ( <*b*> . x)

      proof

        let x be object;

        assume x in {1};

        then

         A5: x = 1 by TARSKI:def 1;

        

        hence (( <*a*> +* (1,b)) . x) = b by A3, Th93

        .= ( <*b*> . x) by A5, FINSEQ_1:def 8;

      end;

      ( dom ( <*a*> +* (1,b))) = (( dom <*a*>) \/ ( dom (1 .--> b))) by A3, FUNCT_4:def 1

      .= ( {1} \/ {1}) by A2

      .= {1};

      hence thesis by A1, A4;

    end;

    theorem :: FUNCT_7:96

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

    proof

      let f be Function;

      let x be set;

      assume x in ( dom f);

      

      hence (f +* (x .--> (f . x))) = (f +* (x,(f . x))) by Def2

      .= f by Th34;

    end;

    reserve i,j for Nat;

    theorem :: FUNCT_7:97

    

     Th96: for w be FinSequence, r be object, i be natural Number holds ( len (w +* (i,r))) = ( len w)

    proof

      let w be FinSequence, r be object, i be natural Number;

      ( dom (w +* (i,r))) = ( dom w) by Th29;

      

      then ( Seg ( len (w +* (i,r)))) = ( dom w) by FINSEQ_1:def 3

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

      hence thesis by FINSEQ_1: 6;

    end;

    theorem :: FUNCT_7:98

    for D be non empty set, w be FinSequence of D, r be Element of D st i in ( dom w) holds (w +* (i,r)) = (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i))

    proof

      let D be non empty set, w be FinSequence of D, r be Element of D;

      assume

       A1: i in ( dom w);

      then

       A2: 1 <= i by FINSEQ_3: 25;

      

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

      

       A4: ( len (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i))) = (( len ((w | (i -' 1)) ^ <*r*>)) + ( len (w /^ i))) by FINSEQ_1: 22

      .= ((( len (w | (i -' 1))) + ( len <*r*>)) + ( len (w /^ i))) by FINSEQ_1: 22

      .= ((( len (w | (i -' 1))) + 1) + ( len (w /^ i))) by FINSEQ_1: 39

      .= (((i -' 1) + 1) + ( len (w /^ i))) by A3, FINSEQ_1: 59, NAT_D: 44

      .= (((i -' 1) + 1) + (( len w) - i)) by A3, RFINSEQ:def 1

      .= (((i - 1) + 1) + (( len w) - i)) by A2, XREAL_1: 233;

      for j be Nat st 1 <= j & j <= ( len (w +* (i,r))) holds ((w +* (i,r)) . j) = ((((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j)

      proof

        

         A5: ( len (w | (i -' 1))) = (i -' 1) by A3, FINSEQ_1: 59, NAT_D: 44

        .= (i - 1) by A2, XREAL_1: 233;

        let j be Nat;

        assume that

         A6: 1 <= j and

         A7: j <= ( len (w +* (i,r)));

        

         A8: ( len ((w | (i -' 1)) ^ <*r*>)) = (( len (w | (i -' 1))) + ( len <*r*>)) by FINSEQ_1: 22

        .= (( len (w | (i -' 1))) + 1) by FINSEQ_1: 39

        .= ((i -' 1) + 1) by A3, FINSEQ_1: 59, NAT_D: 44

        .= ((i - 1) + 1) by A2, XREAL_1: 233

        .= i;

        

         A9: ( len (w +* (i,r))) = ( len w) by Th96;

        now

          per cases by XXREAL_0: 1;

            case

             A10: i < j;

            then (i + 1) <= j by NAT_1: 13;

            then

             A11: ((i + 1) - i) <= (j - i) by XREAL_1: 9;

            then

             A12: 1 <= (j -' i) by NAT_D: 39;

            

             A13: (j - i) <= (( len w) - i) by A7, A9, XREAL_1: 9;

            

             A14: i <= ( len w) by A1, FINSEQ_3: 25;

            ( len (w /^ i)) = (( len w) -' i) by RFINSEQ: 29

            .= (( len w) - i) by A14, XREAL_1: 233;

            then (j -' i) <= ( len (w /^ i)) by A11, A13, NAT_D: 39;

            then

             A15: (j -' i) in ( dom (w /^ i)) by A12, FINSEQ_3: 25;

            j <= ( len (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i))) by A4, A7, Th96;

            

            then ((((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j) = ((w /^ i) . (j - ( len ((w | (i -' 1)) ^ <*r*>)))) by A8, A10, FINSEQ_1: 24

            .= ((w /^ i) . (j -' i)) by A8, A10, XREAL_1: 233

            .= (w . ((j -' i) + i)) by A14, A15, RFINSEQ:def 1

            .= (w . j) by A10, XREAL_1: 235;

            hence thesis by A10, Th31;

          end;

            case

             A16: j = i;

            

             A17: i = (( len (w | (i -' 1))) + 1) by A5;

            ((((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j) = (((w | (i -' 1)) ^ <*r*>) . i) by A6, A8, A16, FINSEQ_1: 64

            .= r by A17, FINSEQ_1: 42;

            hence thesis by A1, A16, Th30;

          end;

            case

             A18: j < i;

            then (j + 1) <= i by NAT_1: 13;

            then

             A19: ((j + 1) - 1) <= (i - 1) by XREAL_1: 9;

            then

             A20: j <= (i -' 1) by A2, XREAL_1: 233;

            ((((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) . j) = (((w | (i -' 1)) ^ <*r*>) . j) by A6, A8, A18, FINSEQ_1: 64

            .= ((w | (i -' 1)) . j) by A6, A5, A19, FINSEQ_1: 64

            .= (w . j) by A20, FINSEQ_3: 112;

            hence thesis by A18, Th31;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A4, Th96, FINSEQ_1: 14;

    end;

    reserve F for Function,

e,x,y,z for object;

    definition

      let F;

      let x,y be object;

      :: FUNCT_7:def12

      func Swap (F,x,y) -> set equals

      : Def11: ((F +* (x,(F . y))) +* (y,(F . x))) if x in ( dom F) & y in ( dom F)

      otherwise F;

      correctness ;

    end

    registration

      let F;

      let x,y be object;

      cluster ( Swap (F,x,y)) -> Relation-like Function-like;

      coherence

      proof

        per cases ;

          suppose x in ( dom F) & y in ( dom F);

          then ( Swap (F,x,y)) = ((F +* (x,(F . y))) +* (y,(F . x))) by Def11;

          hence thesis;

        end;

          suppose not (x in ( dom F) & y in ( dom F));

          hence thesis by Def11;

        end;

      end;

    end

    theorem :: FUNCT_7:99

    

     Th98: for x,y be object holds ( dom ( Swap (F,x,y))) = ( dom F)

    proof

      let x,y be object;

      per cases ;

        suppose x in ( dom F) & y in ( dom F);

        

        hence ( dom ( Swap (F,x,y))) = ( dom ((F +* (x,(F . y))) +* (y,(F . x)))) by Def11

        .= ( dom (F +* (x,(F . y)))) by Th29

        .= ( dom F) by Th29;

      end;

        suppose not (x in ( dom F) & y in ( dom F));

        hence thesis by Def11;

      end;

    end;

    theorem :: FUNCT_7:100

    

     Th99: for x,y be object holds ( rng (F +* (x,y))) c= (( rng F) \/ {y})

    proof

      let x,y be object;

      

       A1: ( rng (x .--> y)) = {y} by FUNCOP_1: 8;

      per cases ;

        suppose x in ( dom F);

        then (F +* (x,y)) = (F +* (x .--> y)) by Def2;

        hence thesis by A1, FUNCT_4: 17;

      end;

        suppose not x in ( dom F);

        then (F +* (x,y)) = F by Def2;

        hence thesis by XBOOLE_1: 7;

      end;

    end;

    theorem :: FUNCT_7:101

    

     Th100: for x,y be object holds ( rng F) c= (( rng (F +* (x,y))) \/ {(F . x)})

    proof

      let x,y be object;

      let z be object;

      assume z in ( rng F);

      then

      consider e be object such that

       A1: e in ( dom F) and

       A2: z = (F . e) by FUNCT_1:def 3;

      

       A3: ( dom F) = ( dom (F +* (x,y))) by Th29;

      per cases ;

        suppose e = x;

        then z in {(F . x)} by A2, TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose e <> x;

        then ((F +* (x,y)) . e) = (F . e) by Th31;

        then z in ( rng (F +* (x,y))) by A1, A2, A3, FUNCT_1: 3;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: FUNCT_7:102

    

     Th101: x in ( dom F) implies y in ( rng (F +* (x,y)))

    proof

      assume x in ( dom F);

      then x in ( dom (F +* (x,y))) & ((F +* (x,y)) . x) = y by Th29, Th30;

      hence thesis by FUNCT_1: 3;

    end;

    theorem :: FUNCT_7:103

    for x,y be object holds ( rng ( Swap (F,x,y))) = ( rng F)

    proof

      let x,y be object;

      per cases ;

        suppose that

         A1: x in ( dom F) and

         A2: y in ( dom F);

        (F . x) in ( rng F) by A1, FUNCT_1: 3;

        then (F . x) in (( rng F) \/ {(F . y)}) by XBOOLE_0:def 3;

        

        then ((( rng F) \/ {(F . y)}) \/ {(F . x)}) = (( rng F) \/ {(F . y)}) by ZFMISC_1: 40

        .= ( rng F) by A2, FUNCT_1: 3, ZFMISC_1: 40;

        then

         A3: (( rng (F +* (x,(F . y)))) \/ {(F . x)}) c= ( rng F) by Th99, XBOOLE_1: 9;

        

         A4: ((F +* (x,(F . y))) . y) = (F . y)

        proof

          per cases ;

            suppose x <> y;

            hence thesis by Th31;

          end;

            suppose x = y;

            hence thesis by A1, Th30;

          end;

        end;

        

         A5: ( rng F) c= (( rng (F +* (x,(F . y)))) \/ {(F . x)}) by Th100;

        

         A6: ( Swap (F,x,y)) = ((F +* (x,(F . y))) +* (y,(F . x))) by A1, A2, Def11;

        then ( rng ( Swap (F,x,y))) c= (( rng (F +* (x,(F . y)))) \/ {(F . x)}) by Th99;

        then

         A7: ( rng ( Swap (F,x,y))) c= ( rng F) by A3;

        

         A8: y in ( dom (F +* (x,(F . y)))) by A2, Th29;

        

         A9: (F . y) in ( rng ( Swap (F,x,y)))

        proof

          per cases ;

            suppose (F . x) = (F . y);

            hence thesis by A6, A8, Th101;

          end;

            suppose

             A10: (F . x) <> (F . y);

            

             A11: ( dom ( Swap (F,x,y))) = ( dom F) by Th98;

            (( Swap (F,x,y)) . x) = ((F +* (x,(F . y))) . x) by A6, A10, Th31

            .= (F . y) by A1, Th30;

            hence thesis by A1, A11, FUNCT_1: 3;

          end;

        end;

        (F . x) in ( rng ( Swap (F,x,y))) by A6, A8, Th101;

        then (F . x) in (( rng ( Swap (F,x,y))) \/ {(F . y)}) by XBOOLE_0:def 3;

        

        then ((( rng ( Swap (F,x,y))) \/ {(F . y)}) \/ {(F . x)}) = (( rng ( Swap (F,x,y))) \/ {(F . y)}) by ZFMISC_1: 40

        .= ( rng ( Swap (F,x,y))) by A9, ZFMISC_1: 40;

        then (( rng (F +* (x,(F . y)))) \/ {(F . x)}) c= ( rng ( Swap (F,x,y))) by A6, A4, Th100, XBOOLE_1: 9;

        then ( rng F) c= ( rng ( Swap (F,x,y))) by A5;

        hence thesis by A7;

      end;

        suppose not (x in ( dom F) & y in ( dom F));

        hence thesis by Def11;

      end;

    end;

    scheme :: FUNCT_7:sch6

     { A() -> set , D() -> non empty set , G( object) -> object } :

(A(),{ G(d) where d be Element of D() : d in A() }) are_equipotent

      provided

       A1: A() c= D()

       and

       A2: for d1,d2 be Element of D() st d1 in A() & d2 in A() & G(d1) = G(d2) holds d1 = d2;

      per cases ;

        suppose A() <> {} ;

        then

        reconsider D = A() as non empty set;

        set X = { G(d) where d be Element of D : d in A() };

        set Y = { G(d) where d be Element of D() : d in A() };

         A3:

        now

          let x be object;

          hereby

            assume x in X;

            then ex d be Element of D st G(d) = x & d in A();

            hence x in Y by A1;

          end;

          hereby

            assume x in Y;

            then ex d be Element of D() st G(d) = x & d in A();

            hence x in X;

          end;

        end;

         A4:

        now

          let d1,d2 be Element of D;

          reconsider d = d1, dd = d2 as Element of D() by A1;

          assume G(d1) = G(d2);

          then d = dd by A2;

          hence d1 = d2;

        end;

        

         A5: A() c= D;

        (A(),X) are_equipotent from CardMono9( A5, A4);

        hence thesis by A3, TARSKI: 2;

      end;

        suppose

         A6: A() = {} ;

        now

          set a = the Element of { G(d) where d be Element of D() : d in A() };

          assume { G(d) where d be Element of D() : d in A() } <> {} ;

          then a in { G(d) where d be Element of D() : d in A() };

          then ex d be Element of D() st a = G(d) & d in A();

          hence contradiction by A6;

        end;

        hence thesis by A6;

      end;

    end;

    theorem :: FUNCT_7:104

    for f,g,h be Function, A be set holds (f,g) equal_outside A implies ((f +* h),(g +* h)) equal_outside A

    proof

      let f,g,h be Function;

      let A be set;

      

       A1: ( dom ((f +* h) | (( dom (f +* h)) \ A))) = (( dom (f +* h)) \ A) by RELAT_1: 156

      .= ((( dom f) \/ ( dom h)) \ A) by FUNCT_4:def 1

      .= ((( dom f) \ A) \/ (( dom h) \ A)) by XBOOLE_1: 42;

      assume (f,g) equal_outside A;

      then

       A2: (f | (( dom f) \ A)) = (g | (( dom g) \ A));

      

      then

       A3: (( dom f) \ A) = ( dom (g | (( dom g) \ A))) by RELAT_1: 156

      .= (( dom g) \ A) by RELAT_1: 156;

      

      then

       A4: ( dom ((f +* h) | (( dom (f +* h)) \ A))) = ((( dom g) \/ ( dom h)) \ A) by A1, XBOOLE_1: 42

      .= (( dom (g +* h)) \ A) by FUNCT_4:def 1

      .= ( dom ((g +* h) | (( dom (g +* h)) \ A))) by RELAT_1: 156;

      now

        let x be object;

        assume

         A5: x in ( dom ((f +* h) | (( dom (f +* h)) \ A)));

        then

         A6: x in (( dom f) \ A) or x in (( dom h) \ A) by A1, XBOOLE_0:def 3;

        per cases ;

          suppose

           A7: x in (( dom h) \ A);

          

          thus (((f +* h) | (( dom (f +* h)) \ A)) . x) = ((f +* h) . x) by A5, FUNCT_1: 47

          .= (h . x) by A7, FUNCT_4: 13

          .= ((g +* h) . x) by A7, FUNCT_4: 13

          .= (((g +* h) | (( dom (g +* h)) \ A)) . x) by A4, A5, FUNCT_1: 47;

        end;

          suppose

           A8: not x in (( dom h) \ A);

           not x in A by A6, XBOOLE_0:def 5;

          then

           A9: not x in ( dom h) by A8, XBOOLE_0:def 5;

          

           A10: x in (( dom f) \ A) by A1, A5, A8, XBOOLE_0:def 3;

          

          thus (((f +* h) | (( dom (f +* h)) \ A)) . x) = ((f +* h) . x) by A5, FUNCT_1: 47

          .= (f . x) by A9, FUNCT_4: 11

          .= ((g | (( dom g) \ A)) . x) by A2, A6, A8, FUNCT_1: 49

          .= (g . x) by A3, A10, FUNCT_1: 49

          .= ((g +* h) . x) by A9, FUNCT_4: 11

          .= (((g +* h) | (( dom (g +* h)) \ A)) . x) by A4, A5, FUNCT_1: 47;

        end;

      end;

      then ((f +* h) | (( dom (f +* h)) \ A)) = ((g +* h) | (( dom (g +* h)) \ A)) by A4;

      hence thesis;

    end;

    theorem :: FUNCT_7:105

    for f,g,h be Function, A be set holds (f,g) equal_outside A implies ((h +* f),(h +* g)) equal_outside A

    proof

      let f,g,h be Function;

      let A be set;

      assume (f,g) equal_outside A;

      then

       A1: (f | (( dom f) \ A)) = (g | (( dom g) \ A));

      

      then

       A2: (( dom f) \ A) = ( dom (g | (( dom g) \ A))) by RELAT_1: 156

      .= (( dom g) \ A) by RELAT_1: 156;

      

       A3: ( dom ((h +* f) | (( dom (h +* f)) \ A))) = (( dom (h +* f)) \ A) by RELAT_1: 156

      .= ((( dom h) \/ ( dom f)) \ A) by FUNCT_4:def 1

      .= ((( dom h) \ A) \/ (( dom f) \ A)) by XBOOLE_1: 42;

      

      then

       A4: ( dom ((h +* f) | (( dom (h +* f)) \ A))) = ((( dom h) \/ ( dom g)) \ A) by A2, XBOOLE_1: 42

      .= (( dom (h +* g)) \ A) by FUNCT_4:def 1

      .= ( dom ((h +* g) | (( dom (h +* g)) \ A))) by RELAT_1: 156;

      now

        let x be object;

        assume

         A5: x in ( dom ((h +* f) | (( dom (h +* f)) \ A)));

        then

         A6: x in (( dom h) \ A) or x in (( dom f) \ A) by A3, XBOOLE_0:def 3;

        per cases ;

          suppose

           A7: x in (( dom f) \ A);

          

          thus (((h +* f) | (( dom (h +* f)) \ A)) . x) = ((h +* f) . x) by A5, FUNCT_1: 47

          .= (f . x) by A7, FUNCT_4: 13

          .= ((g | (( dom g) \ A)) . x) by A1, A7, FUNCT_1: 49

          .= (g . x) by A2, A7, FUNCT_1: 49

          .= ((h +* g) . x) by A2, A7, FUNCT_4: 13

          .= (((h +* g) | (( dom (h +* g)) \ A)) . x) by A4, A5, FUNCT_1: 47;

        end;

          suppose

           A8: not x in (( dom f) \ A);

          

           A9: not x in A by A6, XBOOLE_0:def 5;

          then

           A10: not x in ( dom f) by A8, XBOOLE_0:def 5;

          

           A11: not x in ( dom g) by A2, A8, A9, XBOOLE_0:def 5;

          

          thus (((h +* f) | (( dom (h +* f)) \ A)) . x) = ((h +* f) . x) by A5, FUNCT_1: 47

          .= (h . x) by A10, FUNCT_4: 11

          .= ((h +* g) . x) by A11, FUNCT_4: 11

          .= (((h +* g) | (( dom (h +* g)) \ A)) . x) by A4, A5, FUNCT_1: 47;

        end;

      end;

      then ((h +* f) | (( dom (h +* f)) \ A)) = ((h +* g) | (( dom (h +* g)) \ A)) by A4;

      hence thesis;

    end;

    theorem :: FUNCT_7:106

    for f,g,h be Function holds (f +* h) = (g +* h) iff (f,g) equal_outside ( dom h)

    proof

      let f,g,h be Function;

      thus (f +* h) = (g +* h) implies (f,g) equal_outside ( dom h)

      proof

        assume (f +* h) = (g +* h);

        then

         A1: ((f +* h),g) equal_outside ( dom h) by Th25, Th28;

        (f,(f +* h)) equal_outside ( dom h) by Th28;

        hence thesis by A1;

      end;

      assume

       A2: (f,g) equal_outside ( dom h);

      then

       A3: (( dom f) \ ( dom h)) = (( dom g) \ ( dom h)) by Th27;

      

       A4: for x be object st x in ( dom (f +* h)) holds ((f +* h) . x) = ((g +* h) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom (f +* h));

        per cases ;

          suppose

           A6: x in ( dom h);

          

          hence ((f +* h) . x) = (h . x) by FUNCT_4: 13

          .= ((g +* h) . x) by A6, FUNCT_4: 13;

        end;

          suppose

           A7: not x in ( dom h);

          ( dom (f +* h)) = (( dom f) \/ ( dom h)) by FUNCT_4:def 1;

          then x in ( dom f) by A5, A7, XBOOLE_0:def 3;

          then

           A8: x in (( dom f) \ ( dom h)) by A7, XBOOLE_0:def 5;

          

           A9: (f | (( dom f) \ ( dom h))) = (g | (( dom g) \ ( dom h))) by A2;

          

          thus ((f +* h) . x) = (f . x) by A7, FUNCT_4: 11

          .= ((g | (( dom g) \ ( dom h))) . x) by A9, A8, FUNCT_1: 49

          .= (g . x) by A3, A8, FUNCT_1: 49

          .= ((g +* h) . x) by A7, FUNCT_4: 11;

        end;

      end;

      ( dom (f +* h)) = (( dom f) \/ ( dom h)) by FUNCT_4:def 1

      .= ((( dom g) \ ( dom h)) \/ ( dom h)) by A3, XBOOLE_1: 39

      .= (( dom g) \/ ( dom h)) by XBOOLE_1: 39

      .= ( dom (g +* h)) by FUNCT_4:def 1;

      hence thesis by A4;

    end;

    theorem :: FUNCT_7:107

    

     Th106: for x,y,a be object, f be Function st (f . x) = (f . y) holds (f . a) = ((f * (( id ( dom f)) +* (x,y))) . a)

    proof

      let x,y,a be object, f be Function;

      assume

       A1: (f . x) = (f . y);

      set g1 = (( id ( dom f)) +* (x,y));

      

       A2: ( dom ( id ( dom f))) = ( dom f);

      per cases ;

        suppose not x in ( dom f);

        then ( id ( dom f)) = g1 by Def2;

        hence thesis by RELAT_1: 52;

      end;

        suppose

         A3: x in ( dom f);

        

         A4: ( dom g1) = ( dom f) by A2, Th29;

        

         A5: (g1 . x) = y by A2, A3, Th30;

        thus (f . a) = ((f * (( id ( dom f)) +* (x,y))) . a)

        proof

          per cases ;

            suppose

             A6: a in ( dom f);

            now

              assume a <> x;

              

              then (g1 . a) = (( id ( dom f)) . a) by Th31

              .= a by A6, FUNCT_1: 18;

              hence thesis by A4, A6, FUNCT_1: 13;

            end;

            hence thesis by A1, A3, A5, A4, FUNCT_1: 13;

          end;

            suppose

             A7: not a in ( dom f);

            ( dom (f * g1)) c= ( dom g1) by RELAT_1: 25;

            then not a in ( dom (f * g1)) by A4, A7;

            then ((f * g1) . a) = {} by FUNCT_1:def 2;

            hence thesis by A7, FUNCT_1:def 2;

          end;

        end;

      end;

    end;

    theorem :: FUNCT_7:108

    for x,y be set, f be Function st x in ( dom f) implies y in ( dom f) & (f . x) = (f . y) holds f = (f * (( id ( dom f)) +* (x,y)))

    proof

      let x,y be set, f be Function;

      assume

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

      set g1 = (( id ( dom f)) +* (x,y));

      set g = (f * g1);

      

       A2: ( dom ( id ( dom f))) = ( dom f);

      per cases ;

        suppose not x in ( dom f);

        then ( id ( dom f)) = g1 by Def2;

        hence thesis by RELAT_1: 52;

      end;

        suppose

         A3: x in ( dom f);

        

         A4: ( dom g1) = ( dom f) by A2, Th29;

        now

          ( rng g1) c= ( dom f)

          proof

            let b be object;

            assume b in ( rng g1);

            then

            consider a be object such that

             A5: a in ( dom g1) and

             A6: b = (g1 . a) by FUNCT_1:def 3;

            per cases ;

              suppose a = x;

              hence thesis by A1, A2, A3, A6, Th30;

            end;

              suppose a <> x;

              then (( id ( dom f)) . a) = (g1 . a) by Th31;

              hence thesis by A4, A5, A6, FUNCT_1: 18;

            end;

          end;

          hence ( dom f) = ( dom g) by A4, RELAT_1: 27;

          let a be object;

          assume a in ( dom f);

          thus (f . a) = (g . a) by A1, A3, Th106;

        end;

        hence thesis;

      end;

    end;

    ::$Canceled

    theorem :: FUNCT_7:110

    

     Th109: for X be set, p be Permutation of X, x,y be Element of X holds ((p +* (x,(p . y))) +* (y,(p . x))) is Permutation of X

    proof

      let X be set, p be Permutation of X, x,y be Element of X;

      set p1 = (p +* (x,(p . y)));

      set p2 = (p1 +* (y,(p . x)));

      

       A1: ( dom p2) = ( dom p1) by Th29;

      

       A2: ( dom p1) = ( dom p) by Th29;

      

       A3: X = {} implies X = {} ;

      then

       A4: ( dom p) = X by FUNCT_2:def 1;

      per cases ;

        suppose X is empty;

        then p2 = {} ;

        hence thesis by A3;

      end;

        suppose

         A5: X is non empty;

        

         A6: ( rng p) = X by FUNCT_2:def 3;

        then

         A7: (p . x) in X by A4, A5, FUNCT_1:def 3;

        thus ((p +* (x,(p . y))) +* (y,(p . x))) is Permutation of X

        proof

          per cases ;

            suppose

             A8: x = y;

            

            then p2 = p1 by Th34

            .= p by A8, Th34;

            hence thesis;

          end;

            suppose

             A9: x <> y;

            

            then

             A10: (p2 . x) = (p1 . x) by Th31

            .= (p . y) by A4, A5, Th30;

             A11:

            now

              let z be set such that z in X and

               A12: z <> x and

               A13: z <> y;

              

              thus (p2 . z) = (p1 . z) by A13, Th31

              .= (p . z) by A12, Th31;

            end;

            

             A14: (p2 . y) = (p . x) by A2, A4, A5, Th30;

             A15:

            now

              let pz be object;

              hereby

                assume pz in ( rng p2);

                then

                consider z be object such that

                 A16: z in ( dom p2) and

                 A17: pz = (p2 . z) by FUNCT_1:def 3;

                

                 A18: (p . z) in X by A1, A2, A6, A16, FUNCT_1:def 3;

                per cases ;

                  suppose z = x;

                  hence pz in X by A4, A5, A6, A10, A17, FUNCT_1:def 3;

                end;

                  suppose z = y;

                  hence pz in X by A2, A4, A7, A17, Th30;

                end;

                  suppose z <> x & z <> y;

                  hence pz in X by A1, A2, A11, A16, A17, A18;

                end;

              end;

              assume pz in X;

              then

              consider z be object such that

               A19: z in ( dom p) and

               A20: pz = (p . z) by A6, FUNCT_1:def 3;

              per cases ;

                suppose z = x;

                hence pz in ( rng p2) by A1, A2, A4, A14, A19, A20, FUNCT_1:def 3;

              end;

                suppose z = y;

                hence pz in ( rng p2) by A1, A2, A4, A10, A19, A20, FUNCT_1:def 3;

              end;

                suppose z <> x & z <> y;

                then (p2 . z) = (p . z) by A11, A19;

                hence pz in ( rng p2) by A1, A2, A19, A20, FUNCT_1:def 3;

              end;

            end;

            then ( rng p2) = X by TARSKI: 2;

            then

            reconsider p2 as Function of X, X by A1, A2, A4, A5, FUNCT_2:def 1, RELSET_1: 4;

            now

              let z1,z2 be object such that

               A21: z1 in X and

               A22: z2 in X and

               A23: (p2 . z1) = (p2 . z2) and

               A24: z1 <> z2;

              per cases ;

                suppose z1 = x & z2 = y;

                hence contradiction by A5, A9, A10, A14, A23, FUNCT_2: 19;

              end;

                suppose z1 = y & z2 = x;

                hence contradiction by A5, A9, A10, A14, A23, FUNCT_2: 19;

              end;

                suppose

                 A25: z1 = x & z2 <> y;

                then (p2 . z2) = (p . z2) by A11, A22, A24;

                hence contradiction by A10, A22, A23, A25, FUNCT_2: 19;

              end;

                suppose

                 A26: z1 <> x & z2 = y;

                then (p2 . z1) = (p . z1) by A11, A21, A24;

                hence contradiction by A14, A21, A23, A26, FUNCT_2: 19;

              end;

                suppose

                 A27: z1 = y & z2 <> x;

                then (p2 . z2) = (p . z2) by A11, A22, A24;

                hence contradiction by A14, A22, A23, A27, FUNCT_2: 19;

              end;

                suppose

                 A28: z1 <> y & z2 = x;

                then (p2 . z1) = (p . z1) by A11, A21, A24;

                hence contradiction by A10, A21, A23, A28, FUNCT_2: 19;

              end;

                suppose z1 <> y & z2 <> x & z1 <> x & z2 <> y;

                then (p2 . z1) = (p . z1) & (p2 . z2) = (p . z2) by A11, A21, A22;

                hence contradiction by A21, A22, A23, A24, FUNCT_2: 19;

              end;

            end;

            then

             A29: p2 is one-to-one by A5, FUNCT_2: 19;

            ( rng p2) = X by A15, TARSKI: 2;

            then p2 is onto by FUNCT_2:def 3;

            hence thesis by A29;

          end;

        end;

      end;

    end;

    theorem :: FUNCT_7:111

    for f be Function, x,y be set st x in ( dom f) & y in ( dom f) holds ex p be Permutation of ( dom f) st ((f +* (x,(f . y))) +* (y,(f . x))) = (f * p)

    proof

      let f be Function, x,y be set such that

       A1: x in ( dom f) and

       A2: y in ( dom f);

      set i = ( id ( dom f));

      (i . x) = x & (i . y) = y by A1, A2, FUNCT_1: 18;

      then

      reconsider p = ((i +* (x,y)) +* (y,x)) as Permutation of ( dom f) by A1, A2, Th109;

      set pk = (i +* (x,y));

      set fr = (f * p);

      set fk = (f +* (x,(f . y)));

      take p;

      set fl = (fk +* (y,(f . x)));

      

       A3: ( dom i) = ( dom f);

      

       A4: ( dom fk) = ( dom fl) by Th29;

      

       A5: ( dom p) = ( dom pk) by Th29;

      

       A6: ( dom pk) = ( dom i) by Th29;

      

       A7: ( dom f) = ( dom fk) by Th29;

      now

        thus ( dom f) = ( dom fl) by A4, Th29;

        ( rng p) = ( dom f) by FUNCT_2:def 3;

        hence ( dom f) = ( dom fr) by A5, A6, RELAT_1: 27;

        let z be object such that

         A8: z in ( dom f);

        per cases ;

          suppose

           A9: x <> y;

          thus (fl . z) = (fr . z)

          proof

            per cases ;

              suppose

               A10: z = x;

              

              hence (fl . z) = (fk . z) by A9, Th31

              .= (f . y) by A8, A10, Th30

              .= (f . (pk . x)) by A1, A3, Th30

              .= (f . (p . x)) by A9, Th31

              .= (fr . z) by A5, A6, A8, A10, FUNCT_1: 13;

            end;

              suppose

               A11: z = y;

              

              hence (fl . z) = (f . x) by A7, A8, Th30

              .= (f . (p . y)) by A2, A6, Th30

              .= (fr . z) by A5, A6, A8, A11, FUNCT_1: 13;

            end;

              suppose

               A12: z <> x & z <> y;

              

              then

               A13: (p . z) = (pk . z) by Th31

              .= (i . z) by A12, Th31

              .= z by A8, FUNCT_1: 18;

              

              thus (fl . z) = (fk . z) by A12, Th31

              .= (f . (p . z)) by A12, A13, Th31

              .= (fr . z) by A5, A6, A8, FUNCT_1: 13;

            end;

          end;

        end;

          suppose

           A14: x = y;

          

           A15: x = (i . x) by A1, FUNCT_1: 17;

          fk = f & i = (i +* (x,(i . y))) by A14, Th34;

          hence (fl . z) = (fr . z) by A14, A15, RELAT_1: 52;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_7:112

    for f be Function, d,r be set st d in ( dom f) holds ( dom f) = ( dom (f +* (d .--> r)))

    proof

      let f be Function, d,r be set;

      assume

       A1: d in ( dom f);

      

      thus ( dom f) = ( dom (f +* (d,r))) by Th29

      .= ( dom (f +* (d .--> r))) by A1, Def2;

    end;

    theorem :: FUNCT_7:113

    for f,g be FinSequence of INT , m,n be Nat st 1 <= n & n <= ( len f) & 1 <= m & m <= ( len f) & g = ((f +* (m,(f /. n))) +* (n,(f /. m))) holds (f . m) = (g . n) & (f . n) = (g . m) & (for k be set st k <> m & k <> n & k in ( dom f) holds (f . k) = (g . k)) & (f,g) are_fiberwise_equipotent

    proof

      let f,g be FinSequence of INT , m,n be Nat;

      assume that

       A1: 1 <= n & n <= ( len f) and

       A2: 1 <= m & m <= ( len f) and

       A3: g = ((f +* (m,(f /. n))) +* (n,(f /. m)));

      

       A4: ( dom (f +* (m,(f /. n)))) = ( dom f) by Th29;

      

       A5: n in ( dom f) by A1, FINSEQ_3: 25;

      

      hence

       A6: (g . n) = (f /. m) by A3, A4, Th30

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

      

       A7: m in ( dom f) by A2, FINSEQ_3: 25;

      now

        per cases ;

          suppose m = n;

          hence (g . m) = (f . n) by A6;

        end;

          suppose m <> n;

          

          hence (g . m) = ((f +* (m,(f /. n))) . m) by A3, Th31

          .= (f /. n) by A7, Th30

          .= (f . n) by A1, FINSEQ_4: 15;

        end;

      end;

       A9:

      now

        let k be set;

        assume that

         A10: k <> m and

         A11: k <> n and k in ( dom f);

        

        thus (g . k) = ((f +* (m,(f /. n))) . k) by A3, A11, Th31

        .= (f . k) by A10, Th31;

      end;

      ( dom g) = ( dom f) by A3, A4, Th29;

      hence thesis by A5, A7, A6, A8, A9, RFINSEQ: 28;

    end;

    theorem :: FUNCT_7:114

    for f be Function, a,A,b,B,c,C be set st a <> b & a <> c holds ((((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a) = A

    proof

      let f be Function, a,A,b,B,c,C be set;

      assume a <> b & a <> c;

      

      hence ((((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a) = ((f +* (a .--> A)) . a) by FUNCT_4: 91

      .= A by Th93;

    end;

    theorem :: FUNCT_7:115

    

     Th114: for A,B,a,b be set, f be Function of A, B st b in B holds (f +* (a,b)) is Function of A, B

    proof

      let A,B,a,b be set, f be Function of A, B such that

       A1: b in B;

      

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

      per cases ;

        suppose not a in A;

        hence thesis by A2, Def2;

      end;

        suppose

         A3: a in A;

        set g = (a .--> b);

        set f1 = (f +* g);

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

        then ( rng g) c= B by A1, ZFMISC_1: 31;

        then

         A4: ( rng f1) c= (( rng f) \/ ( rng g)) & (( rng f) \/ ( rng g)) c= (B \/ B) by FUNCT_4: 17, XBOOLE_1: 13;

        

         A5: {a} c= A by A3, ZFMISC_1: 31;

        ( dom f1) = (A \/ ( dom g)) by A2, FUNCT_4:def 1

        .= (A \/ {a})

        .= A by A5, XBOOLE_1: 12;

        then

         A6: (f +* g) is Function of A, B by A4, FUNCT_2: 2, XBOOLE_1: 1;

        a in ( dom f) by A1, A3, FUNCT_2:def 1;

        hence thesis by A6, Def2;

      end;

    end;

    theorem :: FUNCT_7:116

    

     Th115: ( rng f) c= A implies (f +~ (x,y)) = ((( id A) +* (x,y)) * f)

    proof

      assume

       A1: ( rng f) c= A;

      per cases ;

        suppose x in A;

        then

         A2: x in ( dom ( id A));

        

        thus (f +~ (x,y)) = ((( id A) * f) +* ((x .--> y) * f)) by A1, RELAT_1: 53

        .= ((( id A) +* (x .--> y)) * f) by Th10

        .= ((( id A) +* (x,y)) * f) by A2, Def2;

      end;

        suppose

         A3: not x in A;

        then

         A4: not x in ( dom ( id A));

         not x in ( rng f) by A1, A3;

        

        hence (f +~ (x,y)) = f by FUNCT_4: 103

        .= (( id A) * f) by A1, RELAT_1: 53

        .= ((( id A) +* (x,y)) * f) by A4, Def2;

      end;

    end;

    theorem :: FUNCT_7:117

    ((f +* g) +~ (x,y)) = ((f +~ (x,y)) +* (g +~ (x,y)))

    proof

      set A = (( rng f) \/ ( rng g));

      

       A1: (g +~ (x,y)) = ((( id A) +* (x,y)) * g) by Th115, XBOOLE_1: 7;

      

       A2: ( dom (( id A) +* (x,y))) = ( dom ( id A)) by Th29

      .= A;

      ( rng (f +* g)) c= A by FUNCT_4: 17;

      

      hence ((f +* g) +~ (x,y)) = ((( id A) +* (x,y)) * (f +* g)) by Th115

      .= (((( id A) +* (x,y)) * f) +* ((( id A) +* (x,y)) * g)) by A2, Th9, XBOOLE_1: 7

      .= ((f +~ (x,y)) +* (g +~ (x,y))) by A1, Th115, XBOOLE_1: 7;

    end;

    definition

      let a,b be set;

      :: FUNCT_7:def13

      func a followed_by b -> set equals (( NAT --> b) +* ( 0 ,a));

      coherence ;

    end

    registration

      let a,b be set;

      cluster (a followed_by b) -> Function-like Relation-like;

      coherence ;

    end

    reserve a,b,c for set;

    theorem :: FUNCT_7:118

    

     Th117: ( dom (a followed_by b)) = NAT

    proof

      

      thus ( dom (a followed_by b)) = ( dom (( NAT --> b) +* ( 0 ,a)))

      .= ( dom ( NAT --> b)) by Th29

      .= NAT ;

    end;

    definition

      let X be non empty set;

      let a,b be Element of X;

      :: original: followed_by

      redefine

      func a followed_by b -> sequence of X ;

      coherence

      proof

        (a followed_by b) = (( NAT --> b) +* ( 0 ,a));

        hence thesis by Th114;

      end;

    end

    theorem :: FUNCT_7:119

    

     Th118: ((a followed_by b) . 0 ) = a

    proof

      ( dom ( NAT --> b)) = NAT ;

      hence thesis by Th30;

    end;

    theorem :: FUNCT_7:120

    

     Th119: for n st n > 0 holds ((a followed_by b) . n) = b

    proof

      let n;

      

       A1: n in NAT by ORDINAL1:def 12;

      assume n > 0 ;

      

      hence ((a followed_by b) . n) = (( NAT --> b) . n) by Th31

      .= b by A1, FUNCOP_1: 7;

    end;

    definition

      let a,b,c be set;

      :: FUNCT_7:def14

      func (a,b) followed_by c -> set equals (( NAT --> c) +* (( 0 ,1) --> (a,b)));

      coherence ;

    end

    registration

      let a,b,c be set;

      cluster ((a,b) followed_by c) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: FUNCT_7:121

    

     Th120: ( dom ((a,b) followed_by c)) = NAT

    proof

      

      thus ( dom ((a,b) followed_by c)) = (( dom ( NAT --> c)) \/ ( dom (( 0 ,1) --> (a,b)))) by FUNCT_4:def 1

      .= ( NAT \/ ( dom (( 0 ,1) --> (a,b))))

      .= ( NAT \/ { 0 , 1}) by FUNCT_4: 62

      .= NAT by XBOOLE_1: 12;

    end;

    theorem :: FUNCT_7:122

    

     Th121: (((a,b) followed_by c) . 0 ) = a

    proof

      ( dom (( 0 ,1) --> (a,b))) = { 0 , 1} by FUNCT_4: 62;

      then

       A1: 0 in ( dom (( 0 ,1) --> (a,b))) by TARSKI:def 2;

      

      thus (((a,b) followed_by c) . 0 ) = ((( NAT --> c) +* (( 0 ,1) --> (a,b))) . 0 )

      .= ((( 0 ,1) --> (a,b)) . 0 ) by A1, FUNCT_4: 13

      .= a by FUNCT_4: 63;

    end;

    theorem :: FUNCT_7:123

    

     Th122: (((a,b) followed_by c) . 1) = b

    proof

      ( dom (( 0 ,1) --> (a,b))) = { 0 , 1} by FUNCT_4: 62;

      then

       A1: 1 in ( dom (( 0 ,1) --> (a,b))) by TARSKI:def 2;

      

      thus (((a,b) followed_by c) . 1) = ((( NAT --> c) +* (( 0 ,1) --> (a,b))) . 1)

      .= ((( 0 ,1) --> (a,b)) . 1) by A1, FUNCT_4: 13

      .= b by FUNCT_4: 63;

    end;

    theorem :: FUNCT_7:124

    

     Th123: for n st n > 1 holds (((a,b) followed_by c) . n) = c

    proof

      let n;

      assume

       A1: n > 1;

      ( dom (( 0 ,1) --> (a,b))) = { 0 , 1} by FUNCT_4: 62;

      then

       A2: not n in ( dom (( 0 ,1) --> (a,b))) by A1, TARSKI:def 2;

      

       A3: n in NAT by ORDINAL1:def 12;

      

      thus (((a,b) followed_by c) . n) = ((( NAT --> c) +* (( 0 ,1) --> (a,b))) . n)

      .= (( NAT --> c) . n) by A2, FUNCT_4: 11

      .= c by A3, FUNCOP_1: 7;

    end;

    theorem :: FUNCT_7:125

    

     Th124: ((a,b) followed_by c) = ((a followed_by c) +* (1,b))

    proof

      set f = ((a,b) followed_by c), g = ((a followed_by c) +* (1,b));

      

       A1: ( dom (a followed_by c)) = NAT by Th117;

      

       A2: ( dom f) = NAT by Th120;

      hence ( dom f) = ( dom g) by A1, Th29;

      let x be object;

      assume x in ( dom f);

      then

      reconsider n = x as Nat by A2;

      per cases by NAT_1: 25;

        suppose

         A3: n = 0 ;

        

        hence (f . x) = a by Th121

        .= ((a followed_by c) . x) by A3, Th118

        .= (g . x) by A3, Th31;

      end;

        suppose

         A4: n = 1;

        

        hence (f . x) = b by Th122

        .= (g . x) by A1, A4, Th30;

      end;

        suppose

         A5: n > 1;

        

        hence (f . x) = c by Th123

        .= ((a followed_by c) . x) by A5, Th119

        .= (g . x) by A5, Th31;

      end;

    end;

    definition

      let X be non empty set;

      let a,b,c be Element of X;

      :: original: followed_by

      redefine

      func (a,b) followed_by c -> sequence of X ;

      coherence

      proof

        ((a,b) followed_by c) = ((a followed_by c) +* (1,b)) by Th124;

        hence thesis by Th114;

      end;

    end

    theorem :: FUNCT_7:126

    

     Th125: ( rng (a followed_by b)) = {a, b}

    proof

      ( rng ( NAT --> b)) = {b} by FUNCOP_1: 8;

      then ( rng (( NAT --> b) +* ( 0 ,a))) c= ( {b} \/ {a}) by Th99;

      hence ( rng (a followed_by b)) c= {a, b} by ENUMSET1: 1;

      let x be object;

      assume

       A1: x in {a, b};

      

       A2: ( dom ( NAT --> b)) = NAT ;

      1 in ( dom ( NAT --> b));

      then

       A3: 1 in ( dom (a followed_by b)) by Th29;

      ((a followed_by b) . 1) = b by Th119;

      then

       A4: b in ( rng (a followed_by b)) by A3, FUNCT_1: 3;

      a in ( rng (a followed_by b)) by A2, Th101;

      hence thesis by A1, A4, TARSKI:def 2;

    end;

    theorem :: FUNCT_7:127

    ( rng ((a,b) followed_by c)) = {a, b, c}

    proof

      

       A1: ((a,b) followed_by c) = ((a followed_by c) +* (1,b)) by Th124;

      

      then

       A2: ( dom ((a,b) followed_by c)) = ( dom (a followed_by c)) by Th29

      .= ( dom ( NAT --> c)) by Th29

      .= NAT ;

      (((a,b) followed_by c) . 2) = c by Th123;

      then

       A3: c in ( rng ((a,b) followed_by c)) by A2, FUNCT_1: 3;

      (((a,b) followed_by c) . 1) = b by Th122;

      then

       A4: b in ( rng ((a,b) followed_by c)) by A2, FUNCT_1: 3;

      ( rng (a followed_by c)) = {a, c} by Th125;

      then ( rng ((a followed_by c) +* (1,b))) c= ( {a, c} \/ {b}) by Th99;

      then ( rng ((a followed_by c) +* (1,b))) c= {a, c, b} by ENUMSET1: 3;

      hence ( rng ((a,b) followed_by c)) c= {a, b, c} by A1, ENUMSET1: 57;

      let x be object;

      (((a,b) followed_by c) . 0 ) = a by Th121;

      then

       A5: a in ( rng ((a,b) followed_by c)) by A2, FUNCT_1: 3;

      assume x in {a, b, c};

      hence thesis by A5, A4, A3, ENUMSET1:def 1;

    end;

    definition

      let A,B be set, f be Function of A, B, x be set, y be Element of B;

      :: original: +*

      redefine

      func f +* (x,y) -> Function of A, B ;

      coherence

      proof

        set F = (f +* (x,y));

        

         A1: ( rng F) c= (( rng f) \/ {y}) by Th99;

        per cases ;

          suppose B is empty;

          then ( dom f) is empty;

          hence thesis by Def2;

        end;

          suppose

           A2: B is non empty;

          then {y} c= B by ZFMISC_1: 31;

          then (( rng f) \/ {y}) c= B by XBOOLE_1: 8;

          then

           A3: ( rng F) c= B by A1;

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

          then ( dom F) = A by Th29;

          hence thesis by A2, A3, FUNCT_2:def 1, RELSET_1: 4;

        end;

      end;

    end

    theorem :: FUNCT_7:128

    for A,B be non empty set, f be Function of A, B, x be Element of A, y be set holds ((f +* (x,y)) . x) = y

    proof

      let A,B be non empty set, f be Function of A, B, x be Element of A, y be set;

      x in A;

      then x in ( dom f) by FUNCT_2:def 1;

      hence thesis by Th30;

    end;

    theorem :: FUNCT_7:129

    for A,B be non empty set, f,g be Function of A, B, x be Element of A st for y be Element of A st (f . y) <> (g . y) holds y = x holds f = (g +* (x,(f . x)))

    proof

      let A,B be non empty set, f,g be Function of A, B, x be Element of A such that

       A1: for y be Element of A st (f . y) <> (g . y) holds y = x;

      x in A;

      then

       A2: x in ( dom g) by FUNCT_2:def 1;

      

       A3: ( dom f) = A by FUNCT_2:def 1

      .= (A \/ {x}) by XBOOLE_1: 12

      .= (( dom g) \/ {x}) by FUNCT_2:def 1

      .= (( dom g) \/ ( dom (x .--> (f . x))));

      for e be object st e in (( dom g) \/ ( dom (x .--> (f . x)))) holds (e in ( dom (x .--> (f . x))) implies (f . e) = ((x .--> (f . x)) . e)) & ( not e in ( dom (x .--> (f . x))) implies (f . e) = (g . e))

      proof

        let e be object;

        assume

         A4: e in (( dom g) \/ ( dom (x .--> (f . x))));

        thus e in ( dom (x .--> (f . x))) implies (f . e) = ((x .--> (f . x)) . e)

        proof

          assume e in ( dom (x .--> (f . x)));

          then e in {x};

          then e = x by TARSKI:def 1;

          hence thesis by FUNCOP_1: 72;

        end;

        assume not e in ( dom (x .--> (f . x)));

        then not e in {x};

        then e <> x by TARSKI:def 1;

        hence thesis by A1, A4;

      end;

      

      hence f = (g +* (x .--> (f . x))) by A3, FUNCT_4:def 1

      .= (g +* (x,(f . x))) by A2, Def2;

    end;

    theorem :: FUNCT_7:130

    

     Th129: for g be A -defined Function holds (f,(f +* g)) equal_outside A

    proof

      let g be A -defined Function;

      ( dom g) c= A;

      hence thesis by Th28;

    end;

    theorem :: FUNCT_7:131

    for f,g be A -defined Function holds (f,g) equal_outside A

    proof

      let f,g be A -defined Function;

      

       A1: (( dom g) \ A) = {} by XBOOLE_1: 37;

      (( dom f) \ A) = {} by XBOOLE_1: 37;

      

      hence (f | (( dom f) \ A)) = {}

      .= (g | (( dom g) \ A)) by A1;

    end;

    theorem :: FUNCT_7:132

    for f,g be A -defined Function, h be Function holds ((h +* f),(h +* g)) equal_outside A

    proof

      let f,g be A -defined Function, h be Function;

      (h,(h +* f)) equal_outside A by Th129;

      then

       A1: ((h +* f),h) equal_outside A;

      (h,(h +* g)) equal_outside A by Th129;

      hence thesis by A1;

    end;

    theorem :: FUNCT_7:133

    for I be NAT -defined Function holds ( card ( Shift (I,m))) = ( card I)

    proof

      defpred NC[ set] means not contradiction;

      deffunc U( Nat) = $1;

      let I be NAT -defined Function;

      

       A1: for x be set st x in ( dom I) holds ex d be Element of NAT st x = U(d);

      defpred X[ Nat] means $1 in ( dom I);

      deffunc V( Nat) = ($1 + m);

      set B = { l where l be Element of NAT : U(l) in ( dom I) }, C = { V(l) where l be Nat : l in { n : X[n] } & NC[l] }, D = { V(l) where l be Element of NAT : l in B }, E = { (l + m) where l be Nat : l in ( dom I) };

      

       A2: for d1,d2 be Element of NAT st U(d1) = U(d2) holds d1 = d2;

      

       A3: (( dom I),B) are_equipotent from CardMono( A1, A2);

      

       A4: C c= E

      proof

        let e be object;

        assume e in C;

        then

        consider l be Nat such that

         A5: e = V(l) and

         A6: l in { n : X[n] } & NC[l];

        ex n st n = l & X[n] by A6;

        hence thesis by A5;

      end;

      set B = { l where l be Element of NAT : X[l] };

      B is Subset of NAT from DOMAIN_1:sch 7;

      then

       A7: B c= NAT ;

      set B = { l where l be Element of NAT : l in ( dom I) };

      

       A8: for d1,d2 be Element of NAT st V(d1) = V(d2) holds d1 = d2;

      

       A9: (B,D) are_equipotent from CardMono9( A7, A8);

      

       A10: E c= D

      proof

        let e be object;

        assume e in E;

        then

        consider l be Nat such that

         A11: e = (l + m) and

         A12: l in ( dom I);

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

        l in B by A12;

        hence thesis by A11;

      end;

      

       A13: ( dom ( Shift (I,m))) = E by VALUED_1:def 12;

      

       A14: D c= C

      proof

        let e be object;

        assume e in D;

        then

        consider l1 be Element of NAT such that

         A15: e = V(l1) and

         A16: l1 in B;

        ex l be Element of NAT st l1 = l & U(l) in ( dom I) by A16;

        then l1 in ( dom I);

        then l1 in { n : X[n] };

        hence thesis by A15;

      end;

      then E c= C by A10;

      then

       A17: C = E by A4;

      then C = D by A10, A14;

      then

       A18: (( dom ( Shift (I,m))),( dom I)) are_equipotent by A3, A17, A9, A13, WELLORD2: 15;

      

      thus ( card ( Shift (I,m))) = ( card ( dom ( Shift (I,m)))) by CARD_1: 62

      .= ( card ( dom I)) by A18, CARD_1: 5

      .= ( card I) by CARD_1: 62;

    end;

    theorem :: FUNCT_7:134

    

     Th133: ( dom f) = ( dom g) & ( dom f) c= (A \/ B) & (f | B) = (g | B) implies (f,g) equal_outside A by RELAT_1: 153, XBOOLE_1: 43;

    theorem :: FUNCT_7:135

    

     Th134: ( dom f) = ( dom g) & B c= ( dom f) & A misses B & (f,g) equal_outside A implies (f | B) = (g | B) by RELAT_1: 153, XBOOLE_1: 86;

    reserve A,B,I for set,

X,Y for ManySortedSet of I;

    theorem :: FUNCT_7:136

    I c= (A \/ B) & (X | B) = (Y | B) implies (X,Y) equal_outside A

    proof

      ( dom X) = I & ( dom Y) = I by PARTFUN1:def 2;

      hence thesis by Th133;

    end;

    theorem :: FUNCT_7:137

    B c= I & A misses B & (X,Y) equal_outside A implies (X | B) = (Y | B)

    proof

      ( dom X) = I & ( dom Y) = I by PARTFUN1:def 2;

      hence thesis by Th134;

    end;

    registration

      let V be non empty set;

      let f be V -valued Function, x be object, y be Element of V;

      cluster (f +* (x,y)) -> V -valued;

      coherence

      proof

        

         A1: ( rng (f +* (x,y))) c= (( rng f) \/ {y}) by Th99;

        thus ( rng (f +* (x,y))) c= V by A1, XBOOLE_1: 1;

      end;

    end

    theorem :: FUNCT_7:138

    f c= g & not x in ( dom f) implies f c= (g +* (x,y))

    proof

      assume that

       A1: f c= g;

      assume not x in ( dom f);

      then

       A2: f c= (f +* (x .--> y)) by FUNCT_4: 107;

      per cases ;

        suppose x in ( dom g);

        then (g +* (x,y)) = (g +* (x .--> y)) by Def2;

        then (f +* (x .--> y)) c= (g +* (x,y)) by A1, FUNCT_4: 123;

        hence f c= (g +* (x,y)) by A2;

      end;

        suppose not x in ( dom g);

        hence f c= (g +* (x,y)) by A1, Def2;

      end;

    end;

    theorem :: FUNCT_7:139

    for I be non empty set, X be ManySortedSet of I, l1,l2 be Element of I, i1,i2 be set holds (X +* ((l1,l2) --> (i1,i2))) = ((X +* (l1,i1)) +* (l2,i2))

    proof

      let I be non empty set, X be ManySortedSet of I, l1,l2 be Element of I, i1,i2 be set;

      

       A1: ( dom X) = I by PARTFUN1:def 2;

      then

       A2: l1 in ( dom X);

      ( dom (X +* (l1,i1))) = I by A1, Th29;

      then

       A3: l2 in ( dom (X +* (l1,i1)));

      

      thus (X +* ((l1,l2) --> (i1,i2))) = (X +* ((l1 .--> i1) +* (l2 .--> i2)))

      .= ((X +* (l1 .--> i1)) +* (l2 .--> i2)) by FUNCT_4: 14

      .= ((X +* (l1,i1)) +* (l2 .--> i2)) by A2, Def2

      .= ((X +* (l1,i1)) +* (l2,i2)) by A3, Def2;

    end;

    scheme :: FUNCT_7:sch7

    Unionx { A() -> non empty set , a,b() -> Element of A() , f() -> A() -valued Function , x() -> object , F( object) -> object } :

{ F(i) where i be Element of A() : i in ( rng f()) } = { F(j) where j be Element of A() : j in ( rng (f() +* (x(),a()))) }

      provided

       A1: F(b) = F(a)

       and

       A2: b() = (f() . x());

      set X = { F(i) where i be Element of A() : i in ( rng f()) }, Y = { F(j) where j be Element of A() : j in ( rng (f() +* (x(),a()))) };

      thus X c= Y

      proof

        let e be object;

        assume e in X;

        then

        consider j be Element of A() such that

         A3: e = F(j) and

         A4: j in ( rng f());

        consider y be object such that

         A5: y in ( dom f()) and

         A6: (f() . y) = j by A4, FUNCT_1:def 3;

        y in ( dom (f() +* (x(),a()))) by A5, Th29;

        then

         A7: ((f() +* (x(),a())) . y) in ( rng (f() +* (x(),a()))) by FUNCT_1: 3;

        now

          per cases ;

            suppose y = x();

            hence e = F(.) by A1, A2, A3, A6, Th30, A5;

          end;

            suppose y <> x();

            hence e = F(.) by A3, Th31, A6;

          end;

        end;

        hence e in Y by A7;

      end;

      let e be object;

      assume e in Y;

      then

      consider j be Element of A() such that

       A8: e = F(j) and

       A9: j in ( rng (f() +* (x(),a())));

      consider y be object such that

       A10: y in ( dom (f() +* (x(),a()))) and

       A11: ((f() +* (x(),a())) . y) = j by A9, FUNCT_1:def 3;

      

       A12: y in ( dom f()) by A10, Th29;

      then

       A13: (f() . y) in ( rng f()) by FUNCT_1: 3;

      now

        per cases ;

          suppose y = x();

          hence e = F(.) by A1, A2, A8, A11, Th30, A12;

        end;

          suppose y <> x();

          hence e = F(.) by A8, Th31, A11;

        end;

      end;

      hence e in X by A13;

    end;