funct_6.miz



    begin

    reserve x,y,y1,y2,z,a,b for object,

X,Y,Z,V1,V2 for set,

f,g,h,h9,f1,f2 for Function,

i for Nat,

P for Permutation of X,

D,D1,D2,D3 for non empty set,

d1 for Element of D1,

d2 for Element of D2,

d3 for Element of D3;

    theorem :: FUNCT_6:1

    

     Th1: ( product f) c= ( Funcs (( dom f),( Union f)))

    proof

      let x be object;

      assume x in ( product f);

      then

      consider g such that

       A1: x = g and

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

       A3: for x be object st x in ( dom f) holds (g . x) in (f . x) by CARD_3:def 5;

      ( rng g) c= ( Union f)

      proof

        let y be object;

        

         A4: ( Union f) = ( union ( rng f)) by CARD_3:def 4;

        assume y in ( rng g);

        then

        consider z be object such that

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

        y in (f . z) & (f . z) in ( rng f) by A2, A3, A5, FUNCT_1:def 3;

        hence thesis by A4, TARSKI:def 4;

      end;

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

    end;

    begin

    theorem :: FUNCT_6:2

    

     Th2: x in ( dom ( ~ f)) implies ex y,z be object st x = [y, z]

    proof

      assume

       A1: x in ( dom ( ~ f));

      ex X, Y st ( dom ( ~ f)) c= [:X, Y:] by FUNCT_4: 44;

      hence thesis by A1, RELAT_1:def 1;

    end;

    theorem :: FUNCT_6:3

    

     Th3: ( ~ ( [:X, Y:] --> z)) = ( [:Y, X:] --> z)

    proof

      

       A1: ( dom ( [:X, Y:] --> z)) = [:X, Y:];

      then

       A2: ( dom ( ~ ( [:X, Y:] --> z))) = [:Y, X:] by FUNCT_4: 46;

       A3:

      now

        let x be object;

        assume

         A4: x in [:Y, X:];

        then

        consider y1,y2 be object such that

         A5: x = [y2, y1] and

         A6: [y1, y2] in [:X, Y:] by A1, A2, FUNCT_4:def 2;

        

         A7: (( [:X, Y:] --> z) . (y1,y2)) = z by A6, FUNCOP_1: 7;

        (( [:Y, X:] --> z) . (y2,y1)) = z by A4, A5, FUNCOP_1: 7;

        then (( ~ ( [:X, Y:] --> z)) . (y2,y1)) = (( [:Y, X:] --> z) . (y2,y1)) by A1, A6, A7, FUNCT_4:def 2;

        hence (( ~ ( [:X, Y:] --> z)) . x) = (( [:Y, X:] --> z) . x) by A5;

      end;

      thus thesis by A2, A3;

    end;

    theorem :: FUNCT_6:4

    

     Th4: ( curry f) = ( curry' ( ~ f)) & ( uncurry f) = ( ~ ( uncurry' f))

    proof

      

       A1: ( dom ( curry ( ~ ( ~ f)))) = ( proj1 ( dom ( ~ ( ~ f)))) by FUNCT_5:def 1;

      

       A2: ( dom ( curry f)) = ( proj1 ( dom f)) by FUNCT_5:def 1;

      

       A3: ( dom ( curry ( ~ ( ~ f)))) = ( dom ( curry f))

      proof

        thus ( dom ( curry ( ~ ( ~ f)))) c= ( dom ( curry f))

        proof

          let x be object;

          assume x in ( dom ( curry ( ~ ( ~ f))));

          then

          consider y be object such that

           A4: [x, y] in ( dom ( ~ ( ~ f))) by A1, XTUPLE_0:def 12;

           [y, x] in ( dom ( ~ f)) by A4, FUNCT_4: 42;

          then [x, y] in ( dom f) by FUNCT_4: 42;

          hence thesis by A2, XTUPLE_0:def 12;

        end;

        let x be object;

        assume x in ( dom ( curry f));

        then

        consider y be object such that

         A5: [x, y] in ( dom f) by A2, XTUPLE_0:def 12;

         [y, x] in ( dom ( ~ f)) by A5, FUNCT_4: 42;

        then [x, y] in ( dom ( ~ ( ~ f))) by FUNCT_4: 42;

        hence thesis by A1, XTUPLE_0:def 12;

      end;

      

       A6: ( curry' ( ~ f)) = ( curry ( ~ ( ~ f))) by FUNCT_5:def 3;

      now

        let x be object;

        assume

         A7: x in ( dom ( curry f));

        reconsider g = (( curry f) . x), h = (( curry' ( ~ f)) . x) as Function;

        

         A8: ( dom g) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) by A7, FUNCT_5: 31;

        

         A9: ( dom h) = ( proj1 (( dom ( ~ f)) /\ [:( proj1 ( dom ( ~ f))), {x}:])) by A6, A3, A7, FUNCT_5: 34;

        

         A10: ( dom g) = ( dom h)

        proof

          thus ( dom g) c= ( dom h)

          proof

            let a be object;

            assume a in ( dom g);

            then

            consider b be object such that

             A11: [b, a] in (( dom f) /\ [: {x}, ( proj2 ( dom f)):]) by A8, XTUPLE_0:def 13;

             [b, a] in [: {x}, ( proj2 ( dom f)):] by A11, XBOOLE_0:def 4;

            then

             A12: [a, b] in [:( proj2 ( dom f)), {x}:] by ZFMISC_1: 88;

             [b, a] in ( dom f) by A11, XBOOLE_0:def 4;

            then

             A13: [a, b] in ( dom ( ~ f)) by FUNCT_4: 42;

            ( proj2 ( dom f)) = ( proj1 ( dom ( ~ f))) by FUNCT_5: 17;

            then [a, b] in (( dom ( ~ f)) /\ [:( proj1 ( dom ( ~ f))), {x}:]) by A13, A12, XBOOLE_0:def 4;

            hence thesis by A9, XTUPLE_0:def 12;

          end;

          let a be object;

          assume a in ( dom h);

          then

          consider b be object such that

           A14: [a, b] in (( dom ( ~ f)) /\ [:( proj1 ( dom ( ~ f))), {x}:]) by A9, XTUPLE_0:def 12;

           [a, b] in [:( proj1 ( dom ( ~ f))), {x}:] by A14, XBOOLE_0:def 4;

          then

           A15: [b, a] in [: {x}, ( proj1 ( dom ( ~ f))):] by ZFMISC_1: 88;

           [a, b] in ( dom ( ~ f)) by A14, XBOOLE_0:def 4;

          then

           A16: [b, a] in ( dom f) by FUNCT_4: 42;

          ( proj2 ( dom f)) = ( proj1 ( dom ( ~ f))) by FUNCT_5: 17;

          then [b, a] in (( dom f) /\ [: {x}, ( proj2 ( dom f)):]) by A16, A15, XBOOLE_0:def 4;

          hence thesis by A8, XTUPLE_0:def 13;

        end;

        now

          let a be object;

          assume

           A17: a in ( dom g);

          then

           A18: [x, a] in ( dom f) & (g . a) = (f . (x,a)) by A7, FUNCT_5: 31;

          (h . a) = (( ~ f) . (a,x)) by A6, A3, A7, A10, A17, FUNCT_5: 34;

          hence (g . a) = (h . a) by A18, FUNCT_4:def 2;

        end;

        hence (( curry f) . x) = (( curry' ( ~ f)) . x) by A10;

      end;

      hence ( curry f) = ( curry' ( ~ f)) by A6, A3;

      

       A19: ( dom ( uncurry f)) = ( dom ( ~ ( ~ ( uncurry f))))

      proof

        thus ( dom ( uncurry f)) c= ( dom ( ~ ( ~ ( uncurry f))))

        proof

          let a be object;

          assume

           A20: a in ( dom ( uncurry f));

          then

          consider x, g, y such that

           A21: a = [x, y] and x in ( dom f) and g = (f . x) and y in ( dom g) by FUNCT_5:def 2;

           [y, x] in ( dom ( ~ ( uncurry f))) by A20, A21, FUNCT_4: 42;

          hence thesis by A21, FUNCT_4: 42;

        end;

        let a be object;

        assume a in ( dom ( ~ ( ~ ( uncurry f))));

        then ex x,y be object st a = [y, x] & [x, y] in ( dom ( ~ ( uncurry f))) by FUNCT_4:def 2;

        hence thesis by FUNCT_4: 42;

      end;

       A22:

      now

        let a be object;

        assume a in ( dom ( ~ ( ~ ( uncurry f))));

        then

        consider x,y be object such that

         A23: a = [y, x] and

         A24: [x, y] in ( dom ( ~ ( uncurry f))) by FUNCT_4:def 2;

        (( ~ ( uncurry f)) . (x,y)) = (( uncurry f) . (y,x)) & (( ~ ( uncurry f)) . (x,y)) = (( ~ ( ~ ( uncurry f))) . (y,x)) by A24, FUNCT_4: 43, FUNCT_4:def 2;

        hence (( uncurry f) . a) = (( ~ ( ~ ( uncurry f))) . a) by A23;

      end;

      ( uncurry' f) = ( ~ ( uncurry f)) by FUNCT_5:def 4;

      hence thesis by A19, A22;

    end;

    theorem :: FUNCT_6:5

     [:X, Y:] <> {} implies ( curry ( [:X, Y:] --> z)) = (X --> (Y --> z)) & ( curry' ( [:X, Y:] --> z)) = (Y --> (X --> z))

    proof

      assume

       A1: [:X, Y:] <> {} ;

      

       A2: ( dom ( [:X, Y:] --> z)) = [:X, Y:];

       A4:

      now

        let x be object;

        assume

         A5: x in Y;

        then

        consider f such that

         A6: (( curry' ( [:X, Y:] --> z)) . x) = f & ( dom f) = X and ( rng f) c= ( rng ( [:X, Y:] --> z)) and

         A7: for y st y in X holds (f . y) = (( [:X, Y:] --> z) . (y,x)) by A1, A2, FUNCT_5: 32;

         A8:

        now

          let y be object;

          assume

           A9: y in X;

          then

           A10: (f . y) = (( [:X, Y:] --> z) . (y,x)) by A7;

          ((X --> z) . y) = z & [y, x] in [:X, Y:] by A5, A9, FUNCOP_1: 7, ZFMISC_1: 87;

          hence (f . y) = ((X --> z) . y) by A10, FUNCOP_1: 7;

        end;

        ((Y --> (X --> z)) . x) = (X --> z) by A5, FUNCOP_1: 7;

        hence (( curry' ( [:X, Y:] --> z)) . x) = ((Y --> (X --> z)) . x) by A6, A8;

      end;

       A12:

      now

        let x be object;

        assume

         A13: x in X;

        then

        consider f such that

         A14: (( curry ( [:X, Y:] --> z)) . x) = f & ( dom f) = Y and ( rng f) c= ( rng ( [:X, Y:] --> z)) and

         A15: for y st y in Y holds (f . y) = (( [:X, Y:] --> z) . (x,y)) by A1, A2, FUNCT_5: 29;

         A16:

        now

          let y be object;

          assume

           A17: y in Y;

          then

           A18: (f . y) = (( [:X, Y:] --> z) . (x,y)) by A15;

          ((Y --> z) . y) = z & [x, y] in [:X, Y:] by A13, A17, FUNCOP_1: 7, ZFMISC_1: 87;

          hence (f . y) = ((Y --> z) . y) by A18, FUNCOP_1: 7;

        end;

        ((X --> (Y --> z)) . x) = (Y --> z) by A13, FUNCOP_1: 7;

        hence (( curry ( [:X, Y:] --> z)) . x) = ((X --> (Y --> z)) . x) by A14, A16;

      end;

      ( dom (X --> (Y --> z))) = X & ( dom ( curry ( [:X, Y:] --> z))) = X by A1, A2, FUNCT_5: 24;

      hence ( curry ( [:X, Y:] --> z)) = (X --> (Y --> z)) by A12;

      ( dom (Y --> (X --> z))) = Y & ( dom ( curry' ( [:X, Y:] --> z))) = Y by A1, A2, FUNCT_5: 24;

      hence thesis by A4;

    end;

    theorem :: FUNCT_6:6

    ( uncurry (X --> (Y --> z))) = ( [:X, Y:] --> z) & ( uncurry' (X --> (Y --> z))) = ( [:Y, X:] --> z)

    proof

      

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

      

       A2: ( dom (Y --> z)) = Y;

      ( rng (Y --> z)) c= {z} by FUNCOP_1: 13;

      then (Y --> z) in ( Funcs (Y, {z})) by A2, FUNCT_2:def 2;

      then ( rng (X --> (Y --> z))) c= {(Y --> z)} & {(Y --> z)} c= ( Funcs (Y, {z})) by FUNCOP_1: 13, ZFMISC_1: 31;

      then ( rng (X --> (Y --> z))) c= ( Funcs (Y, {z}));

      then

       A3: ( dom ( uncurry (X --> (Y --> z)))) = [:X, Y:] by A1, FUNCT_5: 26;

       A4:

      now

        let x be object;

        assume

         A5: x in [:X, Y:];

        then

        consider y1, g, y2 such that

         A6: x = [y1, y2] and

         A7: y1 in X & g = ((X --> (Y --> z)) . y1) and

         A8: y2 in ( dom g) by A1, A3, FUNCT_5:def 2;

        

         A9: g = (Y --> z) by A7, FUNCOP_1: 7;

        then ((Y --> z) . y2) = z by A8, FUNCOP_1: 7;

        then z = (( uncurry (X --> (Y --> z))) . (y1,y2)) by A1, A7, A8, A9, FUNCT_5: 38;

        hence (( uncurry (X --> (Y --> z))) . x) = (( [:X, Y:] --> z) . x) by A5, A6, FUNCOP_1: 7;

      end;

      thus ( uncurry (X --> (Y --> z))) = ( [:X, Y:] --> z) by A3, A4;

      then ( ~ ( uncurry (X --> (Y --> z)))) = ( [:Y, X:] --> z) by Th3;

      hence thesis by FUNCT_5:def 4;

    end;

    theorem :: FUNCT_6:7

    

     Th7: x in ( dom f) & g = (f . x) implies ( rng g) c= ( rng ( uncurry f)) & ( rng g) c= ( rng ( uncurry' f))

    proof

      assume

       A1: x in ( dom f) & g = (f . x);

      thus ( rng g) c= ( rng ( uncurry f))

      proof

        let y be object;

        assume y in ( rng g);

        then ex z be object st z in ( dom g) & y = (g . z) by FUNCT_1:def 3;

        hence thesis by A1, FUNCT_5: 38;

      end;

      let y be object;

      assume y in ( rng g);

      then ex z be object st z in ( dom g) & y = (g . z) by FUNCT_1:def 3;

      hence thesis by A1, FUNCT_5: 39;

    end;

    theorem :: FUNCT_6:8

    

     Th8: ( dom ( uncurry (X --> f))) = [:X, ( dom f):] & ( rng ( uncurry (X --> f))) c= ( rng f) & ( dom ( uncurry' (X --> f))) = [:( dom f), X:] & ( rng ( uncurry' (X --> f))) c= ( rng f)

    proof

      f in ( Funcs (( dom f),( rng f))) by FUNCT_2:def 2;

      then ( rng (X --> f)) c= {f} & {f} c= ( Funcs (( dom f),( rng f))) by FUNCOP_1: 13, ZFMISC_1: 31;

      then ( dom (X --> f)) = X & ( rng (X --> f)) c= ( Funcs (( dom f),( rng f)));

      hence thesis by FUNCT_5: 26, FUNCT_5: 41;

    end;

    theorem :: FUNCT_6:9

    X <> {} implies ( rng ( uncurry (X --> f))) = ( rng f) & ( rng ( uncurry' (X --> f))) = ( rng f)

    proof

      set x = the Element of X;

      assume

       A1: X <> {} ;

      then ( dom (X --> f)) = X & ((X --> f) . x) = f by FUNCOP_1: 7;

      hence ( rng ( uncurry (X --> f))) c= ( rng f) & ( rng f) c= ( rng ( uncurry (X --> f))) & ( rng ( uncurry' (X --> f))) c= ( rng f) & ( rng f) c= ( rng ( uncurry' (X --> f))) by A1, Th7, Th8;

    end;

    theorem :: FUNCT_6:10

    

     Th10: [:X, Y:] <> {} & f in ( Funcs ( [:X, Y:],Z)) implies ( curry f) in ( Funcs (X,( Funcs (Y,Z)))) & ( curry' f) in ( Funcs (Y,( Funcs (X,Z))))

    proof

      assume

       A1: [:X, Y:] <> {} ;

      assume f in ( Funcs ( [:X, Y:],Z));

      then

       A2: ex g st f = g & ( dom g) = [:X, Y:] & ( rng g) c= Z by FUNCT_2:def 2;

      then ( rng ( curry f)) c= ( Funcs (Y,( rng f))) & ( Funcs (Y,( rng f))) c= ( Funcs (Y,Z)) by FUNCT_5: 35, FUNCT_5: 56;

      then

       A3: ( rng ( curry f)) c= ( Funcs (Y,Z));

      ( rng ( curry' f)) c= ( Funcs (X,( rng f))) & ( Funcs (X,( rng f))) c= ( Funcs (X,Z)) by A2, FUNCT_5: 35, FUNCT_5: 56;

      then

       A4: ( rng ( curry' f)) c= ( Funcs (X,Z));

      ( dom ( curry f)) = X & ( dom ( curry' f)) = Y by A1, A2, FUNCT_5: 24;

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

    end;

    theorem :: FUNCT_6:11

    

     Th11: f in ( Funcs (X,( Funcs (Y,Z)))) implies ( uncurry f) in ( Funcs ( [:X, Y:],Z)) & ( uncurry' f) in ( Funcs ( [:Y, X:],Z))

    proof

      assume f in ( Funcs (X,( Funcs (Y,Z))));

      then

       A1: ex g st f = g & ( dom g) = X & ( rng g) c= ( Funcs (Y,Z)) by FUNCT_2:def 2;

      then

       A2: ( dom ( uncurry f)) = [:X, Y:] & ( dom ( uncurry' f)) = [:Y, X:] by FUNCT_5: 26;

      ( rng ( uncurry f)) c= Z & ( rng ( uncurry' f)) c= Z by A1, FUNCT_5: 41;

      hence thesis by A2, FUNCT_2:def 2;

    end;

    theorem :: FUNCT_6:12

    (( curry f) in ( Funcs (X,( Funcs (Y,Z)))) or ( curry' f) in ( Funcs (Y,( Funcs (X,Z))))) & ( dom f) c= [:V1, V2:] implies f in ( Funcs ( [:X, Y:],Z))

    proof

      assume ( curry f) in ( Funcs (X,( Funcs (Y,Z)))) or ( curry' f) in ( Funcs (Y,( Funcs (X,Z))));

      then

       A1: ( uncurry ( curry f)) in ( Funcs ( [:X, Y:],Z)) or ( uncurry' ( curry' f)) in ( Funcs ( [:X, Y:],Z)) by Th11;

      assume ( dom f) c= [:V1, V2:];

      hence thesis by A1, FUNCT_5: 50;

    end;

    theorem :: FUNCT_6:13

    (( uncurry f) in ( Funcs ( [:X, Y:],Z)) or ( uncurry' f) in ( Funcs ( [:Y, X:],Z))) & ( rng f) c= ( PFuncs (V1,V2)) & ( dom f) = X implies f in ( Funcs (X,( Funcs (Y,Z))))

    proof

      assume that

       A1: ( uncurry f) in ( Funcs ( [:X, Y:],Z)) or ( uncurry' f) in ( Funcs ( [:Y, X:],Z)) and

       A2: ( rng f) c= ( PFuncs (V1,V2)) and

       A3: ( dom f) = X;

      

       A4: ( uncurry' f) = ( ~ ( uncurry f)) by FUNCT_5:def 4;

      

       A5: (ex g st ( uncurry f) = g & ( dom g) = [:X, Y:] & ( rng g) c= Z) or ex g st ( uncurry' f) = g & ( dom g) = [:Y, X:] & ( rng g) c= Z by A1, FUNCT_2:def 2;

      then

       A6: ( dom ( uncurry' f)) = [:Y, X:] by A4, FUNCT_4: 46;

      ( rng f) c= ( Funcs (Y,Z))

      proof

        let y be object;

        assume

         A7: y in ( rng f);

        then

        consider x be object such that

         A8: x in ( dom f) and

         A9: y = (f . x) by FUNCT_1:def 3;

        ex g st y = g & ( dom g) c= V1 & ( rng g) c= V2 by A2, A7, PARTFUN1:def 3;

        then

        reconsider h = y as Function;

        

         A10: ( dom h) = Y

        proof

          thus ( dom h) c= Y

          proof

            let z be object;

            assume z in ( dom h);

            then [z, x] in ( dom ( uncurry' f)) by A8, A9, FUNCT_5: 39;

            hence thesis by A6, ZFMISC_1: 87;

          end;

          let z be object;

          assume z in Y;

          then [z, x] in [:Y, X:] by A3, A8, ZFMISC_1: 87;

          then [x, z] in ( dom ( uncurry f)) by A4, A6, FUNCT_4: 42;

          then

          consider y1, f1, y2 such that

           A11: [x, z] = [y1, y2] and y1 in ( dom f) and

           A12: f1 = (f . y1) & y2 in ( dom f1) by FUNCT_5:def 2;

          x = y1 by A11, XTUPLE_0: 1;

          hence thesis by A9, A11, A12, XTUPLE_0: 1;

        end;

        ( rng h) c= Z

        proof

          let z be object;

          assume z in ( rng h);

          then ex y1 be object st y1 in ( dom h) & z = (h . y1) by FUNCT_1:def 3;

          then z in ( rng ( uncurry f)) & z in ( rng ( uncurry' f)) by A8, A9, FUNCT_5: 38, FUNCT_5: 39;

          hence thesis by A5;

        end;

        hence thesis by A10, FUNCT_2:def 2;

      end;

      hence thesis by A3, FUNCT_2:def 2;

    end;

    theorem :: FUNCT_6:14

    f in ( PFuncs ( [:X, Y:],Z)) implies ( curry f) in ( PFuncs (X,( PFuncs (Y,Z)))) & ( curry' f) in ( PFuncs (Y,( PFuncs (X,Z))))

    proof

      assume f in ( PFuncs ( [:X, Y:],Z));

      then

       A1: ex g st f = g & ( dom g) c= [:X, Y:] & ( rng g) c= Z by PARTFUN1:def 3;

      then ( proj1 [:X, Y:]) c= X & ( proj1 ( dom f)) c= ( proj1 [:X, Y:]) by FUNCT_5: 10, XTUPLE_0: 8;

      then ( proj1 ( dom f)) c= X;

      then

       A2: ( PFuncs (( proj1 ( dom f)),( rng f))) c= ( PFuncs (X,Z)) by A1, PARTFUN1: 50;

      ( proj2 [:X, Y:]) c= Y & ( proj2 ( dom f)) c= ( proj2 [:X, Y:]) by A1, FUNCT_5: 10, XTUPLE_0: 9;

      then ( proj2 ( dom f)) c= Y;

      then ( rng ( curry f)) c= ( PFuncs (( proj2 ( dom f)),( rng f))) & ( PFuncs (( proj2 ( dom f)),( rng f))) c= ( PFuncs (Y,Z)) by A1, FUNCT_5: 36, PARTFUN1: 50;

      then

       A3: ( rng ( curry f)) c= ( PFuncs (Y,Z));

      ( rng ( curry' f)) c= ( PFuncs (( proj1 ( dom f)),( rng f))) by FUNCT_5: 36;

      then

       A4: ( rng ( curry' f)) c= ( PFuncs (X,Z)) by A2;

      ( dom ( curry f)) c= X & ( dom ( curry' f)) c= Y by A1, FUNCT_5: 25;

      hence thesis by A3, A4, PARTFUN1:def 3;

    end;

    theorem :: FUNCT_6:15

    

     Th15: f in ( PFuncs (X,( PFuncs (Y,Z)))) implies ( uncurry f) in ( PFuncs ( [:X, Y:],Z)) & ( uncurry' f) in ( PFuncs ( [:Y, X:],Z))

    proof

      assume f in ( PFuncs (X,( PFuncs (Y,Z))));

      then

       A1: ex g st f = g & ( dom g) c= X & ( rng g) c= ( PFuncs (Y,Z)) by PARTFUN1:def 3;

      then ( dom ( uncurry f)) c= [:( dom f), Y:] & [:( dom f), Y:] c= [:X, Y:] by FUNCT_5: 37, ZFMISC_1: 96;

      then

       A2: ( dom ( uncurry f)) c= [:X, Y:];

      ( dom ( uncurry' f)) c= [:Y, ( dom f):] & [:Y, ( dom f):] c= [:Y, X:] by A1, FUNCT_5: 37, ZFMISC_1: 96;

      then

       A3: ( dom ( uncurry' f)) c= [:Y, X:];

      ( rng ( uncurry f)) c= Z & ( rng ( uncurry' f)) c= Z by A1, FUNCT_5: 40;

      hence thesis by A2, A3, PARTFUN1:def 3;

    end;

    theorem :: FUNCT_6:16

    (( curry f) in ( PFuncs (X,( PFuncs (Y,Z)))) or ( curry' f) in ( PFuncs (Y,( PFuncs (X,Z))))) & ( dom f) c= [:V1, V2:] implies f in ( PFuncs ( [:X, Y:],Z))

    proof

      assume ( curry f) in ( PFuncs (X,( PFuncs (Y,Z)))) or ( curry' f) in ( PFuncs (Y,( PFuncs (X,Z))));

      then

       A1: ( uncurry ( curry f)) in ( PFuncs ( [:X, Y:],Z)) or ( uncurry' ( curry' f)) in ( PFuncs ( [:X, Y:],Z)) by Th15;

      assume ( dom f) c= [:V1, V2:];

      hence thesis by A1, FUNCT_5: 50;

    end;

    theorem :: FUNCT_6:17

    (( uncurry f) in ( PFuncs ( [:X, Y:],Z)) or ( uncurry' f) in ( PFuncs ( [:Y, X:],Z))) & ( rng f) c= ( PFuncs (V1,V2)) & ( dom f) c= X implies f in ( PFuncs (X,( PFuncs (Y,Z))))

    proof

      assume that

       A1: ( uncurry f) in ( PFuncs ( [:X, Y:],Z)) or ( uncurry' f) in ( PFuncs ( [:Y, X:],Z)) and

       A2: ( rng f) c= ( PFuncs (V1,V2)) and

       A3: ( dom f) c= X;

      

       A4: (ex g st ( uncurry f) = g & ( dom g) c= [:X, Y:] & ( rng g) c= Z) or ex g st ( uncurry' f) = g & ( dom g) c= [:Y, X:] & ( rng g) c= Z by A1, PARTFUN1:def 3;

      ( uncurry' f) = ( ~ ( uncurry f)) by FUNCT_5:def 4;

      then

       A5: ( dom ( uncurry' f)) c= [:Y, X:] by A4, FUNCT_4: 45;

      ( rng f) c= ( PFuncs (Y,Z))

      proof

        let y be object;

        assume

         A6: y in ( rng f);

        then

        consider x be object such that

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

        ex g st y = g & ( dom g) c= V1 & ( rng g) c= V2 by A2, A6, PARTFUN1:def 3;

        then

        reconsider h = y as Function;

        

         A8: ( rng h) c= Z

        proof

          let z be object;

          assume z in ( rng h);

          then ex y1 be object st y1 in ( dom h) & z = (h . y1) by FUNCT_1:def 3;

          then z in ( rng ( uncurry f)) & z in ( rng ( uncurry' f)) by A7, FUNCT_5: 38, FUNCT_5: 39;

          hence thesis by A4;

        end;

        ( dom h) c= Y

        proof

          let z be object;

          assume z in ( dom h);

          then [z, x] in ( dom ( uncurry' f)) by A7, FUNCT_5: 39;

          hence thesis by A5, ZFMISC_1: 87;

        end;

        hence thesis by A8, PARTFUN1:def 3;

      end;

      hence thesis by A3, PARTFUN1:def 3;

    end;

    begin

    definition

      ::$Canceled

    end

    ::$Canceled

    definition

      let f be Function-yielding Function;

      :: FUNCT_6:def2

      func doms f -> Function means

      : Def1: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = ( proj1 (f . x));

      existence

      proof

        deffunc F( object) = ( proj1 (f . $1));

        ex F be Function st ( dom F) = ( dom f) & for x be object st x in ( dom f) 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) = ( dom f) and

         A2: for x be object st x in ( dom f) holds (f1 . x) = ( proj1 (f . x)) and

         A3: ( dom f2) = ( dom f) and

         A4: for x be object st x in ( dom f) holds (f2 . x) = ( proj1 (f . x));

        now

          let x be object;

          assume

           A5: x in ( dom f);

          then (f1 . x) = ( proj1 (f . x)) by A2;

          hence (f1 . x) = (f2 . x) by A4, A5;

        end;

        hence thesis by A1, A3;

      end;

      :: FUNCT_6:def3

      func rngs f -> Function means

      : Def2: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = ( proj2 (f . x));

      existence

      proof

        deffunc F( object) = ( proj2 (f . $1));

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

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

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

         A7: for x be object st x in ( dom f) holds (f1 . x) = ( proj2 (f . x)) and

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

         A9: for x be object st x in ( dom f) holds (f2 . x) = ( proj2 (f . x));

        now

          let x be object;

          assume

           A10: x in ( dom f);

          then (f1 . x) = ( proj2 (f . x)) by A7;

          hence (f1 . x) = (f2 . x) by A9, A10;

        end;

        hence thesis by A6, A8;

      end;

    end

    definition

      let f be Function;

      :: FUNCT_6:def4

      func meet f -> set equals ( meet ( rng f));

      correctness ;

    end

    theorem :: FUNCT_6:22

    

     Th18: for f be Function-yielding Function holds x in ( dom f) & g = (f . x) implies x in ( dom ( doms f)) & (( doms f) . x) = ( dom g) & x in ( dom ( rngs f)) & (( rngs f) . x) = ( rng g) by Def1, Def2;

    theorem :: FUNCT_6:23

    ( doms {} ) = {} & ( rngs {} ) = {} by Def1, Def2, RELAT_1: 38;

    theorem :: FUNCT_6:24

    

     Th20: ( doms (X --> f)) = (X --> ( dom f)) & ( rngs (X --> f)) = (X --> ( rng f))

    proof

      

       A1: ( dom (X --> ( dom f))) = X & ( dom ( doms (X --> f))) = ( dom (X --> f)) by Def1;

      

       A2: ( dom (X --> f)) = X & ((X --> f) " ( rng (X --> f))) = ( dom (X --> f)) by RELAT_1: 134;

      now

        let x be object;

        assume

         A3: x in X;

        then ((X --> f) . x) = f & ((X --> ( dom f)) . x) = ( dom f) by FUNCOP_1: 7;

        hence (( doms (X --> f)) . x) = ((X --> ( dom f)) . x) by A2, A3, Def1;

      end;

      hence ( doms (X --> f)) = (X --> ( dom f)) by A1;

       A4:

      now

        let x be object;

        assume

         A5: x in X;

        then ((X --> f) . x) = f & ((X --> ( rng f)) . x) = ( rng f) by FUNCOP_1: 7;

        hence (( rngs (X --> f)) . x) = ((X --> ( rng f)) . x) by A2, A5, Def2;

      end;

      ( dom (X --> ( rng f))) = X & ( dom ( rngs (X --> f))) = ( dom (X --> f)) by Def2;

      hence thesis by A4;

    end;

    theorem :: FUNCT_6:25

    

     Th21: f <> {} implies for x be object holds x in ( meet f) iff for y be object st y in ( dom f) holds x in (f . y)

    proof

      assume

       A1: f <> {} ;

      let x be object;

      thus x in ( meet f) implies for y be object st y in ( dom f) holds x in (f . y)

      proof

        assume

         A2: x in ( meet f);

        let y be object;

        assume y in ( dom f);

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

        then ( meet f) c= (f . y) by SETFAM_1: 3;

        hence thesis by A2;

      end;

      assume

       A3: for y be object st y in ( dom f) holds x in (f . y);

      now

        let z be set;

        assume z in ( rng f);

        then ex y be object st y in ( dom f) & z = (f . y) by FUNCT_1:def 3;

        hence x in z by A3;

      end;

      hence thesis by A1, SETFAM_1:def 1;

    end;

    theorem :: FUNCT_6:26

    ( Union ( {} --> Y)) = {} & ( meet ( {} --> Y)) = {}

    proof

      ( union ( rng ( {} --> Y))) = {} by ZFMISC_1: 2;

      hence thesis by CARD_3:def 4, SETFAM_1:def 1;

    end;

    theorem :: FUNCT_6:27

    

     Th23: X <> {} implies ( Union (X --> Y)) = Y & ( meet (X --> Y)) = Y

    proof

      assume X <> {} ;

      then

       A1: ( rng (X --> Y)) = {Y} by FUNCOP_1: 8;

      then ( union ( rng (X --> Y))) = Y by ZFMISC_1: 25;

      hence thesis by A1, CARD_3:def 4, SETFAM_1: 10;

    end;

    definition

      let f be Function, x,y be object;

      :: FUNCT_6:def5

      func f .. (x,y) -> set equals (( uncurry f) . (x,y));

      correctness ;

    end

    theorem :: FUNCT_6:28

    x in X & y in ( dom f) implies ((X --> f) .. (x,y)) = (f . y)

    proof

      

       A1: x in X implies ((X --> f) . x) = f by FUNCOP_1: 7;

      ( dom (X --> f)) = X;

      hence thesis by A1, FUNCT_5: 38;

    end;

    begin

    definition

      let f be Function-yielding Function;

      :: FUNCT_6:def6

      func <:f:> -> Function equals ( curry (( uncurry' f) | [:( meet ( doms f)), ( dom f):] qua set));

      correctness ;

    end

    theorem :: FUNCT_6:29

    

     Th25: for f be Function-yielding Function holds ( dom <:f:>) = ( meet ( doms f)) & ( rng <:f:>) c= ( product ( rngs f))

    proof

      let f be Function-yielding Function;

      set f9 = (( uncurry' f) | [:( meet ( doms f)), ( dom f):] qua set);

      ( dom (( uncurry' f) | [:( meet ( doms f)), ( dom f):] qua set)) c= [:( meet ( doms f)), ( dom f):] by RELAT_1: 58;

      hence

       A1: ( dom <:f:>) c= ( meet ( doms f)) by FUNCT_5: 25;

      

       A2: ( dom ( doms f)) = ( dom f) by Def1;

      thus ( meet ( doms f)) c= ( dom <:f:>)

      proof

        set y = the Element of ( rng ( doms f));

        let x be object;

        assume

         A3: x in ( meet ( doms f));

        then

         A4: ( rng ( doms f)) <> {} by SETFAM_1:def 1;

        then

         A5: x in y by A3, SETFAM_1:def 1;

        consider z be object such that

         A6: z in ( dom ( doms f)) and

         A7: y = (( doms f) . z) by A4, FUNCT_1:def 3;

        reconsider g = (f . z) as Function;

        

         A8: z in ( dom f) by A2, A6;

        then y = ( dom g) by A7, Th18;

        then

         A9: [x, z] in ( dom ( uncurry' f)) by A8, A5, FUNCT_5: 39;

         [x, z] in [:( meet ( doms f)), ( dom f):] by A3, A8, ZFMISC_1: 87;

        then [x, z] in (( dom ( uncurry' f)) /\ [:( meet ( doms f)), ( dom f):]) by A9, XBOOLE_0:def 4;

        then [x, z] in ( dom (( uncurry' f) | [:( meet ( doms f)), ( dom f):] qua set)) by RELAT_1: 61;

        then x in ( proj1 ( dom (( uncurry' f) | [:( meet ( doms f)), ( dom f):] qua set))) by XTUPLE_0:def 12;

        hence thesis by FUNCT_5:def 1;

      end;

      

       A10: ( dom ( rngs f)) = ( dom f) by Def2;

      thus ( rng <:f:>) c= ( product ( rngs f))

      proof

        let y be object;

        

         A11: ( dom f9) = (( dom ( uncurry' f)) /\ [:( meet ( doms f)), ( dom f):]) by RELAT_1: 61;

        

         A12: ( uncurry' f) = ( ~ ( uncurry f)) by FUNCT_5:def 4;

        assume y in ( rng <:f:>);

        then

        consider x be object such that

         A13: x in ( dom <:f:>) and

         A14: y = ( <:f:> . x) by FUNCT_1:def 3;

        reconsider g = y as Function by A14;

        

         A15: ( dom g) = ( proj2 (( dom f9) /\ [: {x}, ( proj2 ( dom f9)):])) by A13, A14, FUNCT_5: 31;

        

         A16: ( dom g) = ( dom ( rngs f))

        proof

          thus ( dom g) c= ( dom ( rngs f))

          proof

            let z be object;

            assume z in ( dom g);

            then [x, z] in ( dom f9) by A13, A14, FUNCT_5: 31;

            then [x, z] in ( dom ( uncurry' f)) by A11, XBOOLE_0:def 4;

            then [z, x] in ( dom ( uncurry f)) by A12, FUNCT_4: 42;

            then

            consider y1, h, y2 such that

             A17: [z, x] = [y1, y2] and

             A18: y1 in ( dom f) and h = (f . y1) and y2 in ( dom h) by FUNCT_5:def 2;

            

             A19: z = y1 by A17, XTUPLE_0: 1;

            thus thesis by A10, A18, A19;

          end;

          let z be object;

          

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

          assume

           A21: z in ( dom ( rngs f));

          reconsider h = (f . z) as Function;

          

           A22: z in ( dom f) by A10, A21;

          then ( dom h) = (( doms f) . z) by Th18;

          then ( dom h) in ( rng ( doms f)) by A2, A10, A21, FUNCT_1:def 3;

          then x in ( dom h) by A1, A13, SETFAM_1:def 1;

          then [z, x] in ( dom ( uncurry f)) by A22, FUNCT_5:def 2;

          then

           A23: [x, z] in ( dom ( uncurry' f)) by A12, FUNCT_4: 42;

           [x, z] in [:( meet ( doms f)), ( dom f):] by A1, A13, A22, ZFMISC_1: 87;

          then

           A24: [x, z] in ( dom f9) by A11, A23, XBOOLE_0:def 4;

          then z in ( proj2 ( dom f9)) by XTUPLE_0:def 13;

          then [x, z] in [: {x}, ( proj2 ( dom f9)):] by A20, ZFMISC_1: 87;

          then [x, z] in (( dom f9) /\ [: {x}, ( proj2 ( dom f9)):]) by A24, XBOOLE_0:def 4;

          hence thesis by A15, XTUPLE_0:def 13;

        end;

        now

          let z be object;

          assume

           A25: z in ( dom ( rngs f));

          reconsider h = (f . z) as Function;

          

           A26: z in ( dom f) by A10, A25;

          then ( dom h) = (( doms f) . z) by Th18;

          then ( dom h) in ( rng ( doms f)) by A2, A10, A25, FUNCT_1:def 3;

          then

           A27: x in ( dom h) by A1, A13, SETFAM_1:def 1;

          then

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

          (g . z) = (f9 . (x,z)) & [x, z] in ( dom f9) by A13, A14, A16, A25, FUNCT_5: 31;

          then (( uncurry' f) . (x,z)) = (g . z) by FUNCT_1: 47;

          then (g . z) = (h . x) by A26, A27, FUNCT_5: 39;

          hence (g . z) in (( rngs f) . z) by A26, A28, Th18;

        end;

        hence thesis by A16, CARD_3:def 5;

      end;

    end;

    registration

      let f be Function-yielding Function;

      cluster <:f:> -> Function-yielding;

      coherence ;

    end

    ::$Canceled

    theorem :: FUNCT_6:31

    

     Th26: for f be Function-yielding Function holds x in ( dom <:f:>) & g = ( <:f:> . x) implies ( dom g) = ( dom f) & for y st y in ( dom g) holds [y, x] in ( dom ( uncurry f)) & (g . y) = (( uncurry f) . (y,x))

    proof

      let f be Function-yielding Function;

      

       A1: ( rng <:f:>) c= ( product ( rngs f)) & ( dom ( rngs f)) = ( dom f) by Def2, Th25;

      assume

       A2: x in ( dom <:f:>) & g = ( <:f:> . x);

      then g in ( rng <:f:>) by FUNCT_1:def 3;

      hence ( dom g) = ( dom f) by A1, CARD_3: 9;

      let y such that

       A3: y in ( dom g);

      

       A4: [x, y] in ( dom (( uncurry' f) | [:( meet ( doms f)), ( dom f):] qua set)) by A2, A3, FUNCT_5: 31;

      then [x, y] in (( dom ( uncurry' f)) /\ [:( meet ( doms f)), ( dom f):]) by RELAT_1: 61;

      then

       A5: [x, y] in ( dom ( uncurry' f)) by XBOOLE_0:def 4;

      (g . y) = ((( uncurry' f) | [:( meet ( doms f)), ( dom f):] qua set) . (x,y)) by A2, A3, FUNCT_5: 31;

      then

       A6: (g . y) = (( uncurry' f) . (x,y)) by A4, FUNCT_1: 47;

      ( ~ ( uncurry f)) = ( uncurry' f) by FUNCT_5:def 4;

      hence thesis by A6, A5, FUNCT_4: 42, FUNCT_4: 43;

    end;

    theorem :: FUNCT_6:32

    

     Th27: for f be Function-yielding Function st x in ( dom <:f:>) holds for g st g in ( rng f) holds x in ( dom g)

    proof

      let f be Function-yielding Function;

      assume

       A1: x in ( dom <:f:>);

      let g;

      assume g in ( rng f);

      then

      consider y be object such that

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

      y in ( dom ( doms f)) & (( doms f) . y) = ( dom g) by A2, Th18;

      then ( dom g) in ( rng ( doms f)) by FUNCT_1:def 3;

      then

       A3: ( meet ( rng ( doms f))) c= ( dom g) by SETFAM_1: 3;

      ( meet ( doms f)) = ( dom <:f:>) by Th25;

      hence thesis by A1, A3;

    end;

    theorem :: FUNCT_6:33

    for x be object, f be Function-yielding Function st g in ( rng f) & for g st g in ( rng f) holds x in ( dom g) holds x in ( dom <:f:>)

    proof

      let x be object, f be Function-yielding Function;

      assume that

       A1: g in ( rng f) and

       A2: for g st g in ( rng f) holds x in ( dom g);

      ex y be object st y in ( dom f) & g = (f . y) by A1, FUNCT_1:def 3;

      then

       A3: ( doms f) <> {} by Th18;

       A4:

      now

        let y be object;

        assume y in ( dom ( doms f));

        then

         A5: y in ( dom f) by Def1;

        reconsider g = (f . y) as Function;

        

         A6: y in ( dom f) by A5;

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

        then x in ( dom g) by A2;

        hence x in (( doms f) . y) by A6, Th18;

      end;

      ( dom <:f:>) = ( meet ( doms f)) by Th25;

      hence thesis by A3, A4, Th21;

    end;

    theorem :: FUNCT_6:34

    

     Th29: for f be Function-yielding Function st x in ( dom f) & g = (f . x) & y in ( dom <:f:>) & h = ( <:f:> . y) holds (g . y) = (h . x)

    proof

      let f be Function-yielding Function;

      assume that

       A1: x in ( dom f) & g = (f . x) and

       A2: y in ( dom <:f:>) and

       A3: h = ( <:f:> . y);

      ( dom h) = ( dom f) by A2, A3, Th26;

      then x in ( dom h) by A1;

      then

       A4: (h . x) = (( uncurry f) . (x,y)) by A2, A3, Th26;

      g in ( rng f) by A1, FUNCT_1:def 3;

      then y in ( dom g) by A2, Th27;

      hence thesis by A1, A4, FUNCT_5: 38;

    end;

    theorem :: FUNCT_6:35

    for f be Function-yielding Function st x in ( dom f) & (f . x) is Function & y in ( dom <:f:>) holds (f .. (x,y)) = ( <:f:> .. (y,x))

    proof

      let f be Function-yielding Function;

      assume that

       A1: x in ( dom f) and (f . x) is Function and

       A2: y in ( dom <:f:>);

      reconsider g = (f . x), h = ( <:f:> . y) as Function;

      

       A3: ( dom h) = ( dom f) by A2, Th26;

      

       A4: g in ( rng f) by A1, FUNCT_1:def 3;

      

       A5: x in ( dom h) by A1, A3;

      y in ( dom g) by A2, A4, Th27;

      

      hence (f .. (x,y)) = (g . y) by A1, FUNCT_5: 38

      .= (h . x) by A1, A2, Th29

      .= ( <:f:> .. (y,x)) by A2, A5, FUNCT_5: 38;

    end;

    definition

      let f be Function-yielding Function;

      :: FUNCT_6:def7

      func Frege f -> Function means

      : Def6: ( dom it ) = ( product ( doms f)) & for g st g in ( product ( doms f)) holds ex h st (it . g) = h & ( dom h) = ( dom f) & for x st x in ( dom h) holds (h . x) = (( uncurry f) . (x,(g . x)));

      existence

      proof

        defpred P[ object, object] means ex g, h st $1 = g & $2 = h & ( dom h) = ( dom f) & for z st z in ( dom h) holds (h . z) = (( uncurry f) . (z,(g . z)));

        

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

        proof

          let x be object;

          assume x in ( product ( doms f));

          then

          consider g such that

           A2: x = g and ( dom g) = ( dom ( doms f)) and for x be object st x in ( dom ( doms f)) holds (g . x) in (( doms f) . x) by CARD_3:def 5;

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

          consider h such that

           A3: ( dom h) = ( dom f) & for z be object st z in ( dom f) holds (h . z) = F(z) from FUNCT_1:sch 3;

          reconsider y = h as set;

          take y, g, h;

          thus thesis by A2, A3;

        end;

        consider F be Function such that

         A4: ( dom F) = ( product ( doms f)) & for x be object st x in ( product ( doms f)) holds P[x, (F . x)] from CLASSES1:sch 1( A1);

        take F;

        thus ( dom F) = ( product ( doms f)) by A4;

        let g;

        assume g in ( product ( doms f));

        then ex g1,h be Function st g = g1 & (F . g) = h & ( dom h) = ( dom f) & for z st z in ( dom h) holds (h . z) = (( uncurry f) . (z,(g1 . z))) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function such that

         A5: ( dom f1) = ( product ( doms f)) and

         A6: for g st g in ( product ( doms f)) holds ex h st (f1 . g) = h & ( dom h) = ( dom f) & for x st x in ( dom h) holds (h . x) = (( uncurry f) . (x,(g . x))) and

         A7: ( dom f2) = ( product ( doms f)) and

         A8: for g st g in ( product ( doms f)) holds ex h st (f2 . g) = h & ( dom h) = ( dom f) & for x st x in ( dom h) holds (h . x) = (( uncurry f) . (x,(g . x)));

        now

          let x be object;

          assume

           A9: x in ( product ( doms f));

          then

          consider g such that

           A10: x = g and ( dom g) = ( dom ( doms f)) and for x be object st x in ( dom ( doms f)) holds (g . x) in (( doms f) . x) by CARD_3:def 5;

          consider h2 be Function such that

           A11: (f2 . g) = h2 and

           A12: ( dom h2) = ( dom f) and

           A13: for y st y in ( dom h2) holds (h2 . y) = (( uncurry f) . (y,(g . y))) by A8, A9, A10;

          consider h1 be Function such that

           A14: (f1 . g) = h1 and

           A15: ( dom h1) = ( dom f) and

           A16: for y st y in ( dom h1) holds (h1 . y) = (( uncurry f) . (y,(g . y))) by A6, A9, A10;

          now

            let z be object;

            assume

             A17: z in ( dom f);

            then (h1 . z) = (( uncurry f) . (z,(g . z))) by A15, A16;

            hence (h1 . z) = (h2 . z) by A12, A13, A17;

          end;

          hence (f1 . x) = (f2 . x) by A10, A14, A15, A11, A12, FUNCT_1: 2;

        end;

        hence thesis by A5, A7;

      end;

    end

    theorem :: FUNCT_6:36

    for f be Function-yielding Function st g in ( product ( doms f)) & x in ( dom g) holds (( Frege f) .. (g,x)) = (f .. (x,(g . x)))

    proof

      let f be Function-yielding Function;

      assume that

       A1: g in ( product ( doms f)) and

       A2: x in ( dom g);

      

       A3: ( dom g) = ( dom ( doms f)) by A1, CARD_3: 9;

      

       A4: ( dom ( doms f)) = ( dom f) by Def1;

      consider h such that

       A5: (( Frege f) . g) = h and

       A6: ( dom h) = ( dom f) and

       A7: for x st x in ( dom h) holds (h . x) = (( uncurry f) . (x,(g . x))) by A1, Def6;

      ( dom ( Frege f)) = ( product ( doms f)) by Def6;

      

      hence (( Frege f) .. (g,x)) = (h . x) by A1, A2, A5, A6, A3, A4, FUNCT_5: 38

      .= (f .. (x,(g . x))) by A2, A6, A7, A3, A4;

    end;

    

     Lm1: for f be Function-yielding Function holds ( rng ( Frege f)) c= ( product ( rngs f))

    proof

      let f be Function-yielding Function;

      let x be object;

      assume x in ( rng ( Frege f));

      then

      consider y be object such that

       A1: y in ( dom ( Frege f)) and

       A2: x = (( Frege f) . y) by FUNCT_1:def 3;

      

       A3: ( dom ( Frege f)) = ( product ( doms f)) by Def6;

      then

      consider g such that

       A4: y = g and ( dom g) = ( dom ( doms f)) and

       A5: for z be object st z in ( dom ( doms f)) holds (g . z) in (( doms f) . z) by A1, CARD_3:def 5;

      consider h such that

       A6: (( Frege f) . g) = h and

       A7: ( dom h) = ( dom f) and

       A8: for z st z in ( dom h) holds (h . z) = (( uncurry f) . (z,(g . z))) by A1, A3, A4, Def6;

      

       A9: ( dom ( rngs f)) = ( dom f) by Def2;

      

       A10: ( dom ( doms f)) = ( dom f) by Def1;

      now

        let z be object;

        assume

         A11: z in ( dom ( rngs f));

        reconsider t = (f . z) as Function;

        

         A12: (g . z) in (( doms f) . z) by A5, A9, A10, A11;

        

         A13: z in ( dom f) by A9, A11;

        then

         A14: (( rngs f) . z) = ( rng t) by Th18;

        

         A15: (( doms f) . z) = ( dom t) by A13, Th18;

        then

         A16: (t . (g . z)) in ( rng t) by A12, FUNCT_1:def 3;

        (t . (g . z)) = (( uncurry f) . (z,(g . z))) by A13, A12, A15, FUNCT_5: 38;

        hence (h . z) in (( rngs f) . z) by A7, A8, A9, A11, A14, A16;

      end;

      hence thesis by A2, A4, A6, A7, A9, CARD_3:def 5;

    end;

    theorem :: FUNCT_6:37

    for f be Function-yielding Function st x in ( dom f) & g = (f . x) & h in ( product ( doms f)) & h9 = (( Frege f) . h) holds (h . x) in ( dom g) & (h9 . x) = (g . (h . x)) & h9 in ( product ( rngs f))

    proof

      let f be Function-yielding Function;

      assume that

       A1: x in ( dom f) & g = (f . x) and

       A2: h in ( product ( doms f)) and

       A3: h9 = (( Frege f) . h);

      

       A4: x in ( dom f) by A1;

      

       A5: ( dom ( doms f)) = ( dom f) by Def1;

      (ex f2 st h = f2 & ( dom f2) = ( dom ( doms f)) & for x be object st x in ( dom ( doms f)) holds (f2 . x) in (( doms f) . x)) & (( doms f) . x) = ( dom g) by A1, A2, Th18, CARD_3:def 5;

      hence

       A6: (h . x) in ( dom g) by A5, A4;

      ex f1 st (( Frege f) . h) = f1 & ( dom f1) = ( dom f) & for x st x in ( dom f1) holds (f1 . x) = (( uncurry f) . (x,(h . x))) by A2, Def6;

      

      hence (h9 . x) = (( uncurry f) . (x,(h . x))) by A3, A4

      .= (g . (h . x)) by A1, A6, FUNCT_5: 38;

      

       A7: ( rng ( Frege f)) c= ( product ( rngs f)) by Lm1;

      ( dom ( Frege f)) = ( product ( doms f)) by Def6;

      then h9 in ( rng ( Frege f)) by A2, A3, FUNCT_1:def 3;

      hence thesis by A7;

    end;

    

     Lm2: for f be Function-yielding Function holds ( product ( rngs f)) c= ( rng ( Frege f))

    proof

      let f be Function-yielding Function;

      let x be object;

      deffunc F( object) = (( doms f) . $1);

      assume x in ( product ( rngs f));

      then

      consider g such that

       A1: x = g and

       A2: ( dom g) = ( dom ( rngs f)) and

       A3: for y be object st y in ( dom ( rngs f)) holds (g . y) in (( rngs f) . y) by CARD_3:def 5;

      defpred P[ object, object] means ex f1 st f1 = (f . $1) & (f1 . $2) = (g . $1);

      consider h such that

       A4: ( dom h) = ( dom f) & for x be object st x in ( dom f) holds for y be object holds y in (h . x) iff y in F(x) & P[x, y] from CARD_3:sch 2;

      

       A5: ( product ( doms f)) = ( dom ( Frege f)) by Def6;

      

       A6: ( dom ( doms f)) = ( dom f) by Def1;

      

       A7: ( dom ( rngs f)) = ( dom f) by Def2;

       A8:

      now

        let X;

        assume X in ( rng h);

        then

        consider x be object such that

         A9: x in ( dom h) and

         A10: X = (h . x) by FUNCT_1:def 3;

        reconsider fx = (f . x) as Function;

        

         A11: x in ( dom f) by A4, A9;

        then

         A12: (( rngs f) . x) = ( rng fx) by Th18;

        (g . x) in (( rngs f) . x) by A3, A7, A4, A9;

        then

         A13: ex y be object st y in ( dom fx) & (g . x) = (fx . y) by A12, FUNCT_1:def 3;

        (( doms f) . x) = ( dom fx) by A11, Th18;

        hence X <> {} by A4, A9, A10, A13;

      end;

       A14:

      now

        assume ( dom f) <> {} ;

        then

        reconsider D = ( rng h) as non empty set by A4, RELAT_1: 42;

        consider Ch be Function such that

         A15: ( dom Ch) = D and

         A16: for x be set st x in D holds (Ch . x) in x by A8, FUNCT_1: 111;

        

         A17: ( dom (Ch * h)) = ( dom h) by A15, RELAT_1: 27;

        now

          let y be object;

          assume

           A18: y in ( dom ( doms f));

          then ((Ch * h) . y) = (Ch . (h . y)) & (h . y) in ( rng h) by A6, A4, A17, FUNCT_1: 12, FUNCT_1:def 3;

          then ((Ch * h) . y) in (h . y) by A16;

          hence ((Ch * h) . y) in (( doms f) . y) by A6, A4, A18;

        end;

        then

         A19: (Ch * h) in ( product ( doms f)) by A6, A4, A17, CARD_3:def 5;

        then

        consider h1 be Function such that

         A20: (( Frege f) . (Ch * h)) = h1 and

         A21: ( dom h1) = ( dom f) and

         A22: for x st x in ( dom h1) holds (h1 . x) = (( uncurry f) . (x,((Ch * h) . x))) by Def6;

        now

          let z be object;

          assume

           A23: z in ( dom f);

          then

           A24: (h1 . z) = (( uncurry f) . (z,((Ch * h) . z))) by A21, A22;

          ((Ch * h) . z) = (Ch . (h . z)) & (h . z) in ( rng h) by A4, A17, A23, FUNCT_1: 12, FUNCT_1:def 3;

          then

           A25: ((Ch * h) . z) in (h . z) by A16;

          then

          consider f1 such that

           A26: f1 = (f . z) and

           A27: (f1 . ((Ch * h) . z)) = (g . z) by A4, A23;

          

           A28: ((Ch * h) . z) in (( doms f) . z) by A4, A23, A25;

          

           A29: z in ( dom f) by A23;

          then (( doms f) . z) = ( dom f1) by A26, Th18;

          hence (h1 . z) = (g . z) by A29, A24, A26, A27, A28, FUNCT_5: 38;

        end;

        then x = h1 by A1, A2, A7, A21, FUNCT_1: 2;

        hence thesis by A5, A19, A20, FUNCT_1:def 3;

      end;

      now

        assume

         A30: ( dom f) = {} ;

        then

         A31: g = {} by A2, Def2;

        ( dom ( Frege f)) = { {} } by A6, A5, A30, CARD_3: 10, RELAT_1: 41;

        then

         A32: {} in ( dom ( Frege f)) by TARSKI:def 1;

        then

        consider h such that

         A33: (( Frege f) . {} ) = h and

         A34: ( dom h) = ( dom f) and for x st x in ( dom h) holds (h . x) = (( uncurry f) . (x,( {} . x))) by A5, Def6;

        h = {} by A30, A34;

        hence thesis by A1, A31, A32, A33, FUNCT_1:def 3;

      end;

      hence thesis by A14;

    end;

    theorem :: FUNCT_6:38

    

     Th33: for f be Function-yielding Function holds ( rng ( Frege f)) = ( product ( rngs f)) by Lm1, Lm2;

    theorem :: FUNCT_6:39

    

     Th34: for f be Function-yielding Function st not {} in ( rng f) holds (( Frege f) is one-to-one iff for g st g in ( rng f) holds g is one-to-one)

    proof

      let f be Function-yielding Function;

      set h0 = the Element of ( product ( doms f));

      

       A1: ( dom ( doms f)) = ( dom f) by Def1;

      assume

       A2: not {} in ( rng f);

      now

        assume {} in ( rng ( doms f));

        then

        consider x be object such that

         A3: x in ( dom ( doms f)) and

         A4: {} = (( doms f) . x) by FUNCT_1:def 3;

        

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

        reconsider g = (f . x) as Function;

        

         A6: x in ( dom f) by A5;

        then

         A7: g in ( rng f) by FUNCT_1:def 3;

         {} = ( dom g) by A4, A6, Th18;

        hence contradiction by A2, A7, RELAT_1: 41;

      end;

      then ( product ( doms f)) <> {} by CARD_3: 26;

      then

      consider h such that h0 = h and ( dom h) = ( dom ( doms f)) and

       A8: for x be object st x in ( dom ( doms f)) holds (h . x) in (( doms f) . x) by CARD_3:def 5;

      

       A9: ( dom ( Frege f)) = ( product ( doms f)) by Def6;

      thus ( Frege f) is one-to-one implies for g st g in ( rng f) holds g is one-to-one

      proof

        deffunc G( object) = (h . $1);

        assume

         A10: for x,y be object st x in ( dom ( Frege f)) & y in ( dom ( Frege f)) & (( Frege f) . x) = (( Frege f) . y) holds x = y;

        let g;

        assume g in ( rng f);

        then

        consider z be object such that

         A11: z in ( dom f) & g = (f . z) by FUNCT_1:def 3;

        defpred P[ object] means $1 = z;

        let x,y be object;

        deffunc F( object) = x;

        consider h1 be Function such that

         A12: ( dom h1) = ( dom f) & for a be object st a in ( dom f) holds ( P[a] implies (h1 . a) = F(a)) & ( not P[a] implies (h1 . a) = G(a)) from PARTFUN1:sch 1;

        assume that

         A13: x in ( dom g) and

         A14: y in ( dom g) and

         A15: (g . x) = (g . y);

        now

          let a be object;

          assume

           A16: a in ( dom ( doms f));

          then

           A17: a <> z implies (h1 . a) = (h . a) by A1, A12;

          a = z implies (h1 . a) = x by A1, A12, A16;

          hence (h1 . a) in (( doms f) . a) by A8, A11, A13, A16, A17, Th18;

        end;

        then

         A18: h1 in ( product ( doms f)) by A1, A12, CARD_3:def 5;

        then

        consider g1 be Function such that

         A19: (( Frege f) . h1) = g1 and

         A20: ( dom g1) = ( dom f) and

         A21: for x st x in ( dom g1) holds (g1 . x) = (( uncurry f) . (x,(h1 . x))) by Def6;

        defpred P[ object] means $1 = z;

        deffunc G( object) = (h . $1);

        deffunc F( object) = y;

        consider h2 be Function such that

         A22: ( dom h2) = ( dom f) & for a be object st a in ( dom f) holds ( P[a] implies (h2 . a) = F(a)) & ( not P[a] implies (h2 . a) = G(a)) from PARTFUN1:sch 1;

        now

          let a be object;

          assume

           A23: a in ( dom ( doms f));

          then

           A24: a <> z implies (h2 . a) = (h . a) by A1, A22;

          a = z implies (h2 . a) = y by A1, A22, A23;

          hence (h2 . a) in (( doms f) . a) by A8, A11, A14, A23, A24, Th18;

        end;

        then

         A25: h2 in ( product ( doms f)) by A1, A22, CARD_3:def 5;

        then

        consider g2 be Function such that

         A26: (( Frege f) . h2) = g2 and

         A27: ( dom g2) = ( dom f) and

         A28: for x st x in ( dom g2) holds (g2 . x) = (( uncurry f) . (x,(h2 . x))) by Def6;

        now

          let a be object;

          assume

           A29: a in ( dom f);

          then

           A30: (g2 . a) = (( uncurry f) . (a,(h2 . a))) by A27, A28;

          

           A31: (g1 . a) = (( uncurry f) . (a,(h1 . a))) by A20, A21, A29;

          per cases ;

            suppose

             A32: a <> z;

            then (h1 . a) = (h . a) by A12, A29;

            hence (g1 . a) = (g2 . a) by A22, A29, A30, A31, A32;

          end;

            suppose

             A33: a = z;

            then (h1 . a) = x by A12, A29;

            then

             A34: (g1 . a) = (g . x) by A11, A13, A31, A33, FUNCT_5: 38;

            (h2 . a) = y by A22, A29, A33;

            hence (g1 . a) = (g2 . a) by A11, A14, A15, A30, A33, A34, FUNCT_5: 38;

          end;

        end;

        then g1 = g2 by A20, A27;

        then

         A35: h1 = h2 by A9, A10, A18, A19, A25, A26;

        

         A36: z in ( dom f) by A11;

        then (h1 . z) = x by A12;

        hence thesis by A36, A22, A35;

      end;

      assume

       A37: for g st g in ( rng f) holds g is one-to-one;

      let x,y be object;

      assume that

       A38: x in ( dom ( Frege f)) and

       A39: y in ( dom ( Frege f)) and

       A40: (( Frege f) . x) = (( Frege f) . y);

      consider g2 be Function such that

       A41: y = g2 and

       A42: ( dom g2) = ( dom ( doms f)) and

       A43: for x be object st x in ( dom ( doms f)) holds (g2 . x) in (( doms f) . x) by A9, A39, CARD_3:def 5;

      consider g1 be Function such that

       A44: x = g1 and

       A45: ( dom g1) = ( dom ( doms f)) and

       A46: for x be object st x in ( dom ( doms f)) holds (g1 . x) in (( doms f) . x) by A9, A38, CARD_3:def 5;

      consider h2 be Function such that

       A47: (( Frege f) . g2) = h2 and

       A48: ( dom h2) = ( dom f) & for x st x in ( dom h2) holds (h2 . x) = (( uncurry f) . (x,(g2 . x))) by A9, A39, A41, Def6;

      consider h1 be Function such that

       A49: (( Frege f) . g1) = h1 and

       A50: ( dom h1) = ( dom f) & for x st x in ( dom h1) holds (h1 . x) = (( uncurry f) . (x,(g1 . x))) by A9, A38, A44, Def6;

      now

        let a be object;

        assume

         A51: a in ( dom f);

        reconsider g = (f . a) as Function;

        

         A52: a in ( dom f) by A51;

        then

         A53: ( dom g) = (( doms f) . a) by Th18;

        then

         A54: (g2 . a) in ( dom g) by A1, A43, A51;

        

         A55: (g1 . a) in ( dom g) by A1, A46, A51, A53;

        (h2 . a) = (( uncurry f) . (a,(g2 . a))) by A48, A51;

        then

         A56: (h2 . a) = (g . (g2 . a)) by A52, A54, FUNCT_5: 38;

        g in ( rng f) by A52, FUNCT_1:def 3;

        then

         A57: g is one-to-one by A37;

        (h1 . a) = (( uncurry f) . (a,(g1 . a))) by A50, A51;

        then (h1 . a) = (g . (g1 . a)) by A52, A55, FUNCT_5: 38;

        hence (g1 . a) = (g2 . a) by A40, A44, A41, A49, A47, A55, A54, A56, A57;

      end;

      hence thesis by A1, A44, A45, A41, A42, FUNCT_1: 2;

    end;

    begin

    theorem :: FUNCT_6:40

     <: {} :> = {} & ( Frege {} ) = ( {} .--> {} )

    proof

      

       A1: ( dom ( doms {} )) = ( {} " {} ) by Def1, RELAT_1: 38;

      then

       A2: ( product ( doms {} )) = { {} } by CARD_3: 10, RELAT_1: 41;

       A3:

      now

        let x be object;

        assume

         A4: x in { {} };

        then

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

        then ex h st (( Frege {} ) . {} ) = h & ( dom h) = ( dom {} ) & for x st x in ( dom h) holds (h . x) = (( uncurry {} ) . (x,( {} . x))) by A2, A4, Def6;

        hence (( Frege {} ) . x) = {} by A5;

      end;

      

       A6: ( meet {} qua set) = {} by SETFAM_1:def 1;

      ( rng ( doms {} )) = {} by A1, RELAT_1: 38, RELAT_1: 41;

      then ( dom <: {} :>) = {} by A6, Th25;

      hence <: {} :> = {} ;

      ( dom ( Frege {} )) = ( product ( doms {} )) by Def6;

      hence thesis by A2, A3, FUNCOP_1: 11;

    end;

    theorem :: FUNCT_6:41

    X <> {} implies ( dom <:(X --> f):>) = ( dom f) & for x st x in ( dom f) holds ( <:(X --> f):> . x) = (X --> (f . x))

    proof

      assume

       A1: X <> {} ;

      

      thus

       A2: ( dom <:(X --> f):>) = ( meet ( doms (X --> f))) by Th25

      .= ( meet (X --> ( dom f))) by Th20

      .= ( dom f) by A1, Th23;

      

       A3: ( rng <:(X --> f):>) c= ( product ( rngs (X --> f))) & ( rngs (X --> f)) = (X --> ( rng f)) by Th20, Th25;

      let x;

      assume

       A4: x in ( dom f);

      then ( <:(X --> f):> . x) in ( rng <:(X --> f):>) by A2, FUNCT_1:def 3;

      then

      consider g such that

       A5: ( <:(X --> f):> . x) = g and

       A6: ( dom g) = ( dom (X --> ( rng f))) and for y be object st y in ( dom (X --> ( rng f))) holds (g . y) in ((X --> ( rng f)) . y) by A3, CARD_3:def 5;

      

       A7: ( dom g) = X by A6;

      

       A8: ( dom (X --> f)) = X;

       A9:

      now

        let y be object;

        assume

         A10: y in X;

        then (g . y) = (( uncurry (X --> f)) . (y,x)) & ((X --> f) . y) = f by A2, A4, A5, A7, Th26, FUNCOP_1: 7;

        then (g . y) = (f . x) by A4, A8, A10, FUNCT_5: 38;

        hence (g . y) = ((X --> (f . x)) . y) by A10, FUNCOP_1: 7;

      end;

      thus thesis by A5, A7, A9;

    end;

    theorem :: FUNCT_6:42

    ( dom ( Frege (X --> f))) = ( Funcs (X,( dom f))) & ( rng ( Frege (X --> f))) = ( Funcs (X,( rng f))) & for g st g in ( Funcs (X,( dom f))) holds (( Frege (X --> f)) . g) = (f * g)

    proof

      

       A1: ( product (X --> ( dom f))) = ( Funcs (X,( dom f))) by CARD_3: 11;

      

       A2: ( doms (X --> f)) = (X --> ( dom f)) by Th20;

      ( rngs (X --> f)) = (X --> ( rng f)) & ( product (X --> ( rng f))) = ( Funcs (X,( rng f))) by Th20, CARD_3: 11;

      hence ( dom ( Frege (X --> f))) = ( Funcs (X,( dom f))) & ( rng ( Frege (X --> f))) = ( Funcs (X,( rng f))) by A2, A1, Def6, Th33;

      let g;

      assume

       A3: g in ( Funcs (X,( dom f)));

      then

      consider h such that

       A4: (( Frege (X --> f)) . g) = h and

       A5: ( dom h) = ( dom (X --> f)) and

       A6: for x st x in ( dom h) holds (h . x) = (( uncurry (X --> f)) . (x,(g . x))) by A2, A1, Def6;

      

       A7: ( dom h) = X by A5;

      

       A8: ex g9 be Function st g = g9 & ( dom g9) = X & ( rng g9) c= ( dom f) by A3, FUNCT_2:def 2;

      then

       A9: ( dom (f * g)) = X by RELAT_1: 27;

      

       A10: ( dom (X --> f)) = X;

      now

        let x be object;

        assume

         A11: x in X;

        then

         A12: (h . x) = (( uncurry (X --> f)) . (x,(g . x))) & ((X --> f) . x) = f by A6, A7, FUNCOP_1: 7;

        (g . x) in ( rng g) & ((f * g) . x) = (f . (g . x)) by A8, A9, A11, FUNCT_1: 12, FUNCT_1:def 3;

        hence ((f * g) . x) = (h . x) by A8, A10, A11, A12, FUNCT_5: 38;

      end;

      hence thesis by A4, A7, A9, FUNCT_1: 2;

    end;

    theorem :: FUNCT_6:43

    

     Th38: ( dom f) = X & ( dom g) = X & (for x st x in X holds ((f . x),(g . x)) are_equipotent ) implies (( product f),( product g)) are_equipotent

    proof

      assume that

       A1: ( dom f) = X and

       A2: ( dom g) = X and

       A3: for x st x in X holds ((f . x),(g . x)) are_equipotent ;

      defpred P[ object, object] means ex f1 st $2 = f1 & f1 is one-to-one & ( dom f1) = (f . $1) & ( rng f1) = (g . $1);

      

       A4: 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;

        then ((f . x),(g . x)) are_equipotent by A3;

        then ex h st h is one-to-one & ( dom h) = (f . x) & ( rng h) = (g . x);

        hence thesis;

      end;

      consider h such that

       A5: ( dom h) = X & for x be object st x in X holds P[x, (h . x)] from CLASSES1:sch 1( A4);

      h is Function-yielding

      proof

        let x be object;

        assume x in ( dom h);

        then P[x, (h . x)] by A5;

        hence (h . x) is Function;

      end;

      then

      reconsider h as Function-yielding Function;

       A6:

      now

        let x be object;

        assume

         A7: x in X;

        then ex f1 st (h . x) = f1 & f1 is one-to-one & ( dom f1) = (f . x) & ( rng f1) = (g . x) by A5;

        hence (( rngs h) . x) = (g . x) by A5, A7, Th18;

      end;

      

       A8: ( dom h) = X by A5;

      then ( dom ( rngs h)) = X by Def2;

      then

       A9: ( rngs h) = g by A2, A6;

       A10:

      now

        let x be object;

        assume

         A11: x in X;

        then ex f1 st (h . x) = f1 & f1 is one-to-one & ( dom f1) = (f . x) & ( rng f1) = (g . x) by A5;

        hence (( doms h) . x) = (f . x) by A5, A11, Th18;

      end;

      ( dom ( doms h)) = X by A8, Def1;

      then

       A12: ( doms h) = f by A1, A10;

      now

        per cases ;

          suppose {} in ( rng h);

          then

          consider x be object such that

           A13: x in X and

           A14: {} = (h . x) by A5, FUNCT_1:def 3;

          

           A15: ex f1 st {} = f1 & f1 is one-to-one & ( dom f1) = (f . x) & ( rng f1) = (g . x) by A5, A13, A14;

          then {} in ( rng f) by A1, A13, FUNCT_1:def 3;

          then

           A16: ( product f) = {} by CARD_3: 26;

           {} in ( rng g) by A2, A13, A15, FUNCT_1:def 3, RELAT_1: 38;

          hence thesis by A16, CARD_3: 26;

        end;

          suppose

           A17: not {} in ( rng h);

           A18:

          now

            let f1;

            assume f1 in ( rng h);

            then

            consider x be object such that

             A19: x in X and

             A20: f1 = (h . x) by A5, FUNCT_1:def 3;

            ex f1 st (h . x) = f1 & f1 is one-to-one & ( dom f1) = (f . x) & ( rng f1) = (g . x) by A5, A19;

            hence f1 is one-to-one by A20;

          end;

          thus thesis

          proof

            take ( Frege h);

            thus thesis by A12, A9, A17, A18, Def6, Th33, Th34;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_6:44

    

     Th39: ( dom f) = ( dom h) & ( dom g) = ( rng h) & h is one-to-one & (for x st x in ( dom h) holds ((f . x),(g . (h . x))) are_equipotent ) implies (( product f),( product g)) are_equipotent

    proof

      set X = ( dom f);

      assume that

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

       A2: ( dom g) = ( rng h) and

       A3: h is one-to-one and

       A4: for x st x in ( dom h) holds ((f . x),(g . (h . x))) are_equipotent ;

      

       A5: (h * (h " )) = ( id ( dom g)) by A2, A3, FUNCT_1: 39;

      

       A6: ( dom (g * h)) = ( dom f) by A1, A2, RELAT_1: 27;

      now

        let x;

        assume

         A7: x in ( dom f);

        then ((f . x),(g . (h . x))) are_equipotent by A1, A4;

        hence ((f . x),((g * h) . x)) are_equipotent by A6, A7, FUNCT_1: 12;

      end;

      then

       A8: (( product f),( product (g * h))) are_equipotent by A6, Th38;

      defpred P[ object, object] means ex f1 st $1 = f1 & $2 = (f1 * (h " ));

      

       A9: for x be object st x in ( product (g * h)) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in ( product (g * h));

        then ex f1 st x = f1 & ( dom f1) = ( dom (g * h)) & for y be object st y in ( dom (g * h)) holds (f1 . y) in ((g * h) . y) by CARD_3:def 5;

        then

        consider f1 such that

         A10: x = f1;

        (f1 * (h " )) = (f1 * (h " ));

        hence thesis by A10;

      end;

      consider F be Function such that

       A11: ( dom F) = ( product (g * h)) & for x be object st x in ( product (g * h)) holds P[x, (F . x)] from CLASSES1:sch 1( A9);

      

       A12: ( rng (h " )) = X by A1, A3, FUNCT_1: 33;

      

       A13: F is one-to-one

      proof

        let x,y be object;

        assume that

         A14: x in ( dom F) and

         A15: y in ( dom F) and

         A16: (F . x) = (F . y);

        consider g2 be Function such that

         A17: y = g2 and

         A18: (F . y) = (g2 * (h " )) by A11, A15;

        

         A19: ( dom g2) = X by A6, A11, A15, A17, CARD_3: 9;

        consider g1 be Function such that

         A20: x = g1 and

         A21: (F . x) = (g1 * (h " )) by A11, A14;

        ( dom g1) = X by A6, A11, A14, A20, CARD_3: 9;

        hence thesis by A12, A16, A20, A21, A17, A18, A19, FUNCT_1: 86;

      end;

      

       A22: ((g * h) * (h " )) = (g * (h * (h " ))) & (g * ( id ( dom g))) = g by RELAT_1: 36, RELAT_1: 52;

      

       A23: ( product g) c= ( rng F)

      proof

        let x be object;

        assume x in ( product g);

        then

        consider f1 such that

         A24: x = f1 and

         A25: ( dom f1) = ( dom g) and

         A26: for z be object st z in ( dom g) holds (f1 . z) in (g . z) by CARD_3:def 5;

        

         A27: ( dom (f1 * h)) = X by A1, A2, A25, RELAT_1: 27;

        now

          let z be object;

          assume

           A28: z in X;

          then

           A29: (h . z) in ( dom g) by A1, A2, FUNCT_1:def 3;

          

           A30: ((h " ) . (h . z)) = z by A1, A3, A28, FUNCT_1: 34;

          ((f1 * h) . z) = (f1 . (h . z)) by A27, A28, FUNCT_1: 12;

          then ((f1 * h) . z) in (((g * h) * (h " )) . (h . z)) by A5, A22, A26, A29;

          hence ((f1 * h) . z) in ((g * h) . z) by A5, A22, A29, A30, FUNCT_1: 12;

        end;

        then

         A31: (f1 * h) in ( product (g * h)) by A6, A27, CARD_3:def 5;

        then ex f2 st (f1 * h) = f2 & (F . (f1 * h)) = (f2 * (h " )) by A11;

        

        then (F . (f1 * h)) = (f1 * ( id ( dom g))) by A5, RELAT_1: 36

        .= x by A24, A25, RELAT_1: 51;

        hence thesis by A11, A31, FUNCT_1:def 3;

      end;

      

       A32: ( dom (h " )) = ( rng h) by A3, FUNCT_1: 33;

      ( rng F) c= ( product g)

      proof

        let x be object;

        assume x in ( rng F);

        then

        consider y be object such that

         A33: y in ( dom F) and

         A34: x = (F . y) by FUNCT_1:def 3;

        consider f1 such that

         A35: y = f1 and

         A36: ( dom f1) = X and

         A37: for z be object st z in X holds (f1 . z) in ((g * h) . z) by A6, A11, A33, CARD_3:def 5;

        

         A38: ( dom (f1 * (h " ))) = ( dom g) by A2, A12, A32, A36, RELAT_1: 27;

         A39:

        now

          let z be object;

          assume

           A40: z in ( dom g);

          then

           A41: ((h " ) . z) in X by A2, A12, A32, FUNCT_1:def 3;

          (g . z) = ((g * h) . ((h " ) . z)) & ((f1 * (h " )) . z) = (f1 . ((h " ) . z)) by A5, A22, A38, A40, FUNCT_1: 12;

          hence ((f1 * (h " )) . z) in (g . z) by A37, A41;

        end;

        ex f1 st y = f1 & (F . y) = (f1 * (h " )) by A11, A33;

        hence thesis by A34, A35, A38, A39, CARD_3:def 5;

      end;

      then ( rng F) = ( product g) by A23;

      then (( product (g * h)),( product g)) are_equipotent by A11, A13;

      hence thesis by A8, WELLORD2: 15;

    end;

    theorem :: FUNCT_6:45

    ( dom f) = X implies (( product f),( product (f * P))) are_equipotent

    proof

      assume

       A1: ( dom f) = X;

      

       A2: ( rng P) = X by FUNCT_2:def 3;

      ( dom P) = X by FUNCT_2: 52;

      then

       A3: ( dom (f * P)) = X by A1, A2, RELAT_1: 27;

      

       A4: ( rng (P " )) = X by FUNCT_2:def 3;

      

       A5: ( dom (P " )) = X by FUNCT_2: 52;

      now

        let x;

        assume

         A6: x in ( dom (P " ));

        then ((P " ) . x) in X by A4, FUNCT_1:def 3;

        

        then ((f * P) . ((P " ) . x)) = (f . (P . ((P " ) . x))) by A3, FUNCT_1: 12

        .= (f . x) by A5, A2, A6, FUNCT_1: 35;

        hence ((f . x),((f * P) . ((P " ) . x))) are_equipotent ;

      end;

      hence thesis by A1, A5, A4, A3, Th39;

    end;

    begin

    definition

      let f, X;

      :: FUNCT_6:def8

      func Funcs (f,X) -> Function means

      : Def7: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = ( Funcs ((f . x),X));

      existence

      proof

        deffunc F( object) = ( Funcs ((f . $1),X));

        consider F be Function such that

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

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1, f2 such that

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

         A3: for x be object st x in ( dom f) holds (f1 . x) = ( Funcs ((f . x),X)) and

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

         A5: for x be object st x in ( dom f) holds (f2 . x) = ( Funcs ((f . x),X));

        now

          let x be object;

          assume

           A6: x in ( dom f);

          then (f1 . x) = ( Funcs ((f . x),X)) by A3;

          hence (f1 . x) = (f2 . x) by A5, A6;

        end;

        hence thesis by A2, A4;

      end;

    end

    theorem :: FUNCT_6:46

     not {} in ( rng f) implies ( Funcs (f, {} )) = (( dom f) --> {} )

    proof

      assume

       A1: not {} in ( rng f);

       A2:

      now

        let x be object;

        assume x in ( dom f);

        then

         A4: (f . x) <> {} by A1, FUNCT_1:def 3;

        

        thus ((( dom f) --> {} ) . x) = {}

        .= ( Funcs ((f . x), {} )) by A4;

      end;

      ( dom (( dom f) --> {} )) = ( dom f);

      hence thesis by A2, Def7;

    end;

    theorem :: FUNCT_6:47

    ( Funcs ( {} ,X)) = {}

    proof

      ( dom ( Funcs ( {} ,X))) = ( dom {} ) by Def7;

      hence thesis;

    end;

    theorem :: FUNCT_6:48

    ( Funcs ((X --> Y),Z)) = (X --> ( Funcs (Y,Z)))

    proof

      

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

       A2:

      now

        let x be object;

        assume

         A3: x in X;

        then (( Funcs ((X --> Y),Z)) . x) = ( Funcs (((X --> Y) . x),Z)) by A1, Def7;

        hence (( Funcs ((X --> Y),Z)) . x) = ( Funcs (Y,Z)) by A3, FUNCOP_1: 7;

      end;

      ( dom ( Funcs ((X --> Y),Z))) = ( dom (X --> Y)) by Def7;

      hence thesis by A2, FUNCOP_1: 11;

    end;

    

     Lm3: for x,y,z be object holds [x, y] in ( dom f) & g = (( curry f) . x) & z in ( dom g) implies [x, z] in ( dom f)

    proof

      let x,y,z be object;

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

      then x in ( proj1 ( dom f)) by XTUPLE_0:def 12;

      then

       A1: ex g9 be Function st (( curry f) . x) = g9 & ( dom g9) = ( proj2 (( dom f) /\ [: {x}, ( proj2 ( dom f)):])) & for y st y in ( dom g9) holds (g9 . y) = (f . (x,y)) by FUNCT_5:def 1;

      assume g = (( curry f) . x) & z in ( dom g);

      then

      consider y be object such that

       A2: [y, z] in (( dom f) /\ [: {x}, ( proj2 ( dom f)):]) by A1, XTUPLE_0:def 13;

       [y, z] in [: {x}, ( proj2 ( dom f)):] by A2, XBOOLE_0:def 4;

      then

       A3: y in {x} by ZFMISC_1: 87;

       [y, z] in ( dom f) by A2, XBOOLE_0:def 4;

      hence thesis by A3, TARSKI:def 1;

    end;

    theorem :: FUNCT_6:49

    (( Funcs (( Union ( disjoin f)),X)),( product ( Funcs (f,X)))) are_equipotent

    proof

      defpred P[ object, object] means ex g, h st $1 = g & $2 = h & ( dom h) = ( dom f) & for y st y in ( dom f) holds ((f . y) = {} implies (h . y) = {} ) & ((f . y) <> {} implies (h . y) = (( curry' g) . y));

      

       A1: for x be object st x in ( Funcs (( Union ( disjoin f)),X)) holds ex z be object st P[x, z]

      proof

        defpred P[ object] means (f . $1) = {} ;

        deffunc F( object) = {} ;

        let x be object;

        assume x in ( Funcs (( Union ( disjoin f)),X));

        then

        consider g such that

         A2: x = g and ( dom g) = ( Union ( disjoin f)) and ( rng g) c= X by FUNCT_2:def 2;

        deffunc G( object) = (( curry' g) . $1);

        consider h such that

         A3: ( dom h) = ( dom f) & for y be object st y in ( dom f) holds ( P[y] implies (h . y) = F(y)) & ( not P[y] implies (h . y) = G(y)) from PARTFUN1:sch 1;

        take z = h, g, h;

        thus x = g & z = h & ( dom h) = ( dom f) & for y st y in ( dom f) holds ((f . y) = {} implies (h . y) = {} ) & ((f . y) <> {} implies (h . y) = (( curry' g) . y)) by A2, A3;

      end;

      consider F be Function such that

       A4: ( dom F) = ( Funcs (( Union ( disjoin f)),X)) & for x be object st x in ( Funcs (( Union ( disjoin f)),X)) holds P[x, (F . x)] from CLASSES1:sch 1( A1);

      take F;

      thus F is one-to-one

      proof

        let x,y be object;

        assume that

         A5: x in ( dom F) and

         A6: y in ( dom F) and

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

        

         A8: ex f2 be Function st y = f2 & ( dom f2) = ( Union ( disjoin f)) & ( rng f2) c= X by A4, A6, FUNCT_2:def 2;

        consider g1,h1 be Function such that

         A9: x = g1 and

         A10: (F . x) = h1 and ( dom h1) = ( dom f) and

         A11: for y st y in ( dom f) holds ((f . y) = {} implies (h1 . y) = {} ) & ((f . y) <> {} implies (h1 . y) = (( curry' g1) . y)) by A4, A5;

        consider g2,h2 be Function such that

         A12: y = g2 and

         A13: (F . y) = h2 and ( dom h2) = ( dom f) and

         A14: for y st y in ( dom f) holds ((f . y) = {} implies (h2 . y) = {} ) & ((f . y) <> {} implies (h2 . y) = (( curry' g2) . y)) by A4, A6;

        

         A15: ex f1 be Function st x = f1 & ( dom f1) = ( Union ( disjoin f)) & ( rng f1) c= X by A4, A5, FUNCT_2:def 2;

        now

          let z be object;

          assume

           A16: z in ( Union ( disjoin f));

          then

           A17: z = [(z `1 ), (z `2 )] by CARD_3: 22;

          

           A18: (z `2 ) in ( dom f) & (z `1 ) in (f . (z `2 )) by A16, CARD_3: 22;

          then

           A19: (h2 . (z `2 )) = (( curry' g2) . (z `2 )) by A14;

          then

          reconsider g91 = (h1 . (z `2 )), g92 = (h2 . (z `2 )) as Function by A7, A10, A13;

          

           A20: (g2 . ((z `1 ),(z `2 ))) = (g92 . (z `1 )) by A8, A12, A16, A17, A19, FUNCT_5: 22;

          (h1 . (z `2 )) = (( curry' g1) . (z `2 )) by A11, A18;

          then (g1 . ((z `1 ),(z `2 ))) = (g91 . (z `1 )) by A15, A9, A16, A17, FUNCT_5: 22;

          hence (g1 . z) = (g2 . z) by A7, A10, A13, A17, A20;

        end;

        hence thesis by A15, A8, A9, A12, FUNCT_1: 2;

      end;

      thus ( dom F) = ( Funcs (( Union ( disjoin f)),X)) by A4;

      thus ( rng F) c= ( product ( Funcs (f,X)))

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A21: x in ( dom F) and

         A22: y = (F . x) by FUNCT_1:def 3;

        consider g, h such that

         A23: x = g and

         A24: (F . x) = h and

         A25: ( dom h) = ( dom f) and

         A26: for y st y in ( dom f) holds ((f . y) = {} implies (h . y) = {} ) & ((f . y) <> {} implies (h . y) = (( curry' g) . y)) by A4, A21;

        

         A27: ex f1 be Function st x = f1 & ( dom f1) = ( Union ( disjoin f)) & ( rng f1) c= X by A4, A21, FUNCT_2:def 2;

         A28:

        now

          let z be object;

          assume z in ( dom ( Funcs (f,X)));

          then

           A29: z in ( dom f) by Def7;

          then

           A30: (( Funcs (f,X)) . z) = ( Funcs ((f . z),X)) by Def7;

           A31:

          now

            set a = the Element of (f . z);

            assume

             A32: (f . z) <> {} ;

            ( [a, z] `1 ) = a & ( [a, z] `2 ) = z;

            then

             A33: [a, z] in ( Union ( disjoin f)) by A29, A32, CARD_3: 22;

            reconsider k = (( curry' g) . z) as Function;

            

             A34: z in ( dom ( curry' g)) by A23, A27, A33, FUNCT_5: 21;

            then ( rng k) c= ( rng g) by FUNCT_5: 34;

            then

             A35: ( rng k) c= X by A23, A27;

            

             A36: ( dom k) = ( proj1 (( dom g) /\ [:( proj1 ( dom g)), {z}:])) by A34, FUNCT_5: 34;

            

             A37: ( dom k) = (f . z)

            proof

              thus ( dom k) c= (f . z)

              proof

                let b be object;

                assume b in ( dom k);

                then

                consider c be object such that

                 A38: [b, c] in (( dom g) /\ [:( proj1 ( dom g)), {z}:]) by A36, XTUPLE_0:def 12;

                 [b, c] in [:( proj1 ( dom g)), {z}:] by A38, XBOOLE_0:def 4;

                then

                 A39: c in {z} by ZFMISC_1: 87;

                

                 A40: ( [b, c] `1 ) = b & ( [b, c] `2 ) = c;

                 [b, c] in ( dom g) by A38, XBOOLE_0:def 4;

                then b in (f . c) by A23, A27, A40, CARD_3: 22;

                hence thesis by A39, TARSKI:def 1;

              end;

              let b be object such that

               A41: b in (f . z);

              

               A42: z in {z} by TARSKI:def 1;

              ( [b, z] `1 ) = b & ( [b, z] `2 ) = z;

              then

               A43: [b, z] in ( dom g) by A23, A27, A29, A41, CARD_3: 22;

              then b in ( proj1 ( dom g)) by XTUPLE_0:def 12;

              then [b, z] in [:( proj1 ( dom g)), {z}:] by A42, ZFMISC_1: 87;

              then [b, z] in (( dom g) /\ [:( proj1 ( dom g)), {z}:]) by A43, XBOOLE_0:def 4;

              hence thesis by A36, XTUPLE_0:def 12;

            end;

            (h . z) = k by A26, A29, A32;

            hence (h . z) in (( Funcs (f,X)) . z) by A30, A35, A37, FUNCT_2:def 2;

          end;

          now

            assume (f . z) = {} ;

            then (h . z) = {} & (( Funcs (f,X)) . z) = { {} } by A26, A29, A30, FUNCT_5: 57;

            hence (h . z) in (( Funcs (f,X)) . z) by TARSKI:def 1;

          end;

          hence (h . z) in (( Funcs (f,X)) . z) by A31;

        end;

        ( dom h) = ( dom ( Funcs (f,X))) by A25, Def7;

        hence thesis by A22, A24, A28, CARD_3:def 5;

      end;

      let x be object;

      assume x in ( product ( Funcs (f,X)));

      then

      consider s be Function such that

       A44: x = s and

       A45: ( dom s) = ( dom ( Funcs (f,X))) and

       A46: for z be object st z in ( dom ( Funcs (f,X))) holds (s . z) in (( Funcs (f,X)) . z) by CARD_3:def 5;

      

       A47: ( dom s) = ( dom f) by A45, Def7;

      

       A48: ( uncurry' s) = ( ~ ( uncurry s)) by FUNCT_5:def 4;

      

       A49: ( dom ( uncurry' s)) = ( Union ( disjoin f))

      proof

        thus ( dom ( uncurry' s)) c= ( Union ( disjoin f))

        proof

          let z be object;

          assume

           A50: z in ( dom ( uncurry' s));

          then

          consider z1,z2 be object such that

           A51: z = [z1, z2] by A48, Th2;

          

           A52: (z `1 ) = z1 & (z `2 ) = z2 by A51;

           [z2, z1] in ( dom ( uncurry s)) by A48, A50, A51, FUNCT_4: 42;

          then

          consider a be object, u be Function, b be object such that

           A53: [z2, z1] = [a, b] and

           A54: a in ( dom s) and

           A55: u = (s . a) and

           A56: b in ( dom u) by FUNCT_5:def 2;

          

           A57: ( [a, b] `1 ) = a & ( [z2, z1] `1 ) = z2;

          u in (( Funcs (f,X)) . a) & (( Funcs (f,X)) . a) = ( Funcs ((f . a),X)) by A45, A46, A47, A54, A55, Def7;

          then

           A58: ex j be Function st u = j & ( dom j) = (f . z2) & ( rng j) c= X by A53, A57, FUNCT_2:def 2;

          ( [a, b] `2 ) = b & ( [z2, z1] `2 ) = z1;

          hence thesis by A47, A51, A53, A54, A56, A52, A57, A58, CARD_3: 22;

        end;

        let z be object;

        assume

         A59: z in ( Union ( disjoin f));

        then

         A60: (z `1 ) in (f . (z `2 )) & z = [(z `1 ), (z `2 )] by CARD_3: 22;

        

         A61: (z `2 ) in ( dom f) by A59, CARD_3: 22;

        then (s . (z `2 )) in (( Funcs (f,X)) . (z `2 )) & (( Funcs (f,X)) . (z `2 )) = ( Funcs ((f . (z `2 )),X)) by A45, A46, A47, Def7;

        then ex j be Function st (s . (z `2 )) = j & ( dom j) = (f . (z `2 )) & ( rng j) c= X by FUNCT_2:def 2;

        hence thesis by A47, A61, A60, FUNCT_5: 39;

      end;

      ( rng ( uncurry' s)) c= X

      proof

        let d be object;

        assume d in ( rng ( uncurry' s));

        then

        consider z be object such that

         A62: z in ( dom ( uncurry' s)) and

         A63: d = (( uncurry' s) . z) by FUNCT_1:def 3;

        consider z1,z2 be object such that

         A64: z = [z1, z2] by A48, A62, Th2;

         [z2, z1] in ( dom ( uncurry s)) by A48, A62, A64, FUNCT_4: 42;

        then

        consider a be object, u be Function, b be object such that

         A65: [z2, z1] = [a, b] and

         A66: a in ( dom s) & u = (s . a) and

         A67: b in ( dom u) by FUNCT_5:def 2;

        

         A68: ( [a, b] `1 ) = a & ( [z2, z1] `1 ) = z2;

        u in (( Funcs (f,X)) . a) & (( Funcs (f,X)) . a) = ( Funcs ((f . a),X)) by A45, A46, A47, A66, Def7;

        then

         A69: ex j be Function st u = j & ( dom j) = (f . z2) & ( rng j) c= X by A65, A68, FUNCT_2:def 2;

        

         A70: ( [a, b] `2 ) = b & ( [z2, z1] `2 ) = z1;

        (( uncurry' s) . (b,a)) = (u . b) by A66, A67, FUNCT_5: 39;

        then d in ( rng u) by A63, A64, A65, A67, A68, A70, FUNCT_1:def 3;

        hence thesis by A69;

      end;

      then

       A71: ( uncurry' s) in ( dom F) by A4, A49, FUNCT_2:def 2;

      then

      consider g, h such that

       A72: ( uncurry' s) = g and

       A73: (F . ( uncurry' s)) = h and

       A74: ( dom h) = ( dom f) and

       A75: for y st y in ( dom f) holds ((f . y) = {} implies (h . y) = {} ) & ((f . y) <> {} implies (h . y) = (( curry' g) . y)) by A4;

      now

        let z be object;

        assume

         A76: z in ( dom f);

        then (s . z) in (( Funcs (f,X)) . z) & (( Funcs (f,X)) . z) = ( Funcs ((f . z),X)) by A45, A46, A47, Def7;

        then

        consider v be Function such that

         A77: (s . z) = v and

         A78: ( dom v) = (f . z) and ( rng v) c= X by FUNCT_2:def 2;

         A79:

        now

          set a = the Element of (f . z);

          assume

           A80: (f . z) <> {} ;

          then

           A81: [a, z] in ( dom ( uncurry' s)) by A47, A76, A77, A78, FUNCT_5: 39;

          reconsider j = (( curry' ( uncurry' s)) . z) as Function;

          

           A82: j = (( curry ( ~ ( uncurry' s))) . z) by FUNCT_5:def 3;

          

           A83: ( ~ ( uncurry' s)) = ( uncurry s) by Th4;

          then

           A84: [z, a] in ( dom ( uncurry s)) by A81, FUNCT_4: 42;

          

           A85: ( dom j) = ( dom v)

          proof

            thus ( dom j) c= ( dom v)

            proof

              let b be object;

              assume b in ( dom j);

              then [z, b] in ( dom ( uncurry s)) by A82, A83, A84, Lm3;

              then

              consider a1 be object, g1 be Function, a2 be object such that

               A86: [z, b] = [a1, a2] and a1 in ( dom s) and

               A87: g1 = (s . a1) & a2 in ( dom g1) by FUNCT_5:def 2;

              z = a1 by A86, XTUPLE_0: 1;

              hence thesis by A77, A86, A87, XTUPLE_0: 1;

            end;

            let b be object;

            assume b in ( dom v);

            then [z, b] in ( dom ( uncurry s)) by A47, A76, A77, FUNCT_5: 38;

            hence thesis by A82, A83, FUNCT_5: 20;

          end;

          now

            let b be object;

            assume b in (f . z);

            then

             A88: [z, b] in ( dom ( uncurry s)) by A78, A82, A83, A84, A85, Lm3;

            then

            consider a1 be object, g1 be Function, a2 be object such that

             A89: [z, b] = [a1, a2] and

             A90: a1 in ( dom s) & g1 = (s . a1) & a2 in ( dom g1) by FUNCT_5:def 2;

            

             A91: (j . b) = (( uncurry s) . (z,b)) by A82, A83, A88, FUNCT_5: 20;

            z = a1 & b = a2 by A89, XTUPLE_0: 1;

            hence (j . b) = (v . b) by A77, A90, A91, FUNCT_5: 38;

          end;

          then v = j by A78, A85;

          hence (s . z) = (h . z) by A72, A75, A76, A77, A80;

        end;

        (f . z) = {} implies (s . z) = {} & (h . z) = {} by A75, A76, A77, A78;

        hence (s . z) = (h . z) by A79;

      end;

      then h = s by A47, A74;

      hence thesis by A44, A71, A73, FUNCT_1:def 3;

    end;

    definition

      let X, f;

      :: FUNCT_6:def9

      func Funcs (X,f) -> Function means

      : Def8: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = ( Funcs (X,(f . x)));

      existence

      proof

        deffunc F( object) = ( Funcs (X,(f . $1)));

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

        hence thesis;

      end;

      uniqueness

      proof

        let f1, f2 such that

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

         A2: for x be object st x in ( dom f) holds (f1 . x) = ( Funcs (X,(f . x))) and

         A3: ( dom f2) = ( dom f) and

         A4: for x be object st x in ( dom f) holds (f2 . x) = ( Funcs (X,(f . x)));

        now

          let x be object;

          assume

           A5: x in ( dom f);

          then (f1 . x) = ( Funcs (X,(f . x))) by A2;

          hence (f1 . x) = (f2 . x) by A4, A5;

        end;

        hence thesis by A1, A3;

      end;

    end

    

     Lm4: f <> {} & X <> {} implies (( product ( Funcs (X,f))),( Funcs (X,( product f)))) are_equipotent

    proof

      defpred P[ object, object] means ex g be Function-yielding Function st $1 = g & $2 = <:g:>;

      assume that

       A1: f <> {} and

       A2: X <> {} ;

      

       A3: for x be object st x in ( product ( Funcs (X,f))) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in ( product ( Funcs (X,f)));

        then

        consider g such that

         A4: x = g & ( dom g) = ( dom ( Funcs (X,f))) & for x be object st x in ( dom ( Funcs (X,f))) holds (g . x) in (( Funcs (X,f)) . x) by CARD_3:def 5;

        g is Function-yielding

        proof

          let x be object;

          assume

           A5: x in ( dom g);

          then

           A6: (g . x) in (( Funcs (X,f)) . x) by A4;

          x in ( dom f) by A5, A4, Def8;

          then (g . x) in ( Funcs (X,(f . x))) by A6, Def8;

          hence (g . x) is Function;

        end;

        then

        reconsider g = x as Function-yielding Function by A4;

        reconsider y = <:g:> as set;

        take y, g;

        thus thesis;

      end;

      consider F be Function such that

       A7: ( dom F) = ( product ( Funcs (X,f))) & for x be object st x in ( product ( Funcs (X,f))) holds P[x, (F . x)] from CLASSES1:sch 1( A3);

      take F;

      

       A8: for g be Function-yielding Function st g in ( product ( Funcs (X,f))) holds ( dom <:g:>) = X & ( rng g) = ( rng g) & ( rng <:g:>) c= ( product f)

      proof

        let g be Function-yielding Function;

        

         A9: ( dom ( Funcs (X,f))) = ( dom f) by Def8;

        assume

         A10: g in ( product ( Funcs (X,f)));

        then

         A11: ( dom g) = ( dom ( Funcs (X,f))) by CARD_3: 9;

         A12:

        now

          let z be object;

          assume

           A13: z in ( dom f);

          then (g . z) in (( Funcs (X,f)) . z) & (( Funcs (X,f)) . z) = ( Funcs (X,(f . z))) by A10, A9, Def8, CARD_3: 9;

          then ex h st (g . z) = h & ( dom h) = X & ( rng h) c= (f . z) by FUNCT_2:def 2;

          hence ((( dom f) --> X) . z) = ( proj1 (g . z)) by A13, FUNCOP_1: 7;

        end;

        ( dom (( dom f) --> X)) = ( dom f);

        then ( doms g) = (( dom f) --> X) by A11, A9, A12, Def1;

        then ( meet ( doms g)) = X by A1, Th23;

        hence

         A14: ( dom <:g:>) = X & ( rng g) = ( rng g) by Th25;

        let y be object;

        assume y in ( rng <:g:>);

        then

        consider x be object such that

         A15: x in ( dom <:g:>) and

         A16: y = ( <:g:> . x) by FUNCT_1:def 3;

        reconsider h = y as Function by A16;

        

         A17: ( dom h) = ( dom f) by A11, A9, A15, A16, Th26;

        now

          let z be object;

          assume

           A18: z in ( dom f);

          then

           A19: (( uncurry g) . (z,x)) = (h . z) by A15, A16, A17, Th26;

          (g . z) in (( Funcs (X,f)) . z) & (( Funcs (X,f)) . z) = ( Funcs (X,(f . z))) by A10, A9, A18, Def8, CARD_3: 9;

          then

          consider j be Function such that

           A20: (g . z) = j and

           A21: ( dom j) = X and

           A22: ( rng j) c= (f . z) by FUNCT_2:def 2;

          

           A23: (j . x) in ( rng j) by A14, A15, A21, FUNCT_1:def 3;

          (( uncurry g) . (z,x)) = (j . x) by A11, A9, A14, A15, A18, A20, A21, FUNCT_5: 38;

          hence (h . z) in (f . z) by A22, A19, A23;

        end;

        hence thesis by A17, CARD_3:def 5;

      end;

      thus F is one-to-one

      proof

        let x,y be object;

        assume that

         A24: x in ( dom F) and

         A25: y in ( dom F) and

         A26: (F . x) = (F . y) and

         A27: x <> y;

        consider gy be Function-yielding Function such that

         A28: y = gy and

         A29: (F . y) = <:gy:> by A7, A25;

        consider gx be Function-yielding Function such that

         A30: x = gx and

         A31: (F . x) = <:gx:> by A7, A24;

        

         A32: ( dom gx) = ( dom ( Funcs (X,f))) by A7, A24, A30, CARD_3: 9;

        

         A33: ( dom ( Funcs (X,f))) = ( dom f) by Def8;

        

         A34: ( dom gy) = ( dom ( Funcs (X,f))) by A7, A25, A28, CARD_3: 9;

        now

          let z be object;

          assume

           A35: z in ( dom f);

          then

           A36: (( Funcs (X,f)) . z) = ( Funcs (X,(f . z))) by Def8;

          (gy . z) in (( Funcs (X,f)) . z) by A7, A25, A28, A33, A35, CARD_3: 9;

          then

          consider hy be Function such that

           A37: (gy . z) = hy & ( dom hy) = X and ( rng hy) c= (f . z) by A36, FUNCT_2:def 2;

          (gx . z) in (( Funcs (X,f)) . z) by A7, A24, A30, A33, A35, CARD_3: 9;

          then

          consider hx be Function such that

           A38: (gx . z) = hx & ( dom hx) = X and ( rng hx) c= (f . z) by A36, FUNCT_2:def 2;

          

           A39: ( dom <:gx:>) = X by A7, A8, A24, A30;

          now

            let b be object;

            assume

             A40: b in X;

            reconsider fx = ( <:gx:> . b) as Function;

            

             A41: (( uncurry gx) . (z,b)) = (hx . b) & (( uncurry gy) . (z,b)) = (hy . b) by A32, A34, A33, A35, A38, A37, A40, FUNCT_5: 38;

            

             A42: ( dom fx) = ( dom gx) by A39, A40, Th26;

            then (fx . z) = (( uncurry gx) . (z,b)) by A32, A33, A35, A39, A40, Th26;

            hence (hx . b) = (hy . b) by A26, A31, A29, A32, A33, A35, A39, A40, A42, A41, Th26;

          end;

          hence (gx . z) = (gy . z) by A38, A37;

        end;

        hence thesis by A27, A30, A28, A32, A34, A33, FUNCT_1: 2;

      end;

      thus ( dom F) = ( product ( Funcs (X,f))) by A7;

      thus ( rng F) c= ( Funcs (X,( product f)))

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A43: x in ( dom F) and

         A44: y = (F . x) by FUNCT_1:def 3;

        consider g be Function-yielding Function such that

         A45: x = g and

         A46: y = <:g:> by A7, A43, A44;

        ( dom <:g:>) = X & ( rng <:g:>) c= ( product f) by A7, A8, A43, A45;

        hence thesis by A46, FUNCT_2:def 2;

      end;

      let y be object;

      assume y in ( Funcs (X,( product f)));

      then

      consider h be Function such that

       A47: y = h and

       A48: ( dom h) = X and

       A49: ( rng h) c= ( product f) by FUNCT_2:def 2;

      h is Function-yielding

      proof

        let x be object;

        assume x in ( dom h);

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

        then (h . x) is Element of ( product f) by A49;

        hence thesis;

      end;

      then

      reconsider h as Function-yielding Function;

      set g = <:h:>;

       A50:

      now

        let z be object;

        assume

         A51: z in X;

        then (h . z) in ( rng h) by A48, FUNCT_1:def 3;

        then

         A52: ex j be Function st (h . z) = j & ( dom j) = ( dom f) & for x be object st x in ( dom f) holds (j . x) in (f . x) by A49, CARD_3:def 5;

        

        thus ((X --> ( dom f)) . z) = ( dom f) by A51, FUNCOP_1: 7

        .= (( doms h) . z) by A48, A51, A52, Th18;

      end;

      

       A53: ( meet ( doms h)) = ( dom g) by Th25;

      ( dom ( doms h)) = ( dom h) & ( dom (( dom h) --> ( dom f))) = ( dom h) by Def1;

      then (X --> ( dom f)) = ( doms h) by A48, A50;

      then

       A54: ( dom g) = ( dom f) by A2, A53, Th23;

       A55:

      now

        let z be object;

        assume

         A56: z in ( dom f);

        reconsider i = (g . z) as Function;

        

         A57: ( dom i) = X by A48, A54, A56, Th26;

        ( rng i) c= (f . z)

        proof

          let x be object;

          assume x in ( rng i);

          then

          consider a be object such that

           A58: a in ( dom i) and

           A59: x = (i . a) by FUNCT_1:def 3;

          (h . a) in ( rng h) by A48, A57, A58, FUNCT_1:def 3;

          then

          consider j be Function such that

           A60: (h . a) = j & ( dom j) = ( dom f) and

           A61: for x be object st x in ( dom f) holds (j . x) in (f . x) by A49, CARD_3:def 5;

          (i . a) = (( uncurry h) . (a,z)) by A54, A56, A58, Th26

          .= (j . z) by A48, A56, A57, A58, A60, FUNCT_5: 38;

          hence thesis by A56, A59, A61;

        end;

        then (g . z) in ( Funcs (X,(f . z))) by A57, FUNCT_2:def 2;

        hence (g . z) in (( Funcs (X,f)) . z) by A56, Def8;

      end;

      

       A62: ( meet ( doms g)) = ( dom <:g:>) by Th25;

      ( product f) c= ( Funcs (( dom f),( Union f))) by Th1;

      then

       A63: ( rng h) c= ( Funcs (( dom f),( Union f))) by A49;

      then

       A64: ( dom ( uncurry h)) = [:( dom h), ( dom f):] by FUNCT_5: 26;

      ( dom f) = ( dom ( Funcs (X,f))) by Def8;

      then

       A65: g in ( product ( Funcs (X,f))) by A54, A55, CARD_3:def 5;

      then

       A66: ex g9 be Function-yielding Function st g = g9 & (F . g) = <:g9:> by A7;

      ( dom ( uncurry' h)) = [:( dom f), ( dom h):] by A63, FUNCT_5: 26;

      then

       A67: (( uncurry' h) | [:( meet ( doms h)), ( dom h):] qua set) = ( uncurry' h) by A53, A54;

      

       A68: ( uncurry' h) = ( ~ ( uncurry h)) & ( curry ( ~ ( uncurry h))) = ( curry' ( uncurry h)) by FUNCT_5:def 3, FUNCT_5:def 4;

      ( dom <:g:>) = X by A8, A65;

      then

       A69: (( uncurry h) | [:( meet ( doms g)), ( dom g):] qua set) = ( uncurry h) by A48, A54, A64, A62;

      ( uncurry' ( curry' ( uncurry h))) = ( uncurry h) by A64, FUNCT_5: 49;

      then <:g:> = h by A1, A63, A67, A69, A68, FUNCT_5: 48;

      hence thesis by A7, A47, A65, A66, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_6:50

    

     Th45: ( Funcs ( {} ,f)) = (( dom f) --> { {} })

    proof

       A1:

      now

        let x be object;

        assume x in ( dom f);

        

        hence (( Funcs ( {} ,f)) . x) = ( Funcs ( {} qua set,(f . x))) by Def8

        .= { {} } by FUNCT_5: 57;

      end;

      ( dom ( Funcs ( {} ,f))) = ( dom f) by Def8;

      hence thesis by A1, FUNCOP_1: 11;

    end;

    theorem :: FUNCT_6:51

    

     Th46: ( Funcs (X, {} )) = {}

    proof

      ( dom ( Funcs (X, {} ))) = ( dom {} ) by Def8;

      hence thesis;

    end;

    theorem :: FUNCT_6:52

    ( Funcs (X,(Y --> Z))) = (Y --> ( Funcs (X,Z)))

    proof

      

       A1: Y = ( dom (Y --> Z));

       A2:

      now

        let x be object;

        assume

         A3: x in Y;

        then (( Funcs (X,(Y --> Z))) . x) = ( Funcs (X,((Y --> Z) . x))) by A1, Def8;

        hence (( Funcs (X,(Y --> Z))) . x) = ( Funcs (X,Z)) by A3, FUNCOP_1: 7;

      end;

      ( dom ( Funcs (X,(Y --> Z)))) = ( dom (Y --> Z)) by Def8;

      hence thesis by A2, FUNCOP_1: 11;

    end;

    theorem :: FUNCT_6:53

    (( product ( Funcs (X,f))),( Funcs (X,( product f)))) are_equipotent

    proof

      

       A1: ( Funcs (X,( product {} ))) = {(X --> {} )} by CARD_3: 10, FUNCT_5: 59;

      

       A2: ( product ( Funcs ( {} ,f))) = ( product (( dom f) --> { {} })) by Th45

      .= ( Funcs (( dom f), { {} })) by CARD_3: 11

      .= {(( dom f) --> {} )} by FUNCT_5: 59;

      

       A3: ( Funcs ( {} qua set,( product f))) = { {} } & ( product ( Funcs (X, {} ))) = { {} } by Th46, CARD_3: 10, FUNCT_5: 57;

      X <> {} & f <> {} implies thesis by Lm4;

      hence thesis by A2, A3, A1, CARD_1: 28;

    end;

    begin

    definition

      let f be Function;

      :: FUNCT_6:def10

      func commute f -> Function-yielding Function equals ( curry' ( uncurry f));

      coherence ;

    end

    theorem :: FUNCT_6:54

    for f be Function, x be set st x in ( dom ( commute f)) holds (( commute f) . x) is Function;

    theorem :: FUNCT_6:55

    

     Th50: for A,B,C be set, f be Function st A <> {} & B <> {} & f in ( Funcs (A,( Funcs (B,C)))) holds ( commute f) in ( Funcs (B,( Funcs (A,C))))

    proof

      let A,B,C be set, f be Function;

      assume A <> {} & B <> {} & f in ( Funcs (A,( Funcs (B,C))));

      then [:A, B:] <> {} & ( uncurry f) in ( Funcs ( [:A, B:],C)) by Th11, ZFMISC_1: 90;

      hence thesis by Th10;

    end;

    theorem :: FUNCT_6:56

    for A,B,C be set, f be Function st A <> {} & B <> {} & f in ( Funcs (A,( Funcs (B,C)))) holds for g,h be Function, x,y be set st x in A & y in B & (f . x) = g & (( commute f) . y) = h holds (h . x) = (g . y) & ( dom h) = A & ( dom g) = B & ( rng h) c= C & ( rng g) c= C

    proof

      let A,B,C be set, f be Function;

      assume that

       A1: A <> {} & B <> {} and

       A2: f in ( Funcs (A,( Funcs (B,C))));

      set uf = ( uncurry f);

      set cf = ( commute f);

      let g,h be Function, x,y be set;

      assume that

       A3: x in A and

       A4: y in B and

       A5: (f . x) = g and

       A6: (( commute f) . y) = h;

      ( commute f) in ( Funcs (B,( Funcs (A,C)))) by A1, A2, Th50;

      then

       A7: ex g be Function st g = cf & ( dom g) = B & ( rng g) c= ( Funcs (A,C)) by FUNCT_2:def 2;

      then (cf . y) in ( rng cf) by A4, FUNCT_1:def 3;

      then

       A8: ex t be Function st t = h & ( dom t) = A & ( rng t) c= C by A6, A7, FUNCT_2:def 2;

      

       A9: ex g be Function st g = f & ( dom g) = A & ( rng g) c= ( Funcs (B,C)) by A2, FUNCT_2:def 2;

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

      then

       A10: ex t be Function st t = g & ( dom t) = B & ( rng t) c= C by A5, A9, FUNCT_2:def 2;

      then [x, y] in ( dom uf) & (uf . (x,y)) = (g . y) by A3, A4, A5, A9, FUNCT_5: 38;

      hence thesis by A6, A10, A8, FUNCT_5: 22;

    end;

    theorem :: FUNCT_6:57

    for A,B,C be set, f be Function st A <> {} & B <> {} & f in ( Funcs (A,( Funcs (B,C)))) holds ( commute ( commute f)) = f

    proof

      let A,B,C be set, f be Function;

      assume that

       A1: A <> {} & B <> {} and

       A2: f in ( Funcs (A,( Funcs (B,C))));

      

       A3: ex g be Function st g = f & ( dom g) = A & ( rng g) c= ( Funcs (B,C)) by A2, FUNCT_2:def 2;

      set cf = ( commute f);

      

       A4: ( commute f) in ( Funcs (B,( Funcs (A,C)))) by A1, A2, Th50;

      then ( commute cf) in ( Funcs (A,( Funcs (B,C)))) by A1, Th50;

      then

       A5: ex h be Function st h = ( commute cf) & ( dom h) = A & ( rng h) c= ( Funcs (B,C)) by FUNCT_2:def 2;

      

       A6: ex g be Function st g = cf & ( dom g) = B & ( rng g) c= ( Funcs (A,C)) by A4, FUNCT_2:def 2;

      for x be object st x in A holds (f . x) = (( commute cf) . x)

      proof

        set ccf = ( commute cf), uf = ( uncurry f), ucf = ( uncurry cf);

        let x be object;

        assume

         A7: x in A;

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

        then

        consider g be Function such that

         A8: g = (f . x) & ( dom g) = B and ( rng g) c= C by A3, FUNCT_2:def 2;

        (ccf . x) in ( rng ccf) by A5, A7, FUNCT_1:def 3;

        then

        consider h be Function such that

         A9: h = (ccf . x) and

         A10: ( dom h) = B and ( rng h) c= C by A5, FUNCT_2:def 2;

        

         A11: for y st y in B holds for h be Function st h = (cf . y) holds x in ( dom h) & (h . x) = (g . y)

        proof

          let y;

          assume y in B;

          then

           A12: [x, y] in ( dom uf) & (uf . (x,y)) = (g . y) by A3, A7, A8, FUNCT_5: 38;

          let h be Function;

          assume h = (cf . y);

          hence thesis by A12, FUNCT_5: 22;

        end;

        

         A13: for y st y in B holds [y, x] in ( dom ucf) & (ucf . (y,x)) = (g . y)

        proof

          let y;

          reconsider h = (cf . y) as Function;

          assume

           A14: y in B;

          then x in ( dom h) & (h . x) = (g . y) by A11;

          hence thesis by A6, A14, FUNCT_5: 38;

        end;

        for y be object st y in B holds (h . y) = (g . y)

        proof

          let y be object;

          assume y in B;

          then [y, x] in ( dom ucf) & (ucf . (y,x)) = (g . y) by A13;

          hence thesis by A9, FUNCT_5: 22;

        end;

        hence thesis by A8, A9, A10, FUNCT_1: 2;

      end;

      hence thesis by A3, A5;

    end;

    theorem :: FUNCT_6:58

    ( commute {} ) = {} by FUNCT_5: 42, FUNCT_5: 43;

    theorem :: FUNCT_6:59

    for f be Function-yielding Function holds ( dom ( doms f)) = ( dom f) by Def1;

    theorem :: FUNCT_6:60

    for f be Function-yielding Function holds ( dom ( rngs f)) = ( dom f) by Def2;