funct_3.miz



    begin

    reserve p,q,x,x1,x2,y,y1,y2,z,z1,z2 for set;

    reserve A,B,V,X,X1,X2,Y,Y1,Y2,Z for set;

    reserve C,C1,C2,D,D1,D2 for non empty set;

    theorem :: FUNCT_3:1

    

     Th1: A c= Y implies ( id A) = (( id Y) | A)

    proof

      assume A c= Y;

      

      hence ( id A) = ( id (Y /\ A)) by XBOOLE_1: 28

      .= (( id Y) * ( id A)) by FUNCT_1: 22

      .= (( id Y) | A) by RELAT_1: 65;

    end;

    theorem :: FUNCT_3:2

    

     Th2: for f,g be Function st X c= ( dom (g * f)) holds (f .: X) c= ( dom g)

    proof

      let f,g be Function such that

       A1: X c= ( dom (g * f));

      let y be object;

      assume y in (f .: X);

      then ex x be object st x in ( dom f) & x in X & y = (f . x) by FUNCT_1:def 6;

      hence thesis by A1, FUNCT_1: 11;

    end;

    theorem :: FUNCT_3:3

    

     Th3: for f,g be Function st X c= ( dom f) & (f .: X) c= ( dom g) holds X c= ( dom (g * f))

    proof

      let f,g be Function such that

       A1: X c= ( dom f) and

       A2: (f .: X) c= ( dom g);

      let x be object;

      assume

       A3: x in X;

      then (f . x) in (f .: X) by A1, FUNCT_1:def 6;

      hence thesis by A1, A2, A3, FUNCT_1: 11;

    end;

    theorem :: FUNCT_3:4

    

     Th4: for f,g be Function st Y c= ( rng (g * f)) & g is one-to-one holds (g " Y) c= ( rng f)

    proof

      let f,g be Function such that

       A1: Y c= ( rng (g * f)) and

       A2: g is one-to-one;

      let y be object;

      assume

       A3: y in (g " Y);

      then

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

      (g . y) in Y by A3, FUNCT_1:def 7;

      then

      consider x be object such that

       A5: x in ( dom (g * f)) and

       A6: (g . y) = ((g * f) . x) by A1, FUNCT_1:def 3;

      

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

      (g . y) = (g . (f . x)) & (f . x) in ( dom g) by A5, A6, FUNCT_1: 11, FUNCT_1: 12;

      then y = (f . x) by A2, A4;

      hence thesis by A7, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_3:5

    

     Th5: for f,g be Function st Y c= ( rng g) & (g " Y) c= ( rng f) holds Y c= ( rng (g * f))

    proof

      let f,g be Function such that

       A1: Y c= ( rng g) and

       A2: (g " Y) c= ( rng f);

      let y be object;

      assume

       A3: y in Y;

      then

      consider z be object such that

       A4: z in ( dom g) & y = (g . z) by A1, FUNCT_1:def 3;

      z in (g " Y) by A3, A4, FUNCT_1:def 7;

      then

      consider x be object such that

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

      x in ( dom (g * f)) & ((g * f) . x) = y by A4, A5, FUNCT_1: 11, FUNCT_1: 13;

      hence thesis by FUNCT_1:def 3;

    end;

    scheme :: FUNCT_3:sch1

    FuncEx3 { A() -> set , B() -> set , P[ object, object, object] } :

ex f be Function st ( dom f) = [:A(), B():] & for x,y be object st x in A() & y in B() holds P[x, y, (f . (x,y))]

      provided

       A1: for x,y,z1,z2 be object st x in A() & y in B() & P[x, y, z1] & P[x, y, z2] holds z1 = z2

       and

       A2: for x,y be object st x in A() & y in B() holds ex z be object st P[x, y, z];

      defpred R[ object, object] means for x,y be object st $1 = [x, y] holds P[x, y, $2];

      set D = [:A(), B():];

      

       A3: for p be object st p in D holds ex z be object st R[p, z]

      proof

        let p be object;

        assume p in D;

        then

        consider x1,y1 be object such that

         A4: x1 in A() & y1 in B() and

         A5: p = [x1, y1] by ZFMISC_1:def 2;

        consider z be object such that

         A6: P[x1, y1, z] by A2, A4;

        take z;

        let x,y be object;

        assume

         A7: p = [x, y];

        then x = x1 by A5, XTUPLE_0: 1;

        hence thesis by A5, A6, A7, XTUPLE_0: 1;

      end;

      

       A8: for p,y1,y2 be object st p in D & R[p, y1] & R[p, y2] holds y1 = y2

      proof

        let p,y1,y2 be object;

        assume p in D;

        then

        consider x1,x2 be object such that

         A9: x1 in A() & x2 in B() and

         A10: p = [x1, x2] by ZFMISC_1:def 2;

        assume (for x,y be object st p = [x, y] holds P[x, y, y1]) & for x,y be object st p = [x, y] holds P[x, y, y2];

        then P[x1, x2, y1] & P[x1, x2, y2] by A10;

        hence thesis by A1, A9;

      end;

      consider f be Function such that

       A11: ( dom f) = D and

       A12: for p be object st p in D holds R[p, (f . p)] from FUNCT_1:sch 2( A8, A3);

      take f;

      thus ( dom f) = [:A(), B():] by A11;

      let x,y be object;

      assume x in A() & y in B();

      then [x, y] in [:A(), B():] by ZFMISC_1:def 2;

      hence thesis by A12;

    end;

    scheme :: FUNCT_3:sch2

    Lambda3 { A() -> set , B() -> set , F( object, object) -> object } :

ex f be Function st ( dom f) = [:A(), B():] & for x,y be object st x in A() & y in B() holds (f . (x,y)) = F(x,y);

      defpred P[ object, object, object] means $3 = F($1,$2);

      

       A1: for x,y be object st x in A() & y in B() holds ex z be object st P[x, y, z];

      

       A2: for x,y,z1,z2 be object st x in A() & y in B() & P[x, y, z1] & P[x, y, z2] holds z1 = z2;

      ex f be Function st ( dom f) = [:A(), B():] & for x,y be object st x in A() & y in B() holds P[x, y, (f . (x,y))] from FuncEx3( A2, A1);

      hence thesis;

    end;

    theorem :: FUNCT_3:6

    

     Th6: for f,g be Function st ( dom f) = [:X, Y:] & ( dom g) = [:X, Y:] & for x,y be object st x in X & y in Y holds (f . (x,y)) = (g . (x,y)) holds f = g

    proof

      let f,g be Function such that

       A1: ( dom f) = [:X, Y:] & ( dom g) = [:X, Y:] and

       A2: for x,y be object st x in X & y in Y holds (f . (x,y)) = (g . (x,y));

      for p be object holds p in [:X, Y:] implies (f . p) = (g . p)

      proof

        let p be object;

        assume p in [:X, Y:];

        then

        consider x,y be object such that

         A3: x in X & y in Y and

         A4: p = [x, y] by ZFMISC_1:def 2;

        (f . (x,y)) = (g . (x,y)) by A2, A3;

        hence thesis by A4;

      end;

      hence thesis by A1;

    end;

    definition

      let f be Function;

      :: FUNCT_3:def1

      func .: f -> Function means

      : Def1: ( dom it ) = ( bool ( dom f)) & for X st X c= ( dom f) holds (it . X) = (f .: X);

      existence

      proof

        defpred P[ object, object] means for X st $1 = X holds $2 = (f .: X);

        

         A1: for x be object st x in ( bool ( dom f)) holds ex y be object st P[x, y]

        proof

          let x be object such that x in ( bool ( dom f));

          reconsider x as set by TARSKI: 1;

          take (f .: x);

          thus thesis;

        end;

        

         A2: for x,y1,y2 be object st x in ( bool ( dom f)) & P[x, y1] & P[x, y2] holds y1 = y2

        proof

          let x,y1,y2 be object such that x in ( bool ( dom f)) and

           A3: for X st x = X holds y1 = (f .: X) and

           A4: for X st x = X holds y2 = (f .: X);

          reconsider x as set by TARSKI: 1;

          

          thus y1 = (f .: x) by A3

          .= y2 by A4;

        end;

        consider g be Function such that

         A5: ( dom g) = ( bool ( dom f)) & for x be object st x in ( bool ( dom f)) holds P[x, (g . x)] from FUNCT_1:sch 2( A2, A1);

        take g;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A6: ( dom f1) = ( bool ( dom f)) and

         A7: for X st X c= ( dom f) holds (f1 . X) = (f .: X) and

         A8: ( dom f2) = ( bool ( dom f)) and

         A9: for X st X c= ( dom f) holds (f2 . X) = (f .: X);

        for x be object st x in ( bool ( dom f)) holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume

           A10: x in ( bool ( dom f));

          reconsider x as set by TARSKI: 1;

          (f1 . x) = (f .: x) by A7, A10;

          hence thesis by A9, A10;

        end;

        hence thesis by A6, A8;

      end;

    end

    theorem :: FUNCT_3:7

    

     Th7: for f be Function st X in ( dom ( .: f)) holds (( .: f) . X) = (f .: X)

    proof

      let f be Function;

      assume X in ( dom ( .: f));

      then X in ( bool ( dom f)) by Def1;

      hence thesis by Def1;

    end;

    theorem :: FUNCT_3:8

    for f be Function holds (( .: f) . {} ) = {}

    proof

      let f be Function;

       {} c= ( dom f);

      then (( .: f) . {} ) = (f .: {} ) by Def1;

      hence thesis;

    end;

    theorem :: FUNCT_3:9

    

     Th9: for f be Function holds ( rng ( .: f)) c= ( bool ( rng f))

    proof

      let f be Function;

      let y be object;

      reconsider yy = y as set by TARSKI: 1;

      assume y in ( rng ( .: f));

      then

      consider x be object such that

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

      reconsider x as set by TARSKI: 1;

      y = (f .: x) by A1, Th7;

      then yy c= ( rng f) by RELAT_1: 111;

      hence thesis;

    end;

    theorem :: FUNCT_3:10

    for f be Function holds (( .: f) .: A) c= ( bool ( rng f))

    proof

      let f be Function;

      (( .: f) .: A) c= ( rng ( .: f)) & ( rng ( .: f)) c= ( bool ( rng f)) by Th9, RELAT_1: 111;

      hence thesis;

    end;

    theorem :: FUNCT_3:11

    

     Th11: for f be Function holds (( .: f) " B) c= ( bool ( dom f))

    proof

      let f be Function;

      ( dom ( .: f)) = ( bool ( dom f)) by Def1;

      hence thesis by RELAT_1: 132;

    end;

    theorem :: FUNCT_3:12

    for f be Function of X, D holds (( .: f) " B) c= ( bool X)

    proof

      let f be Function of X, D;

      ( dom f) = X by FUNCT_2:def 1;

      hence thesis by Th11;

    end;

    theorem :: FUNCT_3:13

    

     Th13: for f be Function holds ( union (( .: f) .: A)) c= (f .: ( union A))

    proof

      let f be Function;

      let y be object;

      assume y in ( union (( .: f) .: A));

      then

      consider Z such that

       A1: y in Z and

       A2: Z in (( .: f) .: A) by TARSKI:def 4;

      consider X be object such that

       A3: X in ( dom ( .: f)) and

       A4: X in A and

       A5: Z = (( .: f) . X) by A2, FUNCT_1:def 6;

      reconsider X as set by TARSKI: 1;

      y in (f .: X) by A1, A3, A5, Th7;

      then

      consider x be object such that

       A6: x in ( dom f) and

       A7: x in X and

       A8: y = (f . x) by FUNCT_1:def 6;

      x in ( union A) by A4, A7, TARSKI:def 4;

      hence thesis by A6, A8, FUNCT_1:def 6;

    end;

    theorem :: FUNCT_3:14

    

     Th14: for f be Function st A c= ( bool ( dom f)) holds (f .: ( union A)) = ( union (( .: f) .: A))

    proof

      let f be Function such that

       A1: A c= ( bool ( dom f));

      

       A2: (f .: ( union A)) c= ( union (( .: f) .: A))

      proof

        let y be object;

        assume y in (f .: ( union A));

        then

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

         A3: x in ( union A) and

         A4: y = (f . x) by FUNCT_1:def 6;

        consider X such that

         A5: x in X and

         A6: X in A by A3, TARSKI:def 4;

        X in ( bool ( dom f)) by A1, A6;

        then X in ( dom ( .: f)) by Def1;

        then

         A7: (( .: f) . X) in (( .: f) .: A) by A6, FUNCT_1:def 6;

        y in (f .: X) by A1, A4, A5, A6, FUNCT_1:def 6;

        then y in (( .: f) . X) by A1, A6, Def1;

        hence thesis by A7, TARSKI:def 4;

      end;

      ( union (( .: f) .: A)) c= (f .: ( union A)) by Th13;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: FUNCT_3:15

    for f be Function of X, D st A c= ( bool X) holds (f .: ( union A)) = ( union (( .: f) .: A))

    proof

      let f be Function of X, D;

      ( dom f) = X by FUNCT_2:def 1;

      hence thesis by Th14;

    end;

    theorem :: FUNCT_3:16

    

     Th16: for f be Function holds ( union (( .: f) " B)) c= (f " ( union B))

    proof

      let f be Function;

      let x be object;

      assume x in ( union (( .: f) " B));

      then

      consider X such that

       A1: x in X and

       A2: X in (( .: f) " B) by TARSKI:def 4;

      ( dom ( .: f)) = ( bool ( dom f)) by Def1;

      then

       A3: X in ( bool ( dom f)) by A2, FUNCT_1:def 7;

      then

       A4: (f . x) in (f .: X) by A1, FUNCT_1:def 6;

      (( .: f) . X) in B by A2, FUNCT_1:def 7;

      then (f .: X) in B by A3, Def1;

      then (f . x) in ( union B) by A4, TARSKI:def 4;

      hence thesis by A1, A3, FUNCT_1:def 7;

    end;

    theorem :: FUNCT_3:17

    for f be Function st B c= ( bool ( rng f)) holds (f " ( union B)) = ( union (( .: f) " B))

    proof

      let f be Function such that

       A1: B c= ( bool ( rng f));

      

       A2: (f " ( union B)) c= ( union (( .: f) " B))

      proof

        let x be object;

        assume

         A3: x in (f " ( union B));

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

        then

        consider Y such that

         A4: (f . x) in Y and

         A5: Y in B by TARSKI:def 4;

        

         A6: (f " Y) c= ( dom f) by RELAT_1: 132;

        then (f " Y) in ( bool ( dom f));

        then

         A7: (f " Y) in ( dom ( .: f)) by Def1;

        (f .: (f " Y)) = Y by A1, A5, FUNCT_1: 77;

        then (( .: f) . (f " Y)) in B by A5, A6, Def1;

        then

         A8: (f " Y) in (( .: f) " B) by A7, FUNCT_1:def 7;

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

        then x in (f " Y) by A4, FUNCT_1:def 7;

        hence thesis by A8, TARSKI:def 4;

      end;

      ( union (( .: f) " B)) c= (f " ( union B)) by Th16;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: FUNCT_3:18

    for f,g be Function holds ( .: (g * f)) = (( .: g) * ( .: f))

    proof

      let f,g be Function;

      for x be object holds x in ( dom ( .: (g * f))) iff x in ( dom (( .: g) * ( .: f)))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        thus x in ( dom ( .: (g * f))) implies x in ( dom (( .: g) * ( .: f)))

        proof

          assume x in ( dom ( .: (g * f)));

          then

           A1: x in ( bool ( dom (g * f))) by Def1;

          ( dom (g * f)) c= ( dom f) by RELAT_1: 25;

          then

           A2: xx c= ( dom f) by A1;

          then x in ( bool ( dom f));

          then

           A3: x in ( dom ( .: f)) by Def1;

          (f .: xx) c= ( dom g) by A1, Th2;

          then (f .: xx) in ( bool ( dom g));

          then (f .: xx) in ( dom ( .: g)) by Def1;

          then (( .: f) . x) in ( dom ( .: g)) by A2, Def1;

          hence thesis by A3, FUNCT_1: 11;

        end;

        assume

         A4: x in ( dom (( .: g) * ( .: f)));

        then

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

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

        then (f .: xx) in ( dom ( .: g)) by A5, Th7;

        then

         A6: (f .: xx) in ( bool ( dom g)) by Def1;

        x in ( bool ( dom f)) by A5, Def1;

        then xx c= ( dom (g * f)) by A6, Th3;

        then x in ( bool ( dom (g * f)));

        hence thesis by Def1;

      end;

      then

       A7: ( dom ( .: (g * f))) = ( dom (( .: g) * ( .: f))) by TARSKI: 2;

      for x be object st x in ( dom ( .: (g * f))) holds (( .: (g * f)) . x) = ((( .: g) * ( .: f)) . x)

      proof

        let x be object;

        assume

         A8: x in ( dom ( .: (g * f)));

        then

         A9: x in ( bool ( dom (g * f))) by Def1;

        reconsider xx = x as set by TARSKI: 1;

        

         A10: (f .: xx) c= ( dom g) by Th2, A9;

        ( dom (g * f)) c= ( dom f) by RELAT_1: 25;

        then

         A11: xx c= ( dom f) by A9;

        then x in ( bool ( dom f));

        then

         A12: x in ( dom ( .: f)) by Def1;

        

        thus (( .: (g * f)) . x) = ((g * f) .: xx) by A8, Th7

        .= (g .: (f .: xx)) by RELAT_1: 126

        .= (( .: g) . (f .: xx)) by A10, Def1

        .= (( .: g) . (( .: f) . x)) by A11, Def1

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

      end;

      hence thesis by A7;

    end;

    theorem :: FUNCT_3:19

    

     Th19: for f be Function holds ( .: f) is Function of ( bool ( dom f)), ( bool ( rng f))

    proof

      let f be Function;

      ( dom ( .: f)) = ( bool ( dom f)) & ( rng ( .: f)) c= ( bool ( rng f)) by Def1, Th9;

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

    end;

    theorem :: FUNCT_3:20

    

     Th20: for f be Function of X, Y st Y = {} implies X = {} holds ( .: f) is Function of ( bool X), ( bool Y)

    proof

      let f be Function of X, Y;

      assume Y = {} implies X = {} ;

      then

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

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

      then

       A2: ( bool ( rng f)) c= ( bool Y) by ZFMISC_1: 67;

      

       A3: ( .: f) is Function of ( bool ( dom f)), ( bool ( rng f)) by Th19;

      then ( rng ( .: f)) c= ( bool ( rng f)) by RELAT_1:def 19;

      then

       A4: ( rng ( .: f)) c= ( bool Y) by A2;

      ( dom ( .: f)) = ( bool ( dom f)) by A3, FUNCT_2:def 1;

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

    end;

    definition

      let X, D;

      let f be Function of X, D;

      :: original: .:

      redefine

      func .: f -> Function of ( bool X), ( bool D) ;

      coherence by Th20;

    end

    definition

      let f be Function;

      :: FUNCT_3:def2

      func " f -> Function means

      : Def2: ( dom it ) = ( bool ( rng f)) & for Y st Y c= ( rng f) holds (it . Y) = (f " Y);

      existence

      proof

        defpred P[ object, object] means for Y st $1 = Y holds $2 = (f " Y);

        

         A1: for y be object st y in ( bool ( rng f)) holds ex x be object st P[y, x]

        proof

          let y be object such that y in ( bool ( rng f));

          reconsider y as set by TARSKI: 1;

          take (f " y);

          thus thesis;

        end;

        

         A2: for y,x1,x2 be object st y in ( bool ( rng f)) & P[y, x1] & P[y, x2] holds x1 = x2

        proof

          let y,x1,x2 be object such that y in ( bool ( rng f)) and

           A3: for Y st y = Y holds x1 = (f " Y) and

           A4: for Y st y = Y holds x2 = (f " Y);

          reconsider y as set by TARSKI: 1;

          

          thus x1 = (f " y) by A3

          .= x2 by A4;

        end;

        consider g be Function such that

         A5: ( dom g) = ( bool ( rng f)) & for y be object st y in ( bool ( rng f)) holds P[y, (g . y)] from FUNCT_1:sch 2( A2, A1);

        take g;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A6: ( dom f1) = ( bool ( rng f)) and

         A7: for Y st Y c= ( rng f) holds (f1 . Y) = (f " Y) and

         A8: ( dom f2) = ( bool ( rng f)) and

         A9: for Y st Y c= ( rng f) holds (f2 . Y) = (f " Y);

        for y be object st y in ( bool ( rng f)) holds (f1 . y) = (f2 . y)

        proof

          let y be object;

          assume

           A10: y in ( bool ( rng f));

          reconsider y as set by TARSKI: 1;

          (f1 . y) = (f " y) by A7, A10;

          hence thesis by A9, A10;

        end;

        hence thesis by A6, A8;

      end;

    end

    theorem :: FUNCT_3:21

    

     Th21: for f be Function st Y in ( dom ( " f)) holds (( " f) . Y) = (f " Y)

    proof

      let f be Function;

      ( dom ( " f)) = ( bool ( rng f)) by Def2;

      hence thesis by Def2;

    end;

    theorem :: FUNCT_3:22

    

     Th22: for f be Function holds ( rng ( " f)) c= ( bool ( dom f))

    proof

      let f be Function;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in ( rng ( " f));

      then

      consider y be object such that

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

      reconsider y as set by TARSKI: 1;

      x = (f " y) by A1, Th21;

      then xx c= ( dom f) by RELAT_1: 132;

      hence thesis;

    end;

    theorem :: FUNCT_3:23

    for f be Function holds (( " f) .: B) c= ( bool ( dom f))

    proof

      let f be Function;

      ( rng ( " f)) c= ( bool ( dom f)) & (( " f) .: B) c= ( rng ( " f)) by Th22, RELAT_1: 111;

      hence thesis;

    end;

    theorem :: FUNCT_3:24

    for f be Function holds (( " f) " A) c= ( bool ( rng f))

    proof

      let f be Function;

      ( dom ( " f)) = ( bool ( rng f)) by Def2;

      hence thesis by RELAT_1: 132;

    end;

    theorem :: FUNCT_3:25

    

     Th25: for f be Function holds ( union (( " f) .: B)) c= (f " ( union B))

    proof

      let f be Function;

      let x be object;

      assume x in ( union (( " f) .: B));

      then

      consider X such that

       A1: x in X and

       A2: X in (( " f) .: B) by TARSKI:def 4;

      consider Y be object such that

       A3: Y in ( dom ( " f)) and

       A4: Y in B and

       A5: X = (( " f) . Y) by A2, FUNCT_1:def 6;

      reconsider Y as set by TARSKI: 1;

      

       A6: (( " f) . Y) = (f " Y) by A3, Th21;

      Y in ( bool ( rng f)) by A3, Def2;

      then

       A7: (f .: X) in B by A4, A5, A6, FUNCT_1: 77;

      

       A8: (f " Y) c= ( dom f) by RELAT_1: 132;

      then (f . x) in (f .: X) by A1, A5, A6, FUNCT_1:def 6;

      then (f . x) in ( union B) by A7, TARSKI:def 4;

      hence thesis by A1, A5, A6, A8, FUNCT_1:def 7;

    end;

    theorem :: FUNCT_3:26

    for f be Function st B c= ( bool ( rng f)) holds ( union (( " f) .: B)) = (f " ( union B))

    proof

      let f be Function such that

       A1: B c= ( bool ( rng f));

      

       A2: (f " ( union B)) c= ( union (( " f) .: B))

      proof

        let x be object;

        assume

         A3: x in (f " ( union B));

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

        then

        consider Y such that

         A4: (f . x) in Y and

         A5: Y in B by TARSKI:def 4;

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

        then

         A6: x in (f " Y) by A4, FUNCT_1:def 7;

        Y in ( bool ( rng f)) by A1, A5;

        then

         A7: Y in ( dom ( " f)) by Def2;

        (( " f) . Y) = (f " Y) by A1, A5, Def2;

        then (f " Y) in (( " f) .: B) by A5, A7, FUNCT_1:def 6;

        hence thesis by A6, TARSKI:def 4;

      end;

      ( union (( " f) .: B)) c= (f " ( union B)) by Th25;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: FUNCT_3:27

    

     Th27: for f be Function holds ( union (( " f) " A)) c= (f .: ( union A))

    proof

      let f be Function;

      let y be object;

      assume y in ( union (( " f) " A));

      then

      consider Y such that

       A1: y in Y and

       A2: Y in (( " f) " A) by TARSKI:def 4;

      ( dom ( " f)) = ( bool ( rng f)) by Def2;

      then

       A3: Y in ( bool ( rng f)) by A2, FUNCT_1:def 7;

      then

      consider x be object such that

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

      (( " f) . Y) in A by A2, FUNCT_1:def 7;

      then

       A5: (f " Y) in A by A3, Def2;

      x in (f " Y) by A1, A4, FUNCT_1:def 7;

      then x in ( union A) by A5, TARSKI:def 4;

      hence thesis by A4, FUNCT_1:def 6;

    end;

    theorem :: FUNCT_3:28

    for f be Function st A c= ( bool ( dom f)) & f is one-to-one holds ( union (( " f) " A)) = (f .: ( union A))

    proof

      let f be Function such that

       A1: A c= ( bool ( dom f)) and

       A2: f is one-to-one;

      

       A3: (f .: ( union A)) c= ( union (( " f) " A))

      proof

        let y be object;

        assume y in (f .: ( union A));

        then

        consider x be object such that

         A4: x in ( dom f) and

         A5: x in ( union A) and

         A6: y = (f . x) by FUNCT_1:def 6;

        consider X such that

         A7: x in X and

         A8: X in A by A5, TARSKI:def 4;

        

         A9: (f " (f .: X)) c= X by A2, FUNCT_1: 82;

        

         A10: (f .: X) c= ( rng f) by RELAT_1: 111;

        then (f .: X) in ( bool ( rng f));

        then

         A11: (f .: X) in ( dom ( " f)) by Def2;

        X c= (f " (f .: X)) by A1, A8, FUNCT_1: 76;

        then (f " (f .: X)) = X by A9, XBOOLE_0:def 10;

        then (( " f) . (f .: X)) in A by A8, A10, Def2;

        then

         A12: (f .: X) in (( " f) " A) by A11, FUNCT_1:def 7;

        y in (f .: X) by A4, A6, A7, FUNCT_1:def 6;

        hence thesis by A12, TARSKI:def 4;

      end;

      ( union (( " f) " A)) c= (f .: ( union A)) by Th27;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: FUNCT_3:29

    

     Th29: for f be Function holds (( " f) .: B) c= (( .: f) " B)

    proof

      let f be Function;

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in (( " f) .: B);

      then

      consider Y be object such that

       A1: Y in ( dom ( " f)) and

       A2: Y in B and

       A3: x = (( " f) . Y) by FUNCT_1:def 6;

      reconsider Y as set by TARSKI: 1;

      

       A4: (( " f) . Y) = (f " Y) by A1, Th21;

      then

       A5: xx c= ( dom f) by A3, RELAT_1: 132;

      then x in ( bool ( dom f));

      then

       A6: x in ( dom ( .: f)) by Def1;

      Y in ( bool ( rng f)) by A1, Def2;

      then (f .: xx) in B by A2, A3, A4, FUNCT_1: 77;

      then (( .: f) . x) in B by A5, Def1;

      hence thesis by A6, FUNCT_1:def 7;

    end;

    theorem :: FUNCT_3:30

    for f be Function st f is one-to-one holds (( " f) .: B) = (( .: f) " B)

    proof

      let f be Function such that

       A1: f is one-to-one;

      

       A2: (( .: f) " B) c= (( " f) .: B)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        

         A3: (f .: xx) c= ( rng f) by RELAT_1: 111;

        then (f .: xx) in ( bool ( rng f));

        then

         A4: (f .: xx) in ( dom ( " f)) by Def2;

        assume

         A5: x in (( .: f) " B);

        then

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

        then x in ( bool ( dom f)) by Def1;

        then

         A7: xx c= (f " (f .: xx)) by FUNCT_1: 76;

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

        then x = (f " (f .: xx)) by A7, XBOOLE_0:def 10;

        then

         A8: x = (( " f) . (f .: xx)) by A3, Def2;

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

        then (f .: xx) in B by A6, Th7;

        hence thesis by A8, A4, FUNCT_1:def 6;

      end;

      (( " f) .: B) c= (( .: f) " B) by Th29;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: FUNCT_3:31

    

     Th31: for f be Function, A be set st A c= ( bool ( dom f)) holds (( " f) " A) c= (( .: f) .: A)

    proof

      let f be Function, A be set such that

       A1: A c= ( bool ( dom f));

      let y be object;

      reconsider yy = y as set by TARSKI: 1;

      assume

       A2: y in (( " f) " A);

      then

       A3: (( " f) . y) in A by FUNCT_1:def 7;

      y in ( dom ( " f)) by A2, FUNCT_1:def 7;

      then

       A4: y in ( bool ( rng f)) by Def2;

      then

       A5: (f " yy) in A by A3, Def2;

      then (f " yy) in ( bool ( dom f)) by A1;

      then

       A6: (f " yy) in ( dom ( .: f)) by Def1;

      (f .: (f " yy)) = y by A4, FUNCT_1: 77;

      then

       A7: (( .: f) . (f " yy)) = y by A1, A5, Def1;

      (f " yy) in A by A3, A4, Def2;

      hence thesis by A7, A6, FUNCT_1:def 6;

    end;

    theorem :: FUNCT_3:32

    

     Th32: for f be Function, A be set st f is one-to-one holds (( .: f) .: A) c= (( " f) " A)

    proof

      let f be Function, A be set such that

       A1: f is one-to-one;

      let y be object;

      reconsider yy = y as set by TARSKI: 1;

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

      then

      consider x be object such that

       A2: x in ( dom ( .: f)) and

       A3: x in A and

       A4: y = (( .: f) . x) by FUNCT_1:def 6;

      reconsider x as set by TARSKI: 1;

      

       A5: x in ( bool ( dom f)) by A2, Def1;

      then

       A6: y = (f .: x) by A4, Def1;

      then

       A7: x c= (f " yy) by A5, FUNCT_1: 76;

      

       A8: yy c= ( rng f) by A6, RELAT_1: 111;

      then y in ( bool ( rng f));

      then

       A9: y in ( dom ( " f)) by Def2;

      (f " yy) c= x by A1, A6, FUNCT_1: 82;

      then (f " yy) in A by A3, A7, XBOOLE_0:def 10;

      then (( " f) . y) in A by A8, Def2;

      hence thesis by A9, FUNCT_1:def 7;

    end;

    theorem :: FUNCT_3:33

    for f be Function, A be set st f is one-to-one & A c= ( bool ( dom f)) holds (( " f) " A) = (( .: f) .: A)

    proof

      let f be Function, A be set;

      assume f is one-to-one & A c= ( bool ( dom f));

      then (( " f) " A) c= (( .: f) .: A) & (( .: f) .: A) c= (( " f) " A) by Th31, Th32;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: FUNCT_3:34

    for f,g be Function st g is one-to-one holds ( " (g * f)) = (( " f) * ( " g))

    proof

      let f,g be Function such that

       A1: g is one-to-one;

      for y be object holds y in ( dom ( " (g * f))) iff y in ( dom (( " f) * ( " g)))

      proof

        let y be object;

        reconsider yy = y as set by TARSKI: 1;

        thus y in ( dom ( " (g * f))) implies y in ( dom (( " f) * ( " g)))

        proof

          assume y in ( dom ( " (g * f)));

          then

           A2: y in ( bool ( rng (g * f))) by Def2;

          ( rng (g * f)) c= ( rng g) by RELAT_1: 26;

          then

           A3: yy c= ( rng g) by A2;

          then y in ( bool ( rng g));

          then

           A4: y in ( dom ( " g)) by Def2;

          (g " yy) c= ( rng f) by A1, A2, Th4;

          then (g " yy) in ( bool ( rng f));

          then (g " yy) in ( dom ( " f)) by Def2;

          then (( " g) . y) in ( dom ( " f)) by A3, Def2;

          hence thesis by A4, FUNCT_1: 11;

        end;

        assume

         A5: y in ( dom (( " f) * ( " g)));

        then

         A6: y in ( dom ( " g)) by FUNCT_1: 11;

        (( " g) . y) in ( dom ( " f)) by A5, FUNCT_1: 11;

        then (g " yy) in ( dom ( " f)) by A6, Th21;

        then

         A7: (g " yy) in ( bool ( rng f)) by Def2;

        y in ( bool ( rng g)) by A6, Def2;

        then yy c= ( rng (g * f)) by A7, Th5;

        then y in ( bool ( rng (g * f)));

        hence thesis by Def2;

      end;

      then

       A8: ( dom ( " (g * f))) = ( dom (( " f) * ( " g))) by TARSKI: 2;

      for y be object st y in ( dom ( " (g * f))) holds (( " (g * f)) . y) = ((( " f) * ( " g)) . y)

      proof

        let y be object;

        assume

         A9: y in ( dom ( " (g * f)));

        then

         A10: y in ( bool ( rng (g * f))) by Def2;

        reconsider yy = y as set by TARSKI: 1;

        

         A11: (g " yy) c= ( rng f) by A1, Th4, A10;

        ( rng (g * f)) c= ( rng g) by RELAT_1: 26;

        then

         A12: yy c= ( rng g) by A10;

        then y in ( bool ( rng g));

        then

         A13: y in ( dom ( " g)) by Def2;

        

        thus (( " (g * f)) . y) = ((g * f) " yy) by A9, Th21

        .= (f " (g " yy)) by RELAT_1: 146

        .= (( " f) . (g " yy)) by A11, Def2

        .= (( " f) . (( " g) . y)) by A12, Def2

        .= ((( " f) * ( " g)) . y) by A13, FUNCT_1: 13;

      end;

      hence thesis by A8;

    end;

    theorem :: FUNCT_3:35

    for f be Function holds ( " f) is Function of ( bool ( rng f)), ( bool ( dom f))

    proof

      let f be Function;

      ( dom ( " f)) = ( bool ( rng f)) & ( rng ( " f)) c= ( bool ( dom f)) by Def2, Th22;

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

    end;

    definition

      let A, X;

      :: FUNCT_3:def3

      func chi (A,X) -> Function means

      : Def3: ( dom it ) = X & for x be object st x in X holds (x in A implies (it . x) = 1) & ( not x in A implies (it . x) = 0 );

      existence

      proof

        defpred P[ object, object] means ($1 in A implies $2 = 1) & ( not $1 in A implies $2 = 0 );

        

         A1: for x be object st x in X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in X;

           not x in A implies ex y st y = {} & (x in A implies y = 1) & ( not x in A implies y = {} );

          hence thesis;

        end;

        

         A2: for x,y1,y2 be object st x in X & P[x, y1] & P[x, y2] holds y1 = y2;

        ex f be Function st ( dom f) = X & for x be object st x in X holds P[x, (f . x)] from FUNCT_1:sch 2( A2, A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A3: ( dom f1) = X and

         A4: for x be object st x in X holds (x in A implies (f1 . x) = 1) & ( not x in A implies (f1 . x) = 0 ) and

         A5: ( dom f2) = X and

         A6: for x be object st x in X holds (x in A implies (f2 . x) = 1) & ( not x in A implies (f2 . x) = 0 );

        for x be object st x in X holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume

           A7: x in X;

          then

           A8: not x in A implies (f1 . x) = 0 & (f2 . x) = 0 by A4, A6;

          x in A implies (f1 . x) = 1 & (f2 . x) = 1 by A4, A6, A7;

          hence thesis by A8;

        end;

        hence thesis by A3, A5;

      end;

    end

    theorem :: FUNCT_3:36

    

     Th36: for x be object holds (( chi (A,X)) . x) = 1 implies x in A

    proof

      let x be object;

      assume

       A1: (( chi (A,X)) . x) = 1;

      

       A2: 1 = ( succ 0 )

      .= { 0 };

      per cases ;

        suppose x in X;

        hence thesis by A1, Def3;

      end;

        suppose not x in X;

        then not x in ( dom ( chi (A,X))) by Def3;

        hence thesis by A1, FUNCT_1:def 2, A2;

      end;

    end;

    theorem :: FUNCT_3:37

    x in (X \ A) implies (( chi (A,X)) . x) = 0

    proof

      assume

       A1: x in (X \ A);

      then not x in A by XBOOLE_0:def 5;

      hence thesis by A1, Def3;

    end;

    theorem :: FUNCT_3:38

    A c= X & B c= X & ( chi (A,X)) = ( chi (B,X)) implies A = B

    proof

      assume that

       A1: A c= X and

       A2: B c= X and

       A3: ( chi (A,X)) = ( chi (B,X));

      for x be object holds x in A iff x in B

      proof

        let x be object;

        thus x in A implies x in B

        proof

          assume x in A;

          then (( chi (A,X)) . x) = 1 by A1, Def3;

          hence thesis by A3, Th36;

        end;

        assume x in B;

        then (( chi (B,X)) . x) = 1 by A2, Def3;

        hence thesis by A3, Th36;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FUNCT_3:39

    

     Th39: ( rng ( chi (A,X))) c= { 0 , 1}

    proof

      let y be object;

      assume y in ( rng ( chi (A,X)));

      then

      consider x be object such that

       A1: x in ( dom ( chi (A,X))) and

       A2: y = (( chi (A,X)) . x) by FUNCT_1:def 3;

      

       A3: x in A or not x in A;

      x in X by A1, Def3;

      then y = {} or y = 1 by A2, A3, Def3;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: FUNCT_3:40

    for f be Function of X, { 0 , 1} holds f = ( chi ((f " {1}),X))

    proof

      let f be Function of X, { 0 , 1};

      now

        thus

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

        let x be object such that

         A2: x in X;

        thus x in (f " {1}) implies (f . x) = 1

        proof

          assume x in (f " {1});

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

          hence thesis by TARSKI:def 1;

        end;

        assume not x in (f " {1});

        then not (f . x) in {1} by A1, A2, FUNCT_1:def 7;

        then

         A3: ( rng f) c= { {} , 1} & (f . x) <> 1 by RELAT_1:def 19, TARSKI:def 1;

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

        hence (f . x) = {} by A3, TARSKI:def 2;

      end;

      hence thesis by Def3;

    end;

    definition

      let A, X;

      :: original: chi

      redefine

      func chi (A,X) -> Function of X, { 0 , 1} ;

      coherence

      proof

        ( dom ( chi (A,X))) = X & ( rng ( chi (A,X))) c= { 0 , 1} by Def3, Th39;

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

      end;

    end

    notation

      let Y;

      let A be Subset of Y;

      synonym incl A for id A;

    end

    definition

      let Y;

      let A be Subset of Y;

      :: original: incl

      redefine

      func incl A -> Function of A, Y ;

      coherence

      proof

        

         A1: ( rng ( id A)) = A & ( dom ( id A)) = A;

        thus thesis by A1, FUNCT_2: 2;

      end;

    end

    theorem :: FUNCT_3:41

    for A be Subset of Y holds ( incl A) = (( id Y) | A) by Th1;

    theorem :: FUNCT_3:42

    for A be Subset of Y st x in A holds (( incl A) . x) in Y

    proof

      let A be Subset of Y such that

       A1: x in A;

      ( dom ( incl A)) = A & ( rng ( incl A)) = A;

      then (( incl A) . x) in A by A1, FUNCT_1:def 3;

      hence thesis;

    end;

    definition

      let X, Y;

      :: FUNCT_3:def4

      func pr1 (X,Y) -> Function means

      : Def4: ( dom it ) = [:X, Y:] & for x,y be object st x in X & y in Y holds (it . (x,y)) = x;

      existence

      proof

        deffunc F( object, object) = $1;

        ex f be Function st ( dom f) = [:X, Y:] & for x,y be object st x in X & y in Y holds (f . (x,y)) = F(x,y) from Lambda3;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A1: ( dom f1) = [:X, Y:] and

         A2: for x,y be object st x in X & y in Y holds (f1 . (x,y)) = x and

         A3: ( dom f2) = [:X, Y:] and

         A4: for x,y be object st x in X & y in Y holds (f2 . (x,y)) = x;

        for x,y be object st x in X & y in Y holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume

           A5: x in X & y in Y;

          then (f1 . (x,y)) = x by A2;

          hence thesis by A4, A5;

        end;

        hence thesis by A1, A3, Th6;

      end;

      :: FUNCT_3:def5

      func pr2 (X,Y) -> Function means

      : Def5: ( dom it ) = [:X, Y:] & for x,y be object st x in X & y in Y holds (it . (x,y)) = y;

      existence

      proof

        deffunc F( object, object) = $2;

        ex f be Function st ( dom f) = [:X, Y:] & for x,y be object st x in X & y in Y holds (f . (x,y)) = F(x,y) from Lambda3;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A6: ( dom f1) = [:X, Y:] and

         A7: for x,y be object st x in X & y in Y holds (f1 . (x,y)) = y and

         A8: ( dom f2) = [:X, Y:] and

         A9: for x,y be object st x in X & y in Y holds (f2 . (x,y)) = y;

        for x,y be object st x in X & y in Y holds (f1 . (x,y)) = (f2 . (x,y))

        proof

          let x,y be object;

          assume

           A10: x in X & y in Y;

          then (f1 . (x,y)) = y by A7;

          hence thesis by A9, A10;

        end;

        hence thesis by A6, A8, Th6;

      end;

    end

    theorem :: FUNCT_3:43

    

     Th43: ( rng ( pr1 (X,Y))) c= X

    proof

      let x be object;

      assume x in ( rng ( pr1 (X,Y)));

      then

      consider p be object such that

       A1: p in ( dom ( pr1 (X,Y))) and

       A2: x = (( pr1 (X,Y)) . p) by FUNCT_1:def 3;

      p in [:X, Y:] by A1, Def4;

      then

      consider x1,y1 be object such that

       A3: x1 in X & y1 in Y and

       A4: p = [x1, y1] by ZFMISC_1:def 2;

      x = (( pr1 (X,Y)) . (x1,y1)) by A2, A4;

      hence thesis by A3, Def4;

    end;

    theorem :: FUNCT_3:44

    Y <> {} implies ( rng ( pr1 (X,Y))) = X

    proof

      set y = the Element of Y;

      assume

       A1: Y <> {} ;

      

       A2: X c= ( rng ( pr1 (X,Y)))

      proof

        let x be object;

        assume

         A3: x in X;

        then [x, y] in [:X, Y:] by A1, ZFMISC_1: 87;

        then

         A4: [x, y] in ( dom ( pr1 (X,Y))) by Def4;

        (( pr1 (X,Y)) . (x,y)) = x by A1, A3, Def4;

        hence thesis by A4, FUNCT_1:def 3;

      end;

      ( rng ( pr1 (X,Y))) c= X by Th43;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    theorem :: FUNCT_3:45

    

     Th45: ( rng ( pr2 (X,Y))) c= Y

    proof

      let y be object;

      assume y in ( rng ( pr2 (X,Y)));

      then

      consider p be object such that

       A1: p in ( dom ( pr2 (X,Y))) and

       A2: y = (( pr2 (X,Y)) . p) by FUNCT_1:def 3;

      p in [:X, Y:] by A1, Def5;

      then

      consider x1,y1 be object such that

       A3: x1 in X & y1 in Y and

       A4: p = [x1, y1] by ZFMISC_1:def 2;

      y = (( pr2 (X,Y)) . (x1,y1)) by A2, A4;

      hence thesis by A3, Def5;

    end;

    theorem :: FUNCT_3:46

    X <> {} implies ( rng ( pr2 (X,Y))) = Y

    proof

      set x = the Element of X;

      assume

       A1: X <> {} ;

      

       A2: Y c= ( rng ( pr2 (X,Y)))

      proof

        let y be object;

        assume

         A3: y in Y;

        then [x, y] in [:X, Y:] by A1, ZFMISC_1: 87;

        then

         A4: [x, y] in ( dom ( pr2 (X,Y))) by Def5;

        (( pr2 (X,Y)) . (x,y)) = y by A1, A3, Def5;

        hence thesis by A4, FUNCT_1:def 3;

      end;

      ( rng ( pr2 (X,Y))) c= Y by Th45;

      hence thesis by A2, XBOOLE_0:def 10;

    end;

    definition

      let X, Y;

      :: original: pr1

      redefine

      func pr1 (X,Y) -> Function of [:X, Y:], X ;

      coherence

      proof

        per cases ;

          suppose X = {} implies [:X, Y:] = {} ;

          ( dom ( pr1 (X,Y))) = [:X, Y:] & ( rng ( pr1 (X,Y))) c= X by Def4, Th43;

          hence thesis by FUNCT_2: 2;

        end;

          suppose X = {} & [:X, Y:] <> {} ;

          hence thesis by ZFMISC_1: 90;

        end;

      end;

      :: original: pr2

      redefine

      func pr2 (X,Y) -> Function of [:X, Y:], Y ;

      coherence

      proof

        per cases ;

          suppose Y = {} implies [:X, Y:] = {} ;

          ( dom ( pr2 (X,Y))) = [:X, Y:] & ( rng ( pr2 (X,Y))) c= Y by Def5, Th45;

          hence thesis by FUNCT_2: 2;

        end;

          suppose Y = {} & [:X, Y:] <> {} ;

          hence thesis by ZFMISC_1: 90;

        end;

      end;

    end

    definition

      let X;

      :: FUNCT_3:def6

      func delta (X) -> Function means

      : Def6: ( dom it ) = X & for x be object st x in X holds (it . x) = [x, x];

      existence

      proof

        deffunc F( object) = [$1, $1];

        ex f be Function st ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A1: ( dom f1) = X and

         A2: for x be object st x in X holds (f1 . x) = [x, x] and

         A3: ( dom f2) = X and

         A4: for x be object st x in X holds (f2 . x) = [x, x];

        for x be object st x in X holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume

           A5: x in X;

          then (f1 . x) = [x, x] by A2;

          hence thesis by A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    theorem :: FUNCT_3:47

    

     Th47: ( rng ( delta X)) c= [:X, X:]

    proof

      let y be object;

      assume y in ( rng ( delta X));

      then

      consider x be object such that

       A1: x in ( dom ( delta X)) and

       A2: y = (( delta X) . x) by FUNCT_1:def 3;

      

       A3: x in X by A1, Def6;

      then y = [x, x] by A2, Def6;

      hence thesis by A3, ZFMISC_1: 87;

    end;

    definition

      let X;

      :: original: delta

      redefine

      func delta (X) -> Function of X, [:X, X:] ;

      coherence

      proof

        ( dom ( delta X)) = X & ( rng ( delta X)) c= [:X, X:] by Def6, Th47;

        hence thesis by FUNCT_2: 2;

      end;

    end

    definition

      let f,g be Function;

      :: FUNCT_3:def7

      func <:f,g:> -> Function means

      : Def7: ( dom it ) = (( dom f) /\ ( dom g)) & for x be object st x in ( dom it ) holds (it . x) = [(f . x), (g . x)];

      existence

      proof

        deffunc F( object) = [(f . $1), (g . $1)];

        ex fg be Function st ( dom fg) = (( dom f) /\ ( dom g)) & for x be object st x in (( dom f) /\ ( dom g)) holds (fg . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A1: ( dom f1) = (( dom f) /\ ( dom g)) and

         A2: for x be object st x in ( dom f1) holds (f1 . x) = [(f . x), (g . x)] and

         A3: ( dom f2) = (( dom f) /\ ( dom g)) and

         A4: for x be object st x in ( dom f2) holds (f2 . x) = [(f . x), (g . x)];

        for x be object st x in (( dom f) /\ ( dom g)) holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume

           A5: x in (( dom f) /\ ( dom g));

          then (f1 . x) = [(f . x), (g . x)] by A1, A2;

          hence thesis by A3, A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    registration

      let f be empty Function, g be Function;

      cluster <:f, g:> -> empty;

      coherence

      proof

        ( dom f) = {} ;

        then ( dom <:f, g:>) = ( {} /\ ( dom g)) by Def7;

        hence thesis;

      end;

      cluster <:g, f:> -> empty;

      coherence

      proof

        ( dom f) = {} ;

        then ( dom <:g, f:>) = ( {} /\ ( dom g)) by Def7;

        hence thesis;

      end;

    end

    theorem :: FUNCT_3:48

    

     Th48: for f,g be Function st x in (( dom f) /\ ( dom g)) holds ( <:f, g:> . x) = [(f . x), (g . x)]

    proof

      let f,g be Function;

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

      then x in ( dom <:f, g:>) by Def7;

      hence thesis by Def7;

    end;

    theorem :: FUNCT_3:49

    

     Th49: for f,g be Function st ( dom f) = X & ( dom g) = X & x in X holds ( <:f, g:> . x) = [(f . x), (g . x)]

    proof

      let f,g be Function;

      assume ( dom f) = X & ( dom g) = X & x in X;

      then x in (( dom f) /\ ( dom g));

      then x in ( dom <:f, g:>) by Def7;

      hence thesis by Def7;

    end;

    theorem :: FUNCT_3:50

    

     Th50: for f,g be Function st ( dom f) = X & ( dom g) = X holds ( dom <:f, g:>) = X

    proof

      let f,g be Function;

      ( dom <:f, g:>) = (( dom f) /\ ( dom g)) by Def7;

      hence thesis;

    end;

    theorem :: FUNCT_3:51

    

     Th51: for f,g be Function holds ( rng <:f, g:>) c= [:( rng f), ( rng g):]

    proof

      let f,g be Function;

      let q be object;

      assume q in ( rng <:f, g:>);

      then

      consider x be object such that

       A1: x in ( dom <:f, g:>) and

       A2: q = ( <:f, g:> . x) by FUNCT_1:def 3;

      

       A3: x in (( dom f) /\ ( dom g)) by A1, Def7;

      then x in ( dom f) by XBOOLE_0:def 4;

      then

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

      x in ( dom g) by A3, XBOOLE_0:def 4;

      then

       A5: (g . x) in ( rng g) by FUNCT_1:def 3;

      q = [(f . x), (g . x)] by A1, A2, Def7;

      hence thesis by A4, A5, ZFMISC_1: 87;

    end;

    theorem :: FUNCT_3:52

    

     Th52: for f,g be Function st ( dom f) = ( dom g) & ( rng f) c= Y & ( rng g) c= Z holds (( pr1 (Y,Z)) * <:f, g:>) = f & (( pr2 (Y,Z)) * <:f, g:>) = g

    proof

      let f,g be Function such that

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

       A2: ( rng f) c= Y & ( rng g) c= Z;

      

       A3: [:( rng f), ( rng g):] c= [:Y, Z:] by A2, ZFMISC_1: 96;

      

       A4: ( rng <:f, g:>) c= [:( rng f), ( rng g):] by Th51;

      ( dom ( pr1 (Y,Z))) = [:Y, Z:] by Def4;

      then

       A5: ( dom (( pr1 (Y,Z)) * <:f, g:>)) = ( dom <:f, g:>) by A3, A4, RELAT_1: 27, XBOOLE_1: 1;

      then

       A6: ( dom (( pr1 (Y,Z)) * <:f, g:>)) = ( dom f) by A1, Th50;

      for x be object holds x in ( dom f) implies ((( pr1 (Y,Z)) * <:f, g:>) . x) = (f . x)

      proof

        let x be object;

        assume

         A7: x in ( dom f);

        then

         A8: (f . x) in ( rng f) & (g . x) in ( rng g) by A1, FUNCT_1:def 3;

        

        thus ((( pr1 (Y,Z)) * <:f, g:>) . x) = (( pr1 (Y,Z)) . ( <:f, g:> . x)) by A6, A7, FUNCT_1: 12

        .= (( pr1 (Y,Z)) . ((f . x),(g . x))) by A5, A6, A7, Def7

        .= (f . x) by A2, A8, Def4;

      end;

      hence (( pr1 (Y,Z)) * <:f, g:>) = f by A6;

      ( dom ( pr2 (Y,Z))) = [:Y, Z:] by Def5;

      then

       A9: ( dom (( pr2 (Y,Z)) * <:f, g:>)) = ( dom <:f, g:>) by A3, A4, RELAT_1: 27, XBOOLE_1: 1;

      then

       A10: ( dom (( pr2 (Y,Z)) * <:f, g:>)) = ( dom g) by A1, Th50;

      for x be object holds x in ( dom g) implies ((( pr2 (Y,Z)) * <:f, g:>) . x) = (g . x)

      proof

        let x be object;

        assume

         A11: x in ( dom g);

        then

         A12: (f . x) in ( rng f) & (g . x) in ( rng g) by A1, FUNCT_1:def 3;

        

        thus ((( pr2 (Y,Z)) * <:f, g:>) . x) = (( pr2 (Y,Z)) . ( <:f, g:> . x)) by A10, A11, FUNCT_1: 12

        .= (( pr2 (Y,Z)) . ((f . x),(g . x))) by A9, A10, A11, Def7

        .= (g . x) by A2, A12, Def5;

      end;

      hence thesis by A10;

    end;

    theorem :: FUNCT_3:53

    

     Th53: <:( pr1 (X,Y)), ( pr2 (X,Y)):> = ( id [:X, Y:])

    proof

      ( dom ( pr1 (X,Y))) = [:X, Y:] & ( dom ( pr2 (X,Y))) = [:X, Y:] by Def4, Def5;

      then

       A1: ( dom <:( pr1 (X,Y)), ( pr2 (X,Y)):>) = [:X, Y:] by Th50;

      

       A2: for x,y be object st x in X & y in Y holds ( <:( pr1 (X,Y)), ( pr2 (X,Y)):> . (x,y)) = (( id [:X, Y:]) . (x,y))

      proof

        let x,y be object;

        assume

         A3: x in X & y in Y;

        then

         A4: [x, y] in [:X, Y:] by ZFMISC_1: 87;

        

        hence ( <:( pr1 (X,Y)), ( pr2 (X,Y)):> . (x,y)) = [(( pr1 (X,Y)) . (x,y)), (( pr2 (X,Y)) . (x,y))] by A1, Def7

        .= [x, (( pr2 (X,Y)) . (x,y))] by A3, Def4

        .= [x, y] by A3, Def5

        .= (( id [:X, Y:]) . (x,y)) by A4, FUNCT_1: 18;

      end;

      ( dom ( id [:X, Y:])) = [:X, Y:];

      hence thesis by A1, A2, Th6;

    end;

    theorem :: FUNCT_3:54

    

     Th54: for f,g,h,k be Function st ( dom f) = ( dom g) & ( dom k) = ( dom h) & <:f, g:> = <:k, h:> holds f = k & g = h

    proof

      let f,g,h,k be Function such that

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

       A2: ( dom k) = ( dom h) and

       A3: <:f, g:> = <:k, h:>;

      

       A4: ( dom <:f, g:>) = ( dom f) by A1, Th50;

      for x be object holds x in ( dom f) implies (f . x) = (k . x)

      proof

        let x be object;

        assume x in ( dom f);

        then ( <:f, g:> . x) = [(f . x), (g . x)] & ( <:k, h:> . x) = [(k . x), (h . x)] by A3, A4, Def7;

        hence thesis by A3, XTUPLE_0: 1;

      end;

      hence f = k by A2, A3, A4, Th50;

      

       A5: ( dom <:f, g:>) = ( dom g) by A1, Th50;

      for x be object holds x in ( dom g) implies (g . x) = (h . x)

      proof

        let x be object;

        assume x in ( dom g);

        then ( <:f, g:> . x) = [(f . x), (g . x)] & ( <:k, h:> . x) = [(k . x), (h . x)] by A3, A5, Def7;

        hence thesis by A3, XTUPLE_0: 1;

      end;

      hence thesis by A2, A3, A5, Th50;

    end;

    theorem :: FUNCT_3:55

    for f,g,h be Function holds <:(f * h), (g * h):> = ( <:f, g:> * h)

    proof

      let f,g,h be Function;

      for x be object holds x in ( dom <:(f * h), (g * h):>) iff x in ( dom ( <:f, g:> * h))

      proof

        let x be object;

        thus x in ( dom <:(f * h), (g * h):>) implies x in ( dom ( <:f, g:> * h))

        proof

          assume x in ( dom <:(f * h), (g * h):>);

          then

           A1: x in (( dom (f * h)) /\ ( dom (g * h))) by Def7;

          then

           A2: x in ( dom (f * h)) by XBOOLE_0:def 4;

          x in ( dom (g * h)) by A1, XBOOLE_0:def 4;

          then

           A3: (h . x) in ( dom g) by FUNCT_1: 11;

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

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

          then

           A4: (h . x) in ( dom <:f, g:>) by Def7;

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

          hence thesis by A4, FUNCT_1: 11;

        end;

        assume

         A5: x in ( dom ( <:f, g:> * h));

        then

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

        (h . x) in ( dom <:f, g:>) by A5, FUNCT_1: 11;

        then

         A7: (h . x) in (( dom f) /\ ( dom g)) by Def7;

        then (h . x) in ( dom g) by XBOOLE_0:def 4;

        then

         A8: x in ( dom (g * h)) by A6, FUNCT_1: 11;

        (h . x) in ( dom f) by A7, XBOOLE_0:def 4;

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

        then x in (( dom (f * h)) /\ ( dom (g * h))) by A8, XBOOLE_0:def 4;

        hence thesis by Def7;

      end;

      then

       A9: ( dom <:(f * h), (g * h):>) = ( dom ( <:f, g:> * h)) by TARSKI: 2;

      for x be object st x in ( dom <:(f * h), (g * h):>) holds ( <:(f * h), (g * h):> . x) = (( <:f, g:> * h) . x)

      proof

        let x be object;

        assume

         A10: x in ( dom <:(f * h), (g * h):>);

        then

         A11: x in (( dom (f * h)) /\ ( dom (g * h))) by Def7;

        then

         A12: x in ( dom (f * h)) by XBOOLE_0:def 4;

        then

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

        

         A14: x in ( dom (g * h)) by A11, XBOOLE_0:def 4;

        then

         A15: (h . x) in ( dom g) by FUNCT_1: 11;

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

        then

         A16: (h . x) in (( dom f) /\ ( dom g)) by A15, XBOOLE_0:def 4;

        

        thus ( <:(f * h), (g * h):> . x) = [((f * h) . x), ((g * h) . x)] by A10, Def7

        .= [(f . (h . x)), ((g * h) . x)] by A12, FUNCT_1: 12

        .= [(f . (h . x)), (g . (h . x))] by A14, FUNCT_1: 12

        .= ( <:f, g:> . (h . x)) by A16, Th48

        .= (( <:f, g:> * h) . x) by A13, FUNCT_1: 13;

      end;

      hence thesis by A9;

    end;

    theorem :: FUNCT_3:56

    for f,g be Function holds ( <:f, g:> .: A) c= [:(f .: A), (g .: A):]

    proof

      let f,g be Function;

      let y be object;

      assume y in ( <:f, g:> .: A);

      then

      consider x be object such that

       A1: x in ( dom <:f, g:>) and

       A2: x in A and

       A3: y = ( <:f, g:> . x) by FUNCT_1:def 6;

      

       A4: x in (( dom f) /\ ( dom g)) by A1, Def7;

      then x in ( dom f) by XBOOLE_0:def 4;

      then

       A5: (f . x) in (f .: A) by A2, FUNCT_1:def 6;

      x in ( dom g) by A4, XBOOLE_0:def 4;

      then

       A6: (g . x) in (g .: A) by A2, FUNCT_1:def 6;

      y = [(f . x), (g . x)] by A1, A3, Def7;

      hence thesis by A5, A6, ZFMISC_1:def 2;

    end;

    theorem :: FUNCT_3:57

    for f,g be Function holds ( <:f, g:> " [:B, C:]) = ((f " B) /\ (g " C))

    proof

      let f,g be Function;

      for x be object holds x in ( <:f, g:> " [:B, C:]) iff x in ((f " B) /\ (g " C))

      proof

        let x be object;

        thus x in ( <:f, g:> " [:B, C:]) implies x in ((f " B) /\ (g " C))

        proof

          assume

           A1: x in ( <:f, g:> " [:B, C:]);

          then ( <:f, g:> . x) in [:B, C:] by FUNCT_1:def 7;

          then

          consider y1,y2 be object such that

           A2: y1 in B and

           A3: y2 in C and

           A4: ( <:f, g:> . x) = [y1, y2] by ZFMISC_1:def 2;

          

           A5: x in ( dom <:f, g:>) by A1, FUNCT_1:def 7;

          then

           A6: x in (( dom f) /\ ( dom g)) by Def7;

          then

           A7: x in ( dom g) by XBOOLE_0:def 4;

          

           A8: [y1, y2] = [(f . x), (g . x)] by A4, A5, Def7;

          then y2 = (g . x) by XTUPLE_0: 1;

          then

           A9: x in (g " C) by A3, A7, FUNCT_1:def 7;

          

           A10: x in ( dom f) by A6, XBOOLE_0:def 4;

          y1 = (f . x) by A8, XTUPLE_0: 1;

          then x in (f " B) by A2, A10, FUNCT_1:def 7;

          hence thesis by A9, XBOOLE_0:def 4;

        end;

        assume

         A11: x in ((f " B) /\ (g " C));

        then

         A12: x in (g " C) by XBOOLE_0:def 4;

        then

         A13: x in ( dom g) by FUNCT_1:def 7;

        

         A14: x in (f " B) by A11, XBOOLE_0:def 4;

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

        then

         A15: x in (( dom f) /\ ( dom g)) by A13, XBOOLE_0:def 4;

        then

         A16: x in ( dom <:f, g:>) by Def7;

        

         A17: (g . x) in C by A12, FUNCT_1:def 7;

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

        then [(f . x), (g . x)] in [:B, C:] by A17, ZFMISC_1:def 2;

        then ( <:f, g:> . x) in [:B, C:] by A15, Th48;

        hence thesis by A16, FUNCT_1:def 7;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FUNCT_3:58

    

     Th58: for f be Function of X, Y holds for g be Function of X, Z st (Y = {} implies X = {} ) & (Z = {} implies X = {} ) holds <:f, g:> is Function of X, [:Y, Z:]

    proof

      let f be Function of X, Y;

      let g be Function of X, Z;

      assume

       A1: (Y = {} implies X = {} ) & (Z = {} implies X = {} );

      per cases ;

        suppose [:Y, Z:] = {} implies X = {} ;

        ( rng f) c= Y & ( rng g) c= Z by RELAT_1:def 19;

        then

         A2: [:( rng f), ( rng g):] c= [:Y, Z:] by ZFMISC_1: 96;

        ( dom f) = X & ( dom g) = X by A1, FUNCT_2:def 1;

        then

         A3: ( dom <:f, g:>) = X by Th50;

        ( rng <:f, g:>) c= [:( rng f), ( rng g):] by Th51;

        then ( rng <:f, g:>) c= [:Y, Z:] by A2;

        hence thesis by A3, FUNCT_2: 2;

      end;

        suppose [:Y, Z:] = {} & X <> {} ;

        hence thesis by A1;

      end;

    end;

    definition

      let X, D1, D2;

      let f1 be Function of X, D1;

      let f2 be Function of X, D2;

      :: original: <:

      redefine

      func <:f1,f2:> -> Function of X, [:D1, D2:] ;

      coherence by Th58;

    end

    theorem :: FUNCT_3:59

    for f1 be Function of C, D1 holds for f2 be Function of C, D2 holds for c be Element of C holds ( <:f1, f2:> . c) = [(f1 . c), (f2 . c)]

    proof

      let f1 be Function of C, D1;

      let f2 be Function of C, D2;

      let c be Element of C;

      ( dom f1) = C & ( dom f2) = C by FUNCT_2:def 1;

      hence thesis by Th49;

    end;

    theorem :: FUNCT_3:60

    for f be Function of X, Y holds for g be Function of X, Z holds ( rng <:f, g:>) c= [:Y, Z:]

    proof

      let f be Function of X, Y;

      let g be Function of X, Z;

      ( rng f) c= Y & ( rng g) c= Z by RELAT_1:def 19;

      then

       A1: [:( rng f), ( rng g):] c= [:Y, Z:] by ZFMISC_1: 96;

      ( rng <:f, g:>) c= [:( rng f), ( rng g):] by Th51;

      hence thesis by A1;

    end;

    theorem :: FUNCT_3:61

    

     Th61: for f be Function of X, Y holds for g be Function of X, Z st (Y = {} implies X = {} ) & (Z = {} implies X = {} ) holds (( pr1 (Y,Z)) * <:f, g:>) = f & (( pr2 (Y,Z)) * <:f, g:>) = g

    proof

      let f be Function of X, Y;

      let g be Function of X, Z;

      assume (Y = {} implies X = {} ) & (Z = {} implies X = {} );

      then

       A1: ( dom f) = X & ( dom g) = X by FUNCT_2:def 1;

      ( rng f) c= Y & ( rng g) c= Z by RELAT_1:def 19;

      hence thesis by A1, Th52;

    end;

    theorem :: FUNCT_3:62

    for f be Function of X, D1 holds for g be Function of X, D2 holds (( pr1 (D1,D2)) * <:f, g:>) = f & (( pr2 (D1,D2)) * <:f, g:>) = g by Th61;

    theorem :: FUNCT_3:63

    for f1,f2 be Function of X, Y holds for g1,g2 be Function of X, Z st (Y = {} implies X = {} ) & (Z = {} implies X = {} ) & <:f1, g1:> = <:f2, g2:> holds f1 = f2 & g1 = g2

    proof

      let f1,f2 be Function of X, Y;

      let g1,g2 be Function of X, Z;

      assume that

       A1: Y = {} implies X = {} and

       A2: Z = {} implies X = {} ;

      

       A3: ( dom g1) = X & ( dom g2) = X by A2, FUNCT_2:def 1;

      ( dom f1) = X & ( dom f2) = X by A1, FUNCT_2:def 1;

      hence thesis by A3, Th54;

    end;

    theorem :: FUNCT_3:64

    for f1,f2 be Function of X, D1 holds for g1,g2 be Function of X, D2 st <:f1, g1:> = <:f2, g2:> holds f1 = f2 & g1 = g2

    proof

      let f1,f2 be Function of X, D1;

      let g1,g2 be Function of X, D2;

      

       A1: ( dom g1) = X & ( dom g2) = X by FUNCT_2:def 1;

      ( dom f1) = X & ( dom f2) = X by FUNCT_2:def 1;

      hence thesis by A1, Th54;

    end;

    definition

      let f,g be Function;

      :: FUNCT_3:def8

      func [:f,g:] -> Function means

      : Def8: ( dom it ) = [:( dom f), ( dom g):] & for x,y be object st x in ( dom f) & y in ( dom g) holds (it . (x,y)) = [(f . x), (g . y)];

      existence

      proof

        deffunc F( object, object) = [(f . $1), (g . $2)];

        ex F be Function st ( dom F) = [:( dom f), ( dom g):] & for x,y be object st x in ( dom f) & y in ( dom g) holds (F . (x,y)) = F(x,y) from Lambda3;

        hence thesis;

      end;

      uniqueness

      proof

        let fg1,fg2 be Function such that

         A1: ( dom fg1) = [:( dom f), ( dom g):] and

         A2: for x,y be object st x in ( dom f) & y in ( dom g) holds (fg1 . (x,y)) = [(f . x), (g . y)] and

         A3: ( dom fg2) = [:( dom f), ( dom g):] and

         A4: for x,y be object st x in ( dom f) & y in ( dom g) holds (fg2 . (x,y)) = [(f . x), (g . y)];

        for p be object st p in [:( dom f), ( dom g):] holds (fg1 . p) = (fg2 . p)

        proof

          let p be object;

          assume p in [:( dom f), ( dom g):];

          then

          consider x,y be object such that

           A5: x in ( dom f) & y in ( dom g) and

           A6: p = [x, y] by ZFMISC_1:def 2;

          (fg1 . (x,y)) = [(f . x), (g . y)] & (fg2 . (x,y)) = [(f . x), (g . y)] by A2, A4, A5;

          hence thesis by A6;

        end;

        hence thesis by A1, A3;

      end;

    end

    theorem :: FUNCT_3:65

    

     Th65: for f,g be Function, x,y be object st [x, y] in [:( dom f), ( dom g):] holds ( [:f, g:] . (x,y)) = [(f . x), (g . y)]

    proof

      let f,g be Function, x,y be object;

      assume [x, y] in [:( dom f), ( dom g):];

      then x in ( dom f) & y in ( dom g) by ZFMISC_1: 87;

      hence thesis by Def8;

    end;

    theorem :: FUNCT_3:66

    

     Th66: for f,g be Function holds [:f, g:] = <:(f * ( pr1 (( dom f),( dom g)))), (g * ( pr2 (( dom f),( dom g)))):>

    proof

      let f,g be Function;

      

       A1: ( dom ( pr1 (( dom f),( dom g)))) = [:( dom f), ( dom g):] by Def4;

      

       A2: ( dom ( pr2 (( dom f),( dom g)))) = [:( dom f), ( dom g):] by Def5;

      ( rng ( pr2 (( dom f),( dom g)))) c= ( dom g) by Th45;

      then

       A3: ( dom (g * ( pr2 (( dom f),( dom g))))) = [:( dom f), ( dom g):] by A2, RELAT_1: 27;

      ( rng ( pr1 (( dom f),( dom g)))) c= ( dom f) by Th43;

      then ( dom (f * ( pr1 (( dom f),( dom g))))) = [:( dom f), ( dom g):] by A1, RELAT_1: 27;

      then

       A4: ( dom <:(f * ( pr1 (( dom f),( dom g)))), (g * ( pr2 (( dom f),( dom g)))):>) = [:( dom f), ( dom g):] by A3, Th50;

      

       A5: for x,y be object st x in ( dom f) & y in ( dom g) holds ( [:f, g:] . (x,y)) = ( <:(f * ( pr1 (( dom f),( dom g)))), (g * ( pr2 (( dom f),( dom g)))):> . (x,y))

      proof

        let x,y be object;

        assume

         A6: x in ( dom f) & y in ( dom g);

        then

         A7: [x, y] in [:( dom f), ( dom g):] by ZFMISC_1: 87;

        

        thus ( [:f, g:] . (x,y)) = [(f . x), (g . y)] by A6, Def8

        .= [(f . (( pr1 (( dom f),( dom g))) . (x,y))), (g . y)] by A6, Def4

        .= [(f . (( pr1 (( dom f),( dom g))) . (x,y))), (g . (( pr2 (( dom f),( dom g))) . (x,y)))] by A6, Def5

        .= [((f * ( pr1 (( dom f),( dom g)))) . (x,y)), (g . (( pr2 (( dom f),( dom g))) . (x,y)))] by A1, A7, FUNCT_1: 13

        .= [((f * ( pr1 (( dom f),( dom g)))) . (x,y)), ((g * ( pr2 (( dom f),( dom g)))) . (x,y))] by A2, A7, FUNCT_1: 13

        .= ( <:(f * ( pr1 (( dom f),( dom g)))), (g * ( pr2 (( dom f),( dom g)))):> . (x,y)) by A4, A7, Def7;

      end;

      ( dom [:f, g:]) = [:( dom f), ( dom g):] by Def8;

      hence thesis by A4, A5, Th6;

    end;

    theorem :: FUNCT_3:67

    

     Th67: for f,g be Function holds ( rng [:f, g:]) = [:( rng f), ( rng g):]

    proof

      let f,g be Function;

      for q be object holds q in ( rng [:f, g:]) iff q in [:( rng f), ( rng g):]

      proof

        let q be object;

        

         A1: ( dom [:f, g:]) = [:( dom f), ( dom g):] by Def8;

        thus q in ( rng [:f, g:]) implies q in [:( rng f), ( rng g):]

        proof

          assume q in ( rng [:f, g:]);

          then

          consider p be object such that

           A2: p in ( dom [:f, g:]) and

           A3: q = ( [:f, g:] . p) by FUNCT_1:def 3;

          p in [:( dom f), ( dom g):] by A2, Def8;

          then

          consider x,y be object such that

           A4: x in ( dom f) & y in ( dom g) and

           A5: p = [x, y] by ZFMISC_1:def 2;

          

           A6: (f . x) in ( rng f) & (g . y) in ( rng g) by A4, FUNCT_1:def 3;

          q = ( [:f, g:] . (x,y)) by A3, A5

          .= [(f . x), (g . y)] by A4, Def8;

          hence thesis by A6, ZFMISC_1: 87;

        end;

        assume q in [:( rng f), ( rng g):];

        then

        consider y1,y2 be object such that

         A7: y1 in ( rng f) and

         A8: y2 in ( rng g) and

         A9: q = [y1, y2] by ZFMISC_1:def 2;

        consider x2 be object such that

         A10: x2 in ( dom g) and

         A11: y2 = (g . x2) by A8, FUNCT_1:def 3;

        consider x1 be object such that

         A12: x1 in ( dom f) and

         A13: y1 = (f . x1) by A7, FUNCT_1:def 3;

        

         A14: [x1, x2] in [:( dom f), ( dom g):] by A12, A10, ZFMISC_1: 87;

        ( [:f, g:] . (x1,x2)) = q by A9, A12, A13, A10, A11, Def8;

        hence thesis by A14, A1, FUNCT_1:def 3;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FUNCT_3:68

    

     Th68: for f,g be Function st ( dom f) = X & ( dom g) = X holds <:f, g:> = ( [:f, g:] * ( delta X))

    proof

      let f,g be Function such that

       A1: ( dom f) = X & ( dom g) = X;

      

       A2: ( dom ( delta X)) = X by Def6;

      ( rng ( delta X)) c= [:X, X:] by Th47;

      then ( rng ( delta X)) c= ( dom [:f, g:]) by A1, Def8;

      then

       A3: ( dom ( [:f, g:] * ( delta X))) = X by A2, RELAT_1: 27;

      (( dom f) /\ ( dom g)) = X by A1;

      then

       A4: ( dom <:f, g:>) = X by Def7;

      for x be object st x in X holds ( <:f, g:> . x) = (( [:f, g:] * ( delta X)) . x)

      proof

        let x be object;

        assume

         A5: x in X;

        

        hence ( <:f, g:> . x) = [(f . x), (g . x)] by A4, Def7

        .= ( [:f, g:] . (x,x)) by A1, A5, Def8

        .= ( [:f, g:] . (( delta X) . x)) by A5, Def6

        .= (( [:f, g:] * ( delta X)) . x) by A3, A5, FUNCT_1: 12;

      end;

      hence thesis by A4, A3;

    end;

    theorem :: FUNCT_3:69

     [:( id X), ( id Y):] = ( id [:X, Y:])

    proof

      ( rng ( pr1 (X,Y))) c= X by Th43;

      then

       A1: (( id X) * ( pr1 (X,Y))) = ( pr1 (X,Y)) by RELAT_1: 53;

      ( rng ( pr2 (X,Y))) c= Y by Th45;

      then

       A2: (( id Y) * ( pr2 (X,Y))) = ( pr2 (X,Y)) by RELAT_1: 53;

      ( dom ( id X)) = X & ( dom ( id Y)) = Y;

      

      hence [:( id X), ( id Y):] = <:( pr1 (X,Y)), ( pr2 (X,Y)):> by A1, A2, Th66

      .= ( id [:X, Y:]) by Th53;

    end;

    theorem :: FUNCT_3:70

    for f,g,h,k be Function holds ( [:f, h:] * <:g, k:>) = <:(f * g), (h * k):>

    proof

      let f,g,h,k be Function;

      for x be object holds x in ( dom ( [:f, h:] * <:g, k:>)) iff x in ( dom <:(f * g), (h * k):>)

      proof

        let x be object;

        thus x in ( dom ( [:f, h:] * <:g, k:>)) implies x in ( dom <:(f * g), (h * k):>)

        proof

          assume

           A1: x in ( dom ( [:f, h:] * <:g, k:>));

          then

           A2: x in ( dom <:g, k:>) by FUNCT_1: 11;

          then

           A3: x in (( dom g) /\ ( dom k)) by Def7;

          then

           A4: x in ( dom g) by XBOOLE_0:def 4;

          

           A5: x in ( dom k) by A3, XBOOLE_0:def 4;

          ( <:g, k:> . x) in ( dom [:f, h:]) by A1, FUNCT_1: 11;

          then [(g . x), (k . x)] in ( dom [:f, h:]) by A2, Def7;

          then

           A6: [(g . x), (k . x)] in [:( dom f), ( dom h):] by Def8;

          then (k . x) in ( dom h) by ZFMISC_1: 87;

          then

           A7: x in ( dom (h * k)) by A5, FUNCT_1: 11;

          (g . x) in ( dom f) by A6, ZFMISC_1: 87;

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

          then x in (( dom (f * g)) /\ ( dom (h * k))) by A7, XBOOLE_0:def 4;

          hence thesis by Def7;

        end;

        assume x in ( dom <:(f * g), (h * k):>);

        then

         A8: x in (( dom (f * g)) /\ ( dom (h * k))) by Def7;

        then

         A9: x in ( dom (f * g)) by XBOOLE_0:def 4;

        

         A10: x in ( dom (h * k)) by A8, XBOOLE_0:def 4;

        then

         A11: x in ( dom k) by FUNCT_1: 11;

        x in ( dom g) by A9, FUNCT_1: 11;

        then x in (( dom g) /\ ( dom k)) by A11, XBOOLE_0:def 4;

        then

         A12: x in ( dom <:g, k:>) by Def7;

        

         A13: (k . x) in ( dom h) by A10, FUNCT_1: 11;

        (g . x) in ( dom f) by A9, FUNCT_1: 11;

        then [(g . x), (k . x)] in [:( dom f), ( dom h):] by A13, ZFMISC_1: 87;

        then [(g . x), (k . x)] in ( dom [:f, h:]) by Def8;

        then ( <:g, k:> . x) in ( dom [:f, h:]) by A12, Def7;

        hence thesis by A12, FUNCT_1: 11;

      end;

      then

       A14: ( dom ( [:f, h:] * <:g, k:>)) = ( dom <:(f * g), (h * k):>) by TARSKI: 2;

      for x be object st x in ( dom ( [:f, h:] * <:g, k:>)) holds (( [:f, h:] * <:g, k:>) . x) = ( <:(f * g), (h * k):> . x)

      proof

        let x be object;

        assume

         A15: x in ( dom ( [:f, h:] * <:g, k:>));

        then

         A16: x in ( dom <:g, k:>) by FUNCT_1: 11;

        then

         A17: x in (( dom g) /\ ( dom k)) by Def7;

        then

         A18: x in ( dom g) by XBOOLE_0:def 4;

        ( <:g, k:> . x) in ( dom [:f, h:]) by A15, FUNCT_1: 11;

        then [(g . x), (k . x)] in ( dom [:f, h:]) by A16, Def7;

        then

         A19: [(g . x), (k . x)] in [:( dom f), ( dom h):] by Def8;

        then

         A20: (g . x) in ( dom f) by ZFMISC_1: 87;

        

         A21: x in ( dom k) by A17, XBOOLE_0:def 4;

        

         A22: (k . x) in ( dom h) by A19, ZFMISC_1: 87;

        then

         A23: x in ( dom (h * k)) by A21, FUNCT_1: 11;

        x in ( dom (f * g)) by A20, A18, FUNCT_1: 11;

        then

         A24: x in (( dom (f * g)) /\ ( dom (h * k))) by A23, XBOOLE_0:def 4;

        

        thus (( [:f, h:] * <:g, k:>) . x) = ( [:f, h:] . ( <:g, k:> . x)) by A15, FUNCT_1: 12

        .= ( [:f, h:] . ((g . x),(k . x))) by A16, Def7

        .= [(f . (g . x)), (h . (k . x))] by A20, A22, Def8

        .= [((f * g) . x), (h . (k . x))] by A18, FUNCT_1: 13

        .= [((f * g) . x), ((h * k) . x)] by A21, FUNCT_1: 13

        .= ( <:(f * g), (h * k):> . x) by A24, Th48;

      end;

      hence thesis by A14;

    end;

    theorem :: FUNCT_3:71

    for f,g,h,k be Function holds ( [:f, h:] * [:g, k:]) = [:(f * g), (h * k):]

    proof

      let f,g,h,k be Function;

      

       A1: for x,y be object st x in ( dom (f * g)) & y in ( dom (h * k)) holds (( [:f, h:] * [:g, k:]) . (x,y)) = ( [:(f * g), (h * k):] . (x,y))

      proof

        let x,y be object such that

         A2: x in ( dom (f * g)) and

         A3: y in ( dom (h * k));

        

         A4: (g . x) in ( dom f) & (k . y) in ( dom h) by A2, A3, FUNCT_1: 11;

        

         A5: x in ( dom g) & y in ( dom k) by A2, A3, FUNCT_1: 11;

        then [x, y] in [:( dom g), ( dom k):] by ZFMISC_1: 87;

        then [x, y] in ( dom [:g, k:]) by Def8;

        

        hence (( [:f, h:] * [:g, k:]) . (x,y)) = ( [:f, h:] . ( [:g, k:] . (x,y))) by FUNCT_1: 13

        .= ( [:f, h:] . ((g . x),(k . y))) by A5, Def8

        .= [(f . (g . x)), (h . (k . y))] by A4, Def8

        .= [((f * g) . x), (h . (k . y))] by A2, FUNCT_1: 12

        .= [((f * g) . x), ((h * k) . y)] by A3, FUNCT_1: 12

        .= ( [:(f * g), (h * k):] . (x,y)) by A2, A3, Def8;

      end;

      for p be object holds p in ( dom ( [:f, h:] * [:g, k:])) iff p in [:( dom (f * g)), ( dom (h * k)):]

      proof

        let p be object;

        

         A6: ( dom [:g, k:]) = [:( dom g), ( dom k):] by Def8;

        

         A7: ( dom [:f, h:]) = [:( dom f), ( dom h):] by Def8;

        thus p in ( dom ( [:f, h:] * [:g, k:])) implies p in [:( dom (f * g)), ( dom (h * k)):]

        proof

          assume

           A8: p in ( dom ( [:f, h:] * [:g, k:]));

          then

           A9: ( [:g, k:] . p) in ( dom [:f, h:]) by FUNCT_1: 11;

          

           A10: p in ( dom [:g, k:]) by A8, FUNCT_1: 11;

          then

          consider x1,x2 be object such that

           A11: x1 in ( dom g) and

           A12: x2 in ( dom k) and

           A13: p = [x1, x2] by A6, ZFMISC_1:def 2;

          ( [:g, k:] . (x1,x2)) = ( [:g, k:] . p) by A13;

          then

           A14: [(g . x1), (k . x2)] in ( dom [:f, h:]) by A6, A10, A9, A13, Th65;

          then (k . x2) in ( dom h) by A7, ZFMISC_1: 87;

          then

           A15: x2 in ( dom (h * k)) by A12, FUNCT_1: 11;

          (g . x1) in ( dom f) by A7, A14, ZFMISC_1: 87;

          then x1 in ( dom (f * g)) by A11, FUNCT_1: 11;

          hence thesis by A13, A15, ZFMISC_1: 87;

        end;

        assume p in [:( dom (f * g)), ( dom (h * k)):];

        then

        consider x1,x2 be object such that

         A16: x1 in ( dom (f * g)) & x2 in ( dom (h * k)) and

         A17: p = [x1, x2] by ZFMISC_1:def 2;

        x1 in ( dom g) & x2 in ( dom k) by A16, FUNCT_1: 11;

        then

         A18: [x1, x2] in ( dom [:g, k:]) by A6, ZFMISC_1: 87;

        (g . x1) in ( dom f) & (k . x2) in ( dom h) by A16, FUNCT_1: 11;

        then [(g . x1), (k . x2)] in ( dom [:f, h:]) by A7, ZFMISC_1: 87;

        then ( [:g, k:] . (x1,x2)) in ( dom [:f, h:]) by A6, A18, Th65;

        hence thesis by A17, A18, FUNCT_1: 11;

      end;

      then

       A19: ( dom ( [:f, h:] * [:g, k:])) = [:( dom (f * g)), ( dom (h * k)):] by TARSKI: 2;

       [:( dom (f * g)), ( dom (h * k)):] = ( dom [:(f * g), (h * k):]) by Def8;

      hence thesis by A19, A1, Th6;

    end;

    theorem :: FUNCT_3:72

    for f,g be Function holds ( [:f, g:] .: [:B, A:]) = [:(f .: B), (g .: A):]

    proof

      let f,g be Function;

      for q be object holds q in ( [:f, g:] .: [:B, A:]) iff q in [:(f .: B), (g .: A):]

      proof

        let q be object;

        

         A1: [:( dom f), ( dom g):] = ( dom [:f, g:]) by Def8;

        thus q in ( [:f, g:] .: [:B, A:]) implies q in [:(f .: B), (g .: A):]

        proof

          assume q in ( [:f, g:] .: [:B, A:]);

          then

          consider p be object such that

           A2: p in ( dom [:f, g:]) and

           A3: p in [:B, A:] and

           A4: q = ( [:f, g:] . p) by FUNCT_1:def 6;

          ( dom [:f, g:]) = [:( dom f), ( dom g):] by Def8;

          then

          consider x,y be object such that

           A5: x in ( dom f) and

           A6: y in ( dom g) and

           A7: p = [x, y] by A2, ZFMISC_1:def 2;

          x in B by A3, A7, ZFMISC_1: 87;

          then

           A8: (f . x) in (f .: B) by A5, FUNCT_1:def 6;

          y in A by A3, A7, ZFMISC_1: 87;

          then

           A9: (g . y) in (g .: A) by A6, FUNCT_1:def 6;

          q = ( [:f, g:] . (x,y)) by A4, A7;

          then q = [(f . x), (g . y)] by A5, A6, Def8;

          hence thesis by A8, A9, ZFMISC_1: 87;

        end;

        assume q in [:(f .: B), (g .: A):];

        then

        consider y1,y2 be object such that

         A10: y1 in (f .: B) and

         A11: y2 in (g .: A) and

         A12: q = [y1, y2] by ZFMISC_1:def 2;

        consider x1 be object such that

         A13: x1 in ( dom f) and

         A14: x1 in B and

         A15: y1 = (f . x1) by A10, FUNCT_1:def 6;

        consider x2 be object such that

         A16: x2 in ( dom g) and

         A17: x2 in A and

         A18: y2 = (g . x2) by A11, FUNCT_1:def 6;

        

         A19: ( [:f, g:] . (x1,x2)) = [(f . x1), (g . x2)] by A13, A16, Def8;

         [x1, x2] in [:( dom f), ( dom g):] & [x1, x2] in [:B, A:] by A13, A14, A16, A17, ZFMISC_1: 87;

        hence thesis by A12, A15, A18, A1, A19, FUNCT_1:def 6;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FUNCT_3:73

    for f,g be Function holds ( [:f, g:] " [:B, A:]) = [:(f " B), (g " A):]

    proof

      let f,g be Function;

      for q be object holds q in ( [:f, g:] " [:B, A:]) iff q in [:(f " B), (g " A):]

      proof

        let q be object;

        thus q in ( [:f, g:] " [:B, A:]) implies q in [:(f " B), (g " A):]

        proof

          assume

           A1: q in ( [:f, g:] " [:B, A:]);

          then

           A2: ( [:f, g:] . q) in [:B, A:] by FUNCT_1:def 7;

          q in ( dom [:f, g:]) by A1, FUNCT_1:def 7;

          then q in [:( dom f), ( dom g):] by Def8;

          then

          consider x1,x2 be object such that

           A3: x1 in ( dom f) and

           A4: x2 in ( dom g) and

           A5: q = [x1, x2] by ZFMISC_1:def 2;

          ( [:f, g:] . q) = ( [:f, g:] . (x1,x2)) by A5;

          then

           A6: [(f . x1), (g . x2)] in [:B, A:] by A3, A4, A2, Def8;

          then (g . x2) in A by ZFMISC_1: 87;

          then

           A7: x2 in (g " A) by A4, FUNCT_1:def 7;

          (f . x1) in B by A6, ZFMISC_1: 87;

          then x1 in (f " B) by A3, FUNCT_1:def 7;

          hence thesis by A5, A7, ZFMISC_1: 87;

        end;

        assume q in [:(f " B), (g " A):];

        then

        consider x1,x2 be object such that

         A8: x1 in (f " B) & x2 in (g " A) and

         A9: q = [x1, x2] by ZFMISC_1:def 2;

        (f . x1) in B & (g . x2) in A by A8, FUNCT_1:def 7;

        then

         A10: [(f . x1), (g . x2)] in [:B, A:] by ZFMISC_1: 87;

        x1 in ( dom f) & x2 in ( dom g) by A8, FUNCT_1:def 7;

        then

         A11: [x1, x2] in [:( dom f), ( dom g):] & ( [:f, g:] . (x1,x2)) = [(f . x1), (g . x2)] by Def8, ZFMISC_1: 87;

         [:( dom f), ( dom g):] = ( dom [:f, g:]) by Def8;

        hence thesis by A9, A11, A10, FUNCT_1:def 7;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FUNCT_3:74

    

     Th74: for f be Function of X, Y holds for g be Function of V, Z holds [:f, g:] is Function of [:X, V:], [:Y, Z:]

    proof

      let f be Function of X, Y;

      let g be Function of V, Z;

      per cases ;

        suppose

         A1: [:Y, Z:] = {} implies [:X, V:] = {} ;

        now

          per cases by A1;

            suppose

             A2: [:Y, Z:] <> {} ;

            ( rng f) c= Y & ( rng g) c= Z by RELAT_1:def 19;

            then [:( rng f), ( rng g):] c= [:Y, Z:] by ZFMISC_1: 96;

            then

             A3: ( rng [:f, g:]) c= [:Y, Z:] by Th67;

            Z = {} implies V = {} by A2, ZFMISC_1: 90;

            then

             A4: ( dom g) = V by FUNCT_2:def 1;

            Y = {} implies X = {} by A2, ZFMISC_1: 90;

            then ( dom f) = X by FUNCT_2:def 1;

            then ( dom [:f, g:]) = [:X, V:] by A4, Def8;

            hence thesis by A3, FUNCT_2: 2;

          end;

            suppose

             A5: [:X, V:] = {} ;

            then X = {} or V = {} ;

            then ( dom f) = {} or ( dom g) = {} ;

            then [:( dom f), ( dom g):] = {} by ZFMISC_1: 90;

            then

             A6: ( dom [:f, g:]) = [:X, V:] by A5, Def8;

            ( rng f) c= Y & ( rng g) c= Z by RELAT_1:def 19;

            then [:( rng f), ( rng g):] c= [:Y, Z:] by ZFMISC_1: 96;

            then ( rng [:f, g:]) c= [:Y, Z:] by Th67;

            hence thesis by A6, FUNCT_2: 2;

          end;

        end;

        hence thesis;

      end;

        suppose

         A7: [:Y, Z:] = {} & [:X, V:] <> {} ;

        then Y = {} or Z = {} ;

        then f = {} or g = {} ;

        then [:( dom f), ( dom g):] = {} by ZFMISC_1: 90;

        then

         A8: ( dom [:f, g:]) = {} by Def8;

        then ( rng [:f, g:]) = {} & ( dom [:f, g:]) c= [:X, V:] by RELAT_1: 42;

        then

        reconsider R = [:f, g:] as Relation of [:X, V:], [:Y, Z:] by RELSET_1: 4, XBOOLE_1: 2;

         [:f, g:] = {} by A8;

        then R is quasi_total by A7, FUNCT_2:def 1;

        hence thesis;

      end;

    end;

    definition

      let X1, X2, Y1, Y2;

      let f1 be Function of X1, Y1;

      let f2 be Function of X2, Y2;

      :: original: [:

      redefine

      func [:f1,f2:] -> Function of [:X1, X2:], [:Y1, Y2:] ;

      coherence by Th74;

    end

    theorem :: FUNCT_3:75

    

     Th75: for f1 be Function of C1, D1 holds for f2 be Function of C2, D2 holds for c1 be Element of C1 holds for c2 be Element of C2 holds ( [:f1, f2:] . (c1,c2)) = [(f1 . c1), (f2 . c2)]

    proof

      let f1 be Function of C1, D1;

      let f2 be Function of C2, D2;

      let c1 be Element of C1;

      let c2 be Element of C2;

      ( dom f1) = C1 & ( dom f2) = C2 by FUNCT_2:def 1;

      hence thesis by Def8;

    end;

    theorem :: FUNCT_3:76

    for f1 be Function of X1, Y1 holds for f2 be Function of X2, Y2 st (Y1 = {} implies X1 = {} ) & (Y2 = {} implies X2 = {} ) holds [:f1, f2:] = <:(f1 * ( pr1 (X1,X2))), (f2 * ( pr2 (X1,X2))):>

    proof

      let f1 be Function of X1, Y1;

      let f2 be Function of X2, Y2;

      assume (Y1 = {} implies X1 = {} ) & (Y2 = {} implies X2 = {} );

      then ( dom f1) = X1 & ( dom f2) = X2 by FUNCT_2:def 1;

      hence thesis by Th66;

    end;

    theorem :: FUNCT_3:77

    for f1 be Function of X1, D1 holds for f2 be Function of X2, D2 holds [:f1, f2:] = <:(f1 * ( pr1 (X1,X2))), (f2 * ( pr2 (X1,X2))):>

    proof

      let f1 be Function of X1, D1;

      let f2 be Function of X2, D2;

      ( dom f1) = X1 & ( dom f2) = X2 by FUNCT_2:def 1;

      hence thesis by Th66;

    end;

    theorem :: FUNCT_3:78

    for f1 be Function of X, Y1 holds for f2 be Function of X, Y2 holds <:f1, f2:> = ( [:f1, f2:] * ( delta X))

    proof

      let f1 be Function of X, Y1;

      let f2 be Function of X, Y2;

      per cases ;

        suppose Y1 = {} or Y2 = {} ;

        then

         A1: ( dom f1) = {} or ( dom f2) = {} ;

        

         A2: ( dom [:f1, f2:]) = [:( dom f1), ( dom f2):] by Def8

        .= {} by A1, ZFMISC_1: 90;

        ( dom <:f1, f2:>) = (( dom f1) /\ ( dom f2)) by Def7

        .= {} by A1;

        

        hence <:f1, f2:> = ( {} * ( delta X))

        .= ( [:f1, f2:] * ( delta X)) by A2, RELAT_1: 41;

      end;

        suppose Y1 <> {} & Y2 <> {} ;

        then ( dom f1) = X & ( dom f2) = X by FUNCT_2:def 1;

        hence thesis by Th68;

      end;

    end;

    begin

    theorem :: FUNCT_3:79

    for f be Function holds (( pr1 (( dom f),( rng f))) .: f) = ( dom f)

    proof

      let f be Function;

      now

        let y be object;

        thus y in ( dom f) implies ex x be object st x in ( dom ( pr1 (( dom f),( rng f)))) & x in f & y = (( pr1 (( dom f),( rng f))) . x)

        proof

          assume

           A1: y in ( dom f);

          take [y, (f . y)];

          

           A2: (f . y) in ( rng f) by A1, FUNCT_1:def 3;

          then [y, (f . y)] in [:( dom f), ( rng f):] by A1, ZFMISC_1: 87;

          hence [y, (f . y)] in ( dom ( pr1 (( dom f),( rng f)))) by Def4;

          thus [y, (f . y)] in f by A1, FUNCT_1:def 2;

          

          thus y = (( pr1 (( dom f),( rng f))) . (y,(f . y))) by A1, A2, Def4

          .= (( pr1 (( dom f),( rng f))) . [y, (f . y)]);

        end;

        given x be object such that

         A3: x in ( dom ( pr1 (( dom f),( rng f)))) and x in f and

         A4: y = (( pr1 (( dom f),( rng f))) . x);

        consider x1,x2 be object such that

         A5: x1 in ( dom f) & x2 in ( rng f) and

         A6: x = [x1, x2] by A3, ZFMISC_1: 84;

        y = (( pr1 (( dom f),( rng f))) . (x1,x2)) by A4, A6;

        hence y in ( dom f) by A5, Def4;

      end;

      hence thesis by FUNCT_1:def 6;

    end;

    theorem :: FUNCT_3:80

    for A,B,C be non empty set, f,g be Function of A, [:B, C:] st (( pr1 (B,C)) * f) = (( pr1 (B,C)) * g) & (( pr2 (B,C)) * f) = (( pr2 (B,C)) * g) holds f = g

    proof

      let A,B,C be non empty set, f,g be Function of A, [:B, C:] such that

       A1: (( pr1 (B,C)) * f) = (( pr1 (B,C)) * g) & (( pr2 (B,C)) * f) = (( pr2 (B,C)) * g);

      now

        let a be Element of A;

        consider b1 be Element of B, c1 be Element of C such that

         A2: (f . a) = [b1, c1] by DOMAIN_1: 1;

        consider b2 be Element of B, c2 be Element of C such that

         A3: (g . a) = [b2, c2] by DOMAIN_1: 1;

        

         A4: (( pr1 (B,C)) . (g . a)) = ((( pr1 (B,C)) * g) . a) by FUNCT_2: 15;

        

         A5: (( pr1 (B,C)) . (f . a)) = ((( pr1 (B,C)) * f) . a) & (( pr2 (B,C)) . (f . a)) = ((( pr2 (B,C)) * f) . a) by FUNCT_2: 15;

        

         A6: (( pr2 (B,C)) . (b1,c1)) = c1 & (( pr2 (B,C)) . (b2,c2)) = c2 by Def5;

        (( pr1 (B,C)) . (b1,c1)) = b1 & (( pr1 (B,C)) . (b2,c2)) = b2 by Def4;

        hence (f . a) = (g . a) by A1, A2, A3, A6, A5, A4, FUNCT_2: 15;

      end;

      hence thesis;

    end;

    registration

      let F,G be one-to-one Function;

      cluster [:F, G:] -> one-to-one;

      coherence

      proof

        let z1,z2 be object such that

         A1: z1 in ( dom [:F, G:]) and

         A2: z2 in ( dom [:F, G:]) and

         A3: ( [:F, G:] . z1) = ( [:F, G:] . z2);

        

         A4: ( dom [:F, G:]) = [:( dom F), ( dom G):] by Def8;

        then

        consider x1,y1 be object such that

         A5: x1 in ( dom F) and

         A6: y1 in ( dom G) and

         A7: z1 = [x1, y1] by A1, ZFMISC_1: 84;

        

         A8: ( [:F, G:] . (x1,y1)) = [(F . x1), (G . y1)] by A5, A6, Def8;

        consider x2,y2 be object such that

         A9: x2 in ( dom F) and

         A10: y2 in ( dom G) and

         A11: z2 = [x2, y2] by A2, A4, ZFMISC_1: 84;

        

         A12: ( [:F, G:] . (x2,y2)) = [(F . x2), (G . y2)] by A9, A10, Def8;

        then (F . x1) = (F . x2) by A3, A7, A11, A8, XTUPLE_0: 1;

        then

         A13: x1 = x2 by A5, A9, FUNCT_1:def 4;

        (G . y1) = (G . y2) by A3, A7, A11, A8, A12, XTUPLE_0: 1;

        hence thesis by A6, A7, A10, A11, A13, FUNCT_1:def 4;

      end;

    end

    registration

      let A be set;

      cluster idempotent for BinOp of A;

      existence

      proof

        take ( pr1 (A,A));

        per cases ;

          suppose

           A1: A <> {} ;

          let a be Element of A;

          a in A by A1;

          hence (( pr1 (A,A)) . (a,a)) = a by Def4;

        end;

          suppose

           A2: A = {} ;

          let a be Element of A;

           not [a, a] in ( dom ( pr1 (A,A))) by A2;

          

          hence (( pr1 (A,A)) . (a,a)) = {} by FUNCT_1:def 2

          .= a by A2, SUBSET_1:def 1;

        end;

      end;

    end

    registration

      let A be set, b be idempotent BinOp of A;

      let a be Element of A;

      reduce (b . (a,a)) to a;

      reducibility by BINOP_1:def 4;

    end

    reserve A1,A2,B1,B2 for non empty set,

f for Function of A1, B1,

g for Function of A2, B2,

Y1 for non empty Subset of A1,

Y2 for non empty Subset of A2;

    definition

      let A1 be set, B1 be non empty set, f be Function of A1, B1, Y1 be Subset of A1;

      :: original: |

      redefine

      func f | Y1 -> Function of Y1, B1 ;

      coherence by FUNCT_2: 32;

    end

    theorem :: FUNCT_3:81

    ( [:f, g:] | [:Y1, Y2:] qua Subset of [:A1, A2:]) qua Function of [:Y1, Y2:], [:B1, B2:] = [:(f | Y1), (g | Y2):] qua Function of [:Y1, Y2:], [:B1, B2:]

    proof

      let a be Element of [:Y1, Y2:];

      consider a1 be Element of Y1, a2 be Element of Y2 such that

       A1: a = [a1, a2] by DOMAIN_1: 1;

      

       A2: ((g | Y2) . a2) = (g . a2) by FUNCT_1: 49;

      

       A3: ((f | Y1) . a1) = (f . a1) by FUNCT_1: 49;

      

      thus ( [:(f | Y1), (g | Y2):] . a) = ( [:(f | Y1), (g | Y2):] . (a1,a2)) by A1

      .= [(f . a1), (g . a2)] by A3, A2, Th75

      .= ( [:f, g:] . (a1,a2)) by Th75

      .= (( [:f, g:] | [:Y1, Y2:]) . a) by A1, FUNCT_1: 49;

    end;