funct_2.miz



    begin

    reserve P,Q,X,Y,Z for set,

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

    definition

      let X, Y;

      let R be Relation of X, Y;

      :: FUNCT_2:def1

      attr R is quasi_total means

      : Def1: X = ( dom R) if Y <> {}

      otherwise R = {} ;

      consistency ;

    end

    registration

      let X, Y;

      cluster quasi_total for PartFunc of X, Y;

      existence

      proof

        per cases ;

          suppose

           A1: Y = {} ;

          reconsider R = {} as PartFunc of X, Y by RELSET_1: 12;

          take R;

          thus thesis by A1, Def1;

        end;

          suppose

           A2: Y <> {} ;

          then

          consider f be Function such that

           A3: X = ( dom f) and

           A4: ( rng f) c= Y by FUNCT_1: 8;

          reconsider R = f as PartFunc of X, Y by A3, A4, RELSET_1: 4;

          take R;

          thus thesis by A2, A3, Def1;

        end;

      end;

    end

    registration

      let X, Y;

      cluster total -> quasi_total for Relation of X, Y;

      coherence

      proof

        let f be Relation of X, Y;

        assume

         A1: ( dom f) = X;

        per cases ;

          case Y <> {} ;

          thus thesis by A1;

        end;

          case Y = {} ;

          hence thesis;

        end;

      end;

    end

    definition

      let X, Y;

      mode Function of X,Y is quasi_total PartFunc of X, Y;

    end

    registration

      let X be empty set, Y be set;

      cluster quasi_total -> total for Relation of X, Y;

      coherence ;

    end

    registration

      let X be set, Y be non empty set;

      cluster quasi_total -> total for Relation of X, Y;

      coherence by Def1;

    end

    registration

      let X be set;

      cluster quasi_total -> total for Relation of X, X;

      coherence

      proof

        per cases ;

          suppose X = {} ;

          hence thesis;

        end;

          suppose X <> {} ;

          hence thesis;

        end;

      end;

    end

    registration

      let X be set;

      cluster quasi_total -> total for Relation of [:X, X:], X;

      coherence

      proof

        per cases ;

          suppose X = {} ;

          hence thesis;

        end;

          suppose X <> {} ;

          hence thesis;

        end;

      end;

    end

    theorem :: FUNCT_2:1

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

    proof

      let f be Function;

      reconsider R = f as Relation of ( dom f), ( rng f) by RELSET_1: 4;

      ( rng R) <> {} or ( rng R) = {} ;

      hence thesis by Def1;

    end;

    theorem :: FUNCT_2:2

    

     Th2: for f be Function st ( rng f) c= Y holds f is Function of ( dom f), Y

    proof

      let f be Function;

      assume ( rng f) c= Y;

      then

      reconsider R = f as Relation of ( dom f), Y by RELSET_1: 4;

      Y = {} or Y <> {} ;

      then R is quasi_total by Def1;

      hence thesis;

    end;

    theorem :: FUNCT_2:3

    for f be Function st ( dom f) = X & for x st x in X holds (f . x) in Y holds f is Function of X, Y

    proof

      let f be Function such that

       A1: ( dom f) = X and

       A2: for x st x in X holds (f . x) in Y;

      ( rng f) c= Y

      proof

        let y be object;

        assume y in ( rng f);

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

        hence thesis by A2;

      end;

      then

      reconsider R = f as Relation of ( dom f), Y by RELSET_1: 4;

      Y = {} or Y <> {} ;

      then R is quasi_total by Def1;

      hence thesis by A1;

    end;

    theorem :: FUNCT_2:4

    

     Th4: for f be Function of X, Y st Y <> {} & x in X holds (f . x) in ( rng f)

    proof

      let f be Function of X, Y;

      assume Y <> {} ;

      then ( dom f) = X by Def1;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: FUNCT_2:5

    

     Th5: for f be Function of X, Y st Y <> {} & x in X holds (f . x) in Y

    proof

      let f be Function of X, Y;

      assume Y <> {} & x in X;

      then (f . x) in ( rng f) by Th4;

      hence thesis;

    end;

    theorem :: FUNCT_2:6

    for f be Function of X, Y st (Y = {} implies X = {} ) & ( rng f) c= Z holds f is Function of X, Z

    proof

      let f be Function of X, Y;

      assume Y <> {} or X = {} ;

      then

       A1: ( dom f) = X by Def1;

      assume

       A2: ( rng f) c= Z;

      now

        assume Z = {} ;

        then ( rng f) = {} by A2;

        hence X = {} by A1, RELAT_1: 42;

      end;

      hence thesis by A1, A2, Def1, RELSET_1: 4;

    end;

    theorem :: FUNCT_2:7

    for f be Function of X, Y st (Y = {} implies X = {} ) & Y c= Z holds f is Function of X, Z by RELSET_1: 7;

    scheme :: FUNCT_2:sch1

    FuncEx1 { X,Y() -> set , P[ object, object] } :

ex f be Function of X(), Y() st for x be object st x in X() holds P[x, (f . x)]

      provided

       A1: for x be object st x in X() holds ex y be object st y in Y() & P[x, y];

      consider f be Function such that

       A2: ( dom f) = X() & ( rng f) c= Y() and

       A3: for x be object st x in X() holds P[x, (f . x)] from FUNCT_1:sch 6( A1);

      reconsider f as Function of X(), Y() by A2, Th2;

      take f;

      thus thesis by A3;

    end;

    scheme :: FUNCT_2:sch2

    Lambda1 { X,Y() -> set , F( object) -> object } :

ex f be Function of X(), Y() st for x be object st x in X() holds (f . x) = F(x)

      provided

       A1: for x be object st x in X() holds F(x) in Y();

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

      

       A2: for x be object st x in X() holds ex y be object st y in Y() & P[x, y] by A1;

      thus ex f be Function of X(), Y() st for x be object st x in X() holds P[x, (f . x)] from FuncEx1( A2);

    end;

    definition

      let X, Y;

      :: FUNCT_2:def2

      func Funcs (X,Y) -> set means

      : Def2: x in it iff ex f be Function st x = f & ( dom f) = X & ( rng f) c= Y;

      existence

      proof

        defpred P[ object] means ex f be Function st $1 = f & ( dom f) = X & ( rng f) c= Y;

        consider F be set such that

         A1: for z be object holds z in F iff z in ( bool [:X, Y:]) & P[z] from XBOOLE_0:sch 1;

        take F;

        let z;

        thus z in F implies ex f be Function st z = f & ( dom f) = X & ( rng f) c= Y by A1;

        given f be Function such that

         A2: z = f and

         A3: ( dom f) = X & ( rng f) c= Y;

        f c= [:X, Y:]

        proof

          let p be object;

          assume

           A4: p in f;

          then

          consider x,y be object such that

           A5: p = [x, y] by RELAT_1:def 1;

          reconsider y as set by TARSKI: 1;

          

           A6: x in ( dom f) by A4, A5, XTUPLE_0:def 12;

          then y = (f . x) by A4, A5, FUNCT_1:def 2;

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

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

        end;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let F1,F2 be set such that

         A7: x in F1 iff ex f be Function st x = f & ( dom f) = X & ( rng f) c= Y and

         A8: x in F2 iff ex f be Function st x = f & ( dom f) = X & ( rng f) c= Y;

        for x be object holds x in F1 iff x in F2

        proof

          let x be object;

          x in F1 iff ex f be Function st x = f & ( dom f) = X & ( rng f) c= Y by A7;

          hence thesis by A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: FUNCT_2:8

    

     Th8: for f be Function of X, Y st Y = {} implies X = {} holds f in ( Funcs (X,Y))

    proof

      let f be Function of X, Y;

      assume Y = {} implies X = {} ;

      then

       A1: ( dom f) = X by Def1;

      ( rng f) c= Y;

      hence thesis by A1, Def2;

    end;

    theorem :: FUNCT_2:9

    for f be Function of X, X holds f in ( Funcs (X,X)) by Th8;

    registration

      let X be set, Y be non empty set;

      cluster ( Funcs (X,Y)) -> non empty;

      coherence by Th8;

    end

    registration

      let X be set;

      cluster ( Funcs (X,X)) -> non empty;

      coherence by Th8;

    end

    registration

      let X be non empty set, Y be empty set;

      cluster ( Funcs (X,Y)) -> empty;

      coherence

      proof

        assume ( Funcs (X,Y)) is non empty;

        then

        consider f be Function such that the Element of ( Funcs (X,Y)) = f and

         A1: ( dom f) = X and

         A2: ( rng f) c= {} by Def2;

        ( rng f) = {} by A2;

        hence contradiction by A1, RELAT_1: 42;

      end;

    end

    theorem :: FUNCT_2:10

    for f be Function of X, Y st for y be object st y in Y holds ex x be object st x in X & y = (f . x) holds ( rng f) = Y

    proof

      let f be Function of X, Y such that

       A1: for y be object st y in Y holds ex x be object st x in X & y = (f . x);

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        for y be object holds y in ( rng f) iff y in Y

        proof

          let y be object;

          ( dom f) = X by A2, Def1;

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

          hence thesis by A1;

        end;

        hence thesis by TARSKI: 2;

      end;

    end;

    theorem :: FUNCT_2:11

    

     Th11: for f be Function of X, Y st y in ( rng f) holds ex x be object st x in X & (f . x) = y

    proof

      let f be Function of X, Y;

      assume

       A1: y in ( rng f);

      then ( dom f) = X by Def1;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    theorem :: FUNCT_2:12

    

     Th12: for f1,f2 be Function of X, Y st for x be object st x in X holds (f1 . x) = (f2 . x) holds f1 = f2

    proof

      let f1,f2 be Function of X, Y;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose Y <> {} ;

        then ( dom f1) = X & ( dom f2) = X by Def1;

        hence thesis;

      end;

    end;

    theorem :: FUNCT_2:13

    

     Th13: for f be quasi_total Relation of X, Y holds for g be quasi_total Relation of Y, Z st Y = {} implies Z = {} or X = {} holds (f * g) is quasi_total

    proof

      let f be quasi_total Relation of X, Y;

      let g be quasi_total Relation of Y, Z such that

       A1: Y = {} implies Z = {} or X = {} ;

      per cases ;

        case

         A2: Z <> {} ;

        then

         A3: ( dom g) = Y by Def1;

        ( dom f) = X & ( rng f) c= Y by A1, A2, Def1;

        hence thesis by A3, RELAT_1: 27;

      end;

        case Z = {} ;

        hence thesis;

      end;

    end;

    theorem :: FUNCT_2:14

    for f be Function of X, Y holds for g be Function of Y, Z st Z <> {} & ( rng f) = Y & ( rng g) = Z holds ( rng (g * f)) = Z

    proof

      let f be Function of X, Y;

      let g be Function of Y, Z;

      assume Z <> {} ;

      then ( dom g) = Y by Def1;

      hence thesis by RELAT_1: 28;

    end;

    theorem :: FUNCT_2:15

    

     Th15: for x be object holds for f be Function of X, Y, g be Function st Y <> {} & x in X holds ((g * f) . x) = (g . (f . x))

    proof

      let x be object;

      let f be Function of X, Y, g be Function;

      assume Y <> {} ;

      then X = ( dom f) by Def1;

      hence thesis by FUNCT_1: 13;

    end;

    theorem :: FUNCT_2:16

    for f be Function of X, Y st Y <> {} holds ( rng f) = Y iff for Z st Z <> {} holds for g,h be Function of Y, Z st (g * f) = (h * f) holds g = h

    proof

      let f be Function of X, Y;

      assume

       A1: Y <> {} ;

      thus ( rng f) = Y implies for Z st Z <> {} holds for g,h be Function of Y, Z st (g * f) = (h * f) holds g = h

      proof

        assume

         A2: ( rng f) = Y;

        let Z such that

         A3: Z <> {} ;

        let g,h be Function of Y, Z;

        ( dom g) = Y & ( dom h) = Y by A3, Def1;

        hence thesis by A2, FUNCT_1: 86;

      end;

      assume

       A4: for Z st Z <> {} holds for g,h be Function of Y, Z st (g * f) = (h * f) holds g = h;

      for g,h be Function st ( dom g) = Y & ( dom h) = Y & (g * f) = (h * f) holds g = h

      proof

        let g,h be Function;

        assume that

         A5: ( dom g) = Y and

         A6: ( dom h) = Y;

        

         A7: ( rng g) <> {} by A1, A5, RELAT_1: 42;

        

         A8: g is Function of Y, (( rng g) \/ ( rng h)) by A5, Th2, XBOOLE_1: 7;

        h is Function of Y, (( rng g) \/ ( rng h)) by A6, Th2, XBOOLE_1: 7;

        hence thesis by A4, A7, A8;

      end;

      hence thesis by FUNCT_1: 16;

    end;

    theorem :: FUNCT_2:17

    for f be Relation of X, Y holds (( id X) * f) = f & (f * ( id Y)) = f

    proof

      let f be Relation of X, Y;

      ( dom f) c= X;

      hence (( id X) * f) = f by RELAT_1: 51;

      ( rng f) c= Y;

      hence thesis by RELAT_1: 53;

    end;

    theorem :: FUNCT_2:18

    for f be Function of X, Y holds for g be Function of Y, X st (f * g) = ( id Y) holds ( rng f) = Y

    proof

      let f be Function of X, Y, g be Function of Y, X;

      assume (f * g) = ( id Y);

      then ( rng (f * g)) = Y;

      then Y c= ( rng f) by RELAT_1: 26;

      hence thesis;

    end;

    theorem :: FUNCT_2:19

    for f be Function of X, Y st Y = {} implies X = {} holds f is one-to-one iff for x1,x2 be object st x1 in X & x2 in X & (f . x1) = (f . x2) holds x1 = x2

    proof

      let f be Function of X, Y;

      assume Y = {} implies X = {} ;

      then ( dom f) = X by Def1;

      hence thesis;

    end;

    theorem :: FUNCT_2:20

    for f be Function of X, Y holds for g be Function of Y, Z st (Z = {} implies Y = {} ) & (g * f) is one-to-one holds f is one-to-one

    proof

      let f be Function of X, Y;

      let g be Function of Y, Z;

      assume Z <> {} or Y = {} ;

      then

       A1: Y = ( dom g) by Def1;

      ( rng f) c= Y;

      hence thesis by A1, FUNCT_1: 25;

    end;

    theorem :: FUNCT_2:21

    for f be Function of X, Y st X <> {} & Y <> {} holds f is one-to-one iff for Z holds for g,h be Function of Z, X st (f * g) = (f * h) holds g = h

    proof

      let f be Function of X, Y;

      assume that

       A1: X <> {} and

       A2: Y <> {} ;

      

       A3: ( dom f) = X by A2, Def1;

      thus f is one-to-one implies for Z holds for g,h be Function of Z, X st (f * g) = (f * h) holds g = h

      proof

        assume

         A4: f is one-to-one;

        let Z;

        let g,h be Function of Z, X;

        

         A5: ( rng g) c= X & ( rng h) c= X;

        ( dom g) = Z & ( dom h) = Z by A1, Def1;

        hence thesis by A3, A4, A5, FUNCT_1: 27;

      end;

      assume

       A6: for Z holds for g,h be Function of Z, X st (f * g) = (f * h) holds g = h;

      now

        let g,h be Function;

        assume ( rng g) c= ( dom f) & ( rng h) c= ( dom f) & ( dom g) = ( dom h);

        then g is Function of ( dom g), X & h is Function of ( dom g), X by A3, Th2;

        hence (f * g) = (f * h) implies g = h by A6;

      end;

      hence thesis by FUNCT_1: 27;

    end;

    theorem :: FUNCT_2:22

    for f be Function of X, Y holds for g be Function of Y, Z st Z <> {} & ( rng (g * f)) = Z & g is one-to-one holds ( rng f) = Y

    proof

      let f be Function of X, Y;

      let g be Function of Y, Z;

      assume that

       A1: Z <> {} and

       A2: ( rng (g * f)) = Z and

       A3: g is one-to-one;

      

       A4: ( dom g) = Y by A1, Def1;

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

      then ( rng g) = ( rng (g * f)) by A2;

      then Y c= ( rng f) by A3, A4, FUNCT_1: 29;

      hence thesis;

    end;

    definition

      let Y be set;

      let f be Y -valued Relation;

      :: FUNCT_2:def3

      attr f is onto means

      : Def3: ( rng f) = Y;

    end

    theorem :: FUNCT_2:23

    for f be Function of X, Y holds for g be Function of Y, X st (g * f) = ( id X) holds f is one-to-one & g is onto

    proof

      let f be Function of X, Y;

      let g be Function of Y, X;

      assume that

       A1: (g * f) = ( id X);

      thus f is one-to-one

      proof

        per cases ;

          suppose Y = {} ;

          hence thesis;

        end;

          suppose Y <> {} ;

          then ( dom f) = X by Def1;

          hence thesis by A1, FUNCT_1: 31;

        end;

      end;

      ( rng (g * f)) = X by A1;

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

      hence ( rng g) = X;

    end;

    theorem :: FUNCT_2:24

    for f be Function of X, Y holds for g be Function of Y, Z st (Z = {} implies Y = {} ) & (g * f) is one-to-one & ( rng f) = Y holds f is one-to-one & g is one-to-one

    proof

      let f be Function of X, Y;

      let g be Function of Y, Z;

      assume Z <> {} or Y = {} ;

      then Y = ( dom g) by Def1;

      hence thesis by FUNCT_1: 26;

    end;

    theorem :: FUNCT_2:25

    

     Th25: for f be Function of X, Y st f is one-to-one & ( rng f) = Y holds (f " ) is Function of Y, X

    proof

      let f be Function of X, Y;

      assume that

       A1: f is one-to-one and

       A2: ( rng f) = Y;

      

       A3: ( rng (f " )) c= X

      proof

        let x be object;

        assume x in ( rng (f " ));

        then x in ( dom f) by A1, FUNCT_1: 33;

        hence thesis;

      end;

      ( dom (f " )) = Y by A1, A2, FUNCT_1: 33;

      then

      reconsider R = (f " ) as Relation of Y, X by A3, RELSET_1: 4;

      R is quasi_total

      proof

        per cases ;

          case X <> {} ;

          thus thesis by A1, A2, FUNCT_1: 33;

        end;

          case X = {} ;

          then ( rng f) = {} ;

          then ( dom (f " )) = {} by A1, FUNCT_1: 32;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_2:26

    for f be Function of X, Y st Y <> {} & f is one-to-one & x in X holds ((f " ) . (f . x)) = x

    proof

      let f be Function of X, Y;

      assume Y <> {} ;

      then ( dom f) = X by Def1;

      hence thesis by FUNCT_1: 34;

    end;

    theorem :: FUNCT_2:27

    for X be set, Y,Z be non empty set holds for f be Function of X, Y holds for g be Function of Y, Z holds f is onto & g is onto implies (g * f) is onto

    proof

      let X be set, Y,Z be non empty set;

      let f be Function of X, Y;

      let g be Function of Y, Z;

      assume that

       A1: f is onto and

       A2: g is onto;

      ( rng f) = Y by A1

      .= ( dom g) by Def1;

      

      then ( rng (g * f)) = ( rng g) by RELAT_1: 28

      .= Z by A2;

      hence thesis;

    end;

    theorem :: FUNCT_2:28

    for f be Function of X, Y holds for g be Function of Y, X st X <> {} & Y <> {} & ( rng f) = Y & f is one-to-one & for y,x be object holds y in Y & (g . y) = x iff x in X & (f . x) = y holds g = (f " )

    proof

      let f be Function of X, Y;

      let g be Function of Y, X;

      assume X <> {} & Y <> {} ;

      then ( dom f) = X & ( dom g) = Y by Def1;

      hence thesis by FUNCT_1: 32;

    end;

    theorem :: FUNCT_2:29

    for f be Function of X, Y st Y <> {} & ( rng f) = Y & f is one-to-one holds ((f " ) * f) = ( id X) & (f * (f " )) = ( id Y)

    proof

      let f be Function of X, Y;

      assume Y <> {} ;

      then ( dom f) = X by Def1;

      hence thesis by FUNCT_1: 39;

    end;

    theorem :: FUNCT_2:30

    for f be Function of X, Y holds for g be Function of Y, X st X <> {} & Y <> {} & ( rng f) = Y & (g * f) = ( id X) & f is one-to-one holds g = (f " )

    proof

      let f be Function of X, Y;

      let g be Function of Y, X;

      assume X <> {} & Y <> {} ;

      then ( dom f) = X & ( dom g) = Y by Def1;

      hence thesis by FUNCT_1: 41;

    end;

    theorem :: FUNCT_2:31

    for f be Function of X, Y st Y <> {} & ex g be Function of Y, X st (g * f) = ( id X) holds f is one-to-one

    proof

      let f be Function of X, Y;

      assume Y <> {} ;

      then

       A1: ( dom f) = X by Def1;

      given g be Function of Y, X such that

       A2: (g * f) = ( id X);

      thus thesis by A2, A1, FUNCT_1: 31;

    end;

    theorem :: FUNCT_2:32

    

     Th32: for f be Function of X, Y st (Y = {} implies X = {} ) & Z c= X holds (f | Z) is Function of Z, Y

    proof

      let f be Function of X, Y such that

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

       A2: Z c= X;

      ( dom f) = X by A1, Def1;

      then

       A3: Z = ( dom (f | Z)) by A2, RELAT_1: 62;

      ( rng (f | Z)) c= Y;

      then

      reconsider R = (f | Z) as Relation of Z, Y by A3, RELSET_1: 4;

      R is quasi_total

      proof

        per cases ;

          case Y <> {} ;

          ( dom f) = X by A1, Def1;

          hence thesis by A2, RELAT_1: 62;

        end;

          case Y = {} ;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_2:33

    for f be Function of X, Y st X c= Z holds (f | Z) = f by RELSET_1: 19;

    theorem :: FUNCT_2:34

    for f be Function of X, Y st Y <> {} & x in X & (f . x) in Z holds ((Z |` f) . x) = (f . x)

    proof

      let f be Function of X, Y;

      assume that

       A1: Y <> {} & x in X and

       A2: (f . x) in Z;

      x in ( dom f) by A1, Def1;

      then x in ( dom (Z |` f)) by A2, FUNCT_1: 54;

      hence thesis by FUNCT_1: 55;

    end;

    theorem :: FUNCT_2:35

    for f be Function of X, Y st Y <> {} holds for y holds (ex x st x in X & x in P & y = (f . x)) implies y in (f .: P)

    proof

      let f be Function of X, Y;

      assume Y <> {} ;

      then

       A1: ( dom f) = X by Def1;

      let y;

      given x such that

       A2: x in X & x in P & y = (f . x);

      thus thesis by A1, A2, FUNCT_1:def 6;

    end;

    theorem :: FUNCT_2:36

    for f be Function of X, Y holds (f .: P) c= Y;

    ::$Canceled

    theorem :: FUNCT_2:38

    for f be Function of X, Y st Y <> {} holds for x holds x in (f " Q) iff x in X & (f . x) in Q

    proof

      let f be Function of X, Y;

      assume Y <> {} ;

      then ( dom f) = X by Def1;

      hence thesis by FUNCT_1:def 7;

    end;

    theorem :: FUNCT_2:39

    for f be PartFunc of X, Y holds (f " Q) c= X;

    theorem :: FUNCT_2:40

    

     Th39: for f be Function of X, Y st Y = {} implies X = {} holds (f " Y) = X

    proof

      let f be Function of X, Y;

      (( rng f) /\ Y) = ( rng f) by XBOOLE_1: 28;

      then

       A1: (f " Y) = (f " ( rng f)) by RELAT_1: 133;

      assume Y <> {} or X = {} ;

      then ( dom f) = X by Def1;

      hence thesis by A1, RELAT_1: 134;

    end;

    theorem :: FUNCT_2:41

    for f be Function of X, Y holds (for y be object st y in Y holds (f " {y}) <> {} ) iff ( rng f) = Y by FUNCT_1: 73, FUNCT_1: 72;

    theorem :: FUNCT_2:42

    

     Th41: for f be Function of X, Y st (Y = {} implies X = {} ) & P c= X holds P c= (f " (f .: P))

    proof

      let f be Function of X, Y;

      assume Y <> {} or X = {} ;

      then ( dom f) = X by Def1;

      hence thesis by FUNCT_1: 76;

    end;

    theorem :: FUNCT_2:43

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

    proof

      let f be Function of X, Y;

      assume Y <> {} or X = {} ;

      then

       A1: ( dom f) = X by Def1;

      then (f " ( rng f)) = X by RELAT_1: 134;

      hence thesis by A1, RELAT_1: 113;

    end;

    theorem :: FUNCT_2:44

    for f be Function of X, Y holds for g be Function of Y, Z st (Z = {} implies Y = {} ) holds (f " Q) c= ((g * f) " (g .: Q))

    proof

      let f be Function of X, Y;

      let g be Function of Y, Z;

      assume Z <> {} or Y = {} ;

      then

       A1: ( dom g) = Y by Def1;

      ( rng f) c= Y;

      hence thesis by A1, FUNCT_1: 90;

    end;

    theorem :: FUNCT_2:45

    for f be Function of {} , Y holds (f .: P) = {} ;

    theorem :: FUNCT_2:46

    for f be Function of {} , Y holds (f " Q) = {} ;

    theorem :: FUNCT_2:47

    for x be object holds for f be Function of {x}, Y st Y <> {} holds (f . x) in Y

    proof

      let x be object;

      let f be Function of {x}, Y;

      assume Y <> {} ;

      then

       A1: ( dom f) = {x} by Def1;

      ( rng f) c= Y;

      then {(f . x)} c= Y by A1, FUNCT_1: 4;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: FUNCT_2:48

    

     Th47: for x be object holds for f be Function of {x}, Y st Y <> {} holds ( rng f) = {(f . x)}

    proof

      let x be object;

      let f be Function of {x}, Y;

      assume Y <> {} ;

      then ( dom f) = {x} by Def1;

      hence thesis by FUNCT_1: 4;

    end;

    theorem :: FUNCT_2:49

    for x be object holds for f be Function of {x}, Y st Y <> {} holds (f .: P) c= {(f . x)}

    proof

      let x be object;

      let f be Function of {x}, Y;

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

      hence thesis by Th47;

    end;

    theorem :: FUNCT_2:50

    

     Th49: for y be object holds for f be Function of X, {y} st x in X holds (f . x) = y

    proof

      let y be object;

      let f be Function of X, {y};

      x in X implies (f . x) in {y} by Th5;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FUNCT_2:51

    

     Th50: for y be object holds for f1,f2 be Function of X, {y} holds f1 = f2

    proof

      let y be object;

      let f1,f2 be Function of X, {y};

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

      proof

        let x be object;

        assume

         A1: x in X;

        then (f1 . x) = y by Th49;

        hence thesis by A1, Th49;

      end;

      hence thesis by Th12;

    end;

    theorem :: FUNCT_2:52

    

     Th51: for f be Function of X, X holds ( dom f) = X

    proof

      X = {} implies X = {} ;

      hence thesis by Def1;

    end;

    registration

      let X,Y be set;

      let f be quasi_total PartFunc of X, Y;

      let g be quasi_total PartFunc of X, X;

      cluster (f * g) -> quasi_total;

      coherence

      proof

        per cases ;

          suppose Y = {} ;

          hence thesis;

        end;

          suppose

           A1: Y <> {} ;

          then ( dom f) = X by Def1;

          

          then ( dom (f * g)) = (g " X) by RELAT_1: 147

          .= ( dom g) by RELSET_1: 22

          .= X by Th51;

          hence thesis by A1, Def1;

        end;

      end;

    end

    registration

      let X,Y be set;

      let f be quasi_total PartFunc of Y, Y;

      let g be quasi_total PartFunc of X, Y;

      cluster (f * g) -> quasi_total;

      coherence

      proof

        per cases ;

          suppose Y = {} ;

          hence thesis;

        end;

          suppose

           A1: Y <> {} ;

          ( dom f) = Y by Th51;

          

          then ( dom (f * g)) = (g " Y) by RELAT_1: 147

          .= ( dom g) by RELSET_1: 22

          .= X by A1, Def1;

          hence thesis by A1, Def1;

        end;

      end;

    end

    theorem :: FUNCT_2:53

    

     Th52: for f,g be Relation of X, X st ( rng f) = X & ( rng g) = X holds ( rng (g * f)) = X

    proof

      let f,g be Relation of X, X;

      assume that

       A1: ( rng f) = X and

       A2: ( rng g) = X;

      

      thus ( rng (g * f)) = (f .: X) by A2, RELAT_1: 127

      .= X by A1, RELSET_1: 22;

    end;

    theorem :: FUNCT_2:54

    for f,g be Function of X, X st (g * f) = f & ( rng f) = X holds g = ( id X)

    proof

      let f,g be Function of X, X;

      ( dom g) = X by Th51;

      hence thesis by FUNCT_1: 23;

    end;

    theorem :: FUNCT_2:55

    for f,g be Function of X, X st (f * g) = f & f is one-to-one holds g = ( id X)

    proof

      let f,g be Function of X, X;

      

       A1: ( rng g) c= X;

      ( dom f) = X & ( dom g) = X by Th51;

      hence thesis by A1, FUNCT_1: 28;

    end;

    theorem :: FUNCT_2:56

    

     Th55: for f be Function of X, X holds f is one-to-one iff for x1,x2 be object st x1 in X & x2 in X & (f . x1) = (f . x2) holds x1 = x2

    proof

      let f be Function of X, X;

      ( dom f) = X by Th51;

      hence thesis;

    end;

    definition

      let X, Y;

      let f be X -definedY -valued Function;

      :: FUNCT_2:def4

      attr f is bijective means f is one-to-one onto;

    end

    registration

      let X,Y be set;

      cluster bijective -> one-to-one onto for PartFunc of X, Y;

      coherence ;

      cluster one-to-one onto -> bijective for PartFunc of X, Y;

      coherence ;

    end

    registration

      let X;

      cluster bijective for Function of X, X;

      existence

      proof

        take ( id X);

        thus ( id X) is one-to-one & ( rng ( id X)) = X;

      end;

    end

    definition

      let X;

      mode Permutation of X is bijective Function of X, X;

    end

    theorem :: FUNCT_2:57

    

     Th56: for f be Function of X, X st f is one-to-one & ( rng f) = X holds f is Permutation of X

    proof

      let f be Function of X, X;

      assume that

       A1: f is one-to-one and

       A2: ( rng f) = X;

      f is onto by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_2:58

    for f be Function of X, X st f is one-to-one holds for x1, x2 st x1 in X & x2 in X & (f . x1) = (f . x2) holds x1 = x2 by Th55;

    registration

      let X;

      let f,g be onto PartFunc of X, X;

      cluster (f * g) -> onto;

      coherence

      proof

        ( rng f) = X & ( rng g) = X by Def3;

        then ( rng (f * g)) = X by Th52;

        hence thesis;

      end;

    end

    registration

      let X;

      let f,g be bijective Function of X, X;

      cluster (g * f) -> bijective;

      coherence ;

    end

    registration

      let X;

      cluster reflexive total -> bijective for Function of X, X;

      coherence

      proof

        let f be Function of X, X;

        assume

         A1: f is reflexive total;

        

         A2: ( field f) = (( dom f) \/ ( rng f)) by RELAT_1:def 6;

        thus f is one-to-one

        proof

          let x1,x2 be object such that

           A3: x1 in ( dom f) and

           A4: x2 in ( dom f) and

           A5: (f . x1) = (f . x2);

          x1 in ( field f) by A2, A3, XBOOLE_0:def 3;

          then [x1, x1] in f by A1, RELAT_2:def 1, RELAT_2:def 9;

          then

           A6: x1 = (f . x1) by A3, FUNCT_1:def 2;

          x2 in ( field f) by A2, A4, XBOOLE_0:def 3;

          then [x2, x2] in f by A1, RELAT_2:def 1, RELAT_2:def 9;

          hence thesis by A4, A5, A6, FUNCT_1:def 2;

        end;

        thus ( rng f) c= X;

        let x be object;

        assume x in X;

        then x in ( dom f) by PARTFUN1:def 2;

        then x in ( field f) by A2, XBOOLE_0:def 3;

        then [x, x] in f by A1, RELAT_2:def 1, RELAT_2:def 9;

        hence thesis by XTUPLE_0:def 13;

      end;

    end

    definition

      let X;

      let f be Permutation of X;

      :: original: "

      redefine

      func f " -> Permutation of X ;

      coherence

      proof

        ( dom f) = X by Th51;

        then

         A1: ( rng (f " )) = X by FUNCT_1: 33;

        ( rng f) = X by Def3;

        then (f " ) is Function of X, X by Th25;

        hence thesis by A1, Th56;

      end;

    end

    theorem :: FUNCT_2:59

    for f,g be Permutation of X st (g * f) = g holds f = ( id X)

    proof

      let f,g be Permutation of X;

      

       A1: ( rng f) c= X;

      ( dom f) = X & ( dom g) = X by Th51;

      hence thesis by A1, FUNCT_1: 28;

    end;

    theorem :: FUNCT_2:60

    for f,g be Permutation of X st (g * f) = ( id X) holds g = (f " )

    proof

      let f,g be Permutation of X;

      

       A1: ( dom f) = X by Th51;

      ( rng f) = X & ( dom g) = X by Def3, Th51;

      hence thesis by A1, FUNCT_1: 41;

    end;

    theorem :: FUNCT_2:61

    for f be Permutation of X holds ((f " ) * f) = ( id X) & (f * (f " )) = ( id X)

    proof

      let f be Permutation of X;

      ( dom f) = X & ( rng f) = X by Def3, Th51;

      hence thesis by FUNCT_1: 39;

    end;

    theorem :: FUNCT_2:62

    

     Th61: for f be Permutation of X st P c= X holds (f .: (f " P)) = P & (f " (f .: P)) = P

    proof

      let f be Permutation of X such that

       A1: P c= X;

      ( dom f) = X by Th51;

      then

       A2: P c= (f " (f .: P)) by A1, FUNCT_1: 76;

      (f " (f .: P)) c= P & ( rng f) = X by Def3, FUNCT_1: 82;

      hence thesis by A1, A2, FUNCT_1: 77;

    end;

    reserve D for non empty set;

    registration

      let X, D, Z;

      let f be Function of X, D;

      let g be Function of D, Z;

      cluster (g * f) -> quasi_total;

      coherence by Th13;

    end

    definition

      let C be non empty set, D be set;

      let f be Function of C, D;

      let c be Element of C;

      :: original: .

      redefine

      func f . c -> Element of D ;

      coherence

      proof

        D is non empty or D is empty;

        hence thesis by Th5, SUBSET_1:def 1;

      end;

    end

    scheme :: FUNCT_2:sch3

    FuncExD { C,D() -> non empty set , P[ object, object] } :

ex f be Function of C(), D() st for x be Element of C() holds P[x, (f . x)]

      provided

       A1: for x be Element of C() holds ex y be Element of D() st P[x, y];

      defpred R[ object, object] means $1 in C() & $2 in D() & P[$1, $2];

      

       A2: for x be object st x in C() holds ex y be object st y in D() & R[x, y]

      proof

        let x be object;

        assume

         A3: x in C();

        then ex y be Element of D() st P[x, y] by A1;

        hence thesis by A3;

      end;

      consider f be Function of C(), D() such that

       A4: for x be object st x in C() holds R[x, (f . x)] from FuncEx1( A2);

      take f;

      let x be Element of C();

      thus thesis by A4;

    end;

    scheme :: FUNCT_2:sch4

    LambdaD { C,D() -> non empty set , F( Element of C()) -> Element of D() } :

ex f be Function of C(), D() st for x be Element of C() holds (f . x) = F(x);

      defpred P[ Element of C(), set] means $2 = F($1);

      

       A1: for x be Element of C() holds ex y be Element of D() st P[x, y];

      thus ex f be Function of C(), D() st for x be Element of C() holds P[x, (f . x)] from FuncExD( A1);

    end;

    theorem :: FUNCT_2:63

    

     Th62: for f1,f2 be Function of X, Y st for x be Element of X holds (f1 . x) = (f2 . x) holds f1 = f2

    proof

      let f1,f2 be Function of X, Y;

      assume for x be Element of X holds (f1 . x) = (f2 . x);

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

      hence thesis by Th12;

    end;

    theorem :: FUNCT_2:64

    

     Th63: for P be set holds for f be Function of X, Y holds for y holds y in (f .: P) implies ex x st x in X & x in P & y = (f . x)

    proof

      let P be set;

      let f be Function of X, Y;

      let y;

      assume y in (f .: P);

      then

      consider x be object such that

       A1: x in ( dom f) and

       A2: x in P & y = (f . x) by FUNCT_1:def 6;

      reconsider x as set by TARSKI: 1;

      take x;

      thus x in X by A1;

      thus thesis by A2;

    end;

    theorem :: FUNCT_2:65

    for f be Function of X, Y holds for y st y in (f .: P) holds ex c be Element of X st c in P & y = (f . c)

    proof

      let f be Function of X, Y;

      let y;

      assume y in (f .: P);

      then

      consider x such that

       A1: x in X and

       A2: x in P & y = (f . x) by Th63;

      reconsider c = x as Element of X by A1;

      take c;

      thus thesis by A2;

    end;

    begin

    theorem :: FUNCT_2:66

    

     Th65: for f be set st f in ( Funcs (X,Y)) holds f is Function of X, Y

    proof

      let f be set;

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

      then ( not (Y = {} & X <> {} )) & ex f9 be Function st f9 = f & ( dom f9) = X & ( rng f9) c= Y by Def2;

      hence thesis by Def1, RELSET_1: 4;

    end;

    scheme :: FUNCT_2:sch5

    Lambda1C { A,B() -> set , C[ object], F,G( object) -> object } :

ex f be Function of A(), B() st for x be object st x in A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x))

      provided

       A1: for x be object st x in A() holds (C[x] implies F(x) in B()) & ( not C[x] implies G(x) in B());

       A2:

      now

        set x = the Element of A();

        assume

         A3: B() = {} ;

        assume

         A4: A() <> {} ;

        then C[x] implies F(x) in B() by A1;

        hence contradiction by A1, A3, A4;

      end;

      consider f be Function such that

       A5: ( dom f) = A() and

       A6: for x be object st x in A() holds (C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from PARTFUN1:sch 1;

      ( rng f) c= B()

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A7: x in ( dom f) and

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

        

         A9: not C[x] implies (f . x) = G(x) by A5, A6, A7;

        C[x] implies (f . x) = F(x) by A5, A6, A7;

        hence thesis by A1, A5, A7, A8, A9;

      end;

      then f is Function of A(), B() by A5, A2, Def1, RELSET_1: 4;

      hence thesis by A6;

    end;

    theorem :: FUNCT_2:67

    for f be PartFunc of X, Y st ( dom f) = X holds f is Function of X, Y

    proof

      let f be PartFunc of X, Y;

      ( rng f) c= Y;

      hence thesis by Th2;

    end;

    theorem :: FUNCT_2:68

    for f be PartFunc of X, Y st f is total holds f is Function of X, Y;

    theorem :: FUNCT_2:69

    for f be PartFunc of X, Y st (Y = {} implies X = {} ) & f is Function of X, Y holds f is total;

    theorem :: FUNCT_2:70

    for f be Function of X, Y st (Y = {} implies X = {} ) holds <:f, X, Y:> is total;

    registration

      let X;

      let f be Function of X, X;

      cluster <:f, X, X:> -> total;

      coherence ;

    end

    theorem :: FUNCT_2:71

    

     Th70: for f be PartFunc of X, Y st Y = {} implies X = {} holds ex g be Function of X, Y st for x be object st x in ( dom f) holds (g . x) = (f . x)

    proof

      let f be PartFunc of X, Y such that

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

      per cases ;

        suppose Y = {} ;

        then

        reconsider g = f as Function of X, Y by A1;

        take g;

        thus thesis;

      end;

        suppose

         A2: Y <> {} ;

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

        defpred P[ object] means $1 in ( dom f);

        set y = the Element of Y;

        deffunc G( object) = y;

        

         A3: for x be object st x in X holds ( P[x] implies F(x) in Y) & ( not P[x] implies G(x) in Y) by A2, PARTFUN1: 4;

        consider g be Function of X, Y such that

         A4: for x be object st x in X holds ( P[x] implies (g . x) = F(x)) & ( not P[x] implies (g . x) = G(x)) from Lambda1C( A3);

        take g;

        thus thesis by A4;

      end;

    end;

    theorem :: FUNCT_2:72

    ( Funcs (X,Y)) c= ( PFuncs (X,Y))

    proof

      let x be object;

      assume x in ( Funcs (X,Y));

      then ex f be Function st x = f & ( dom f) = X & ( rng f) c= Y by Def2;

      hence thesis by PARTFUN1:def 3;

    end;

    theorem :: FUNCT_2:73

    for f,g be Function of X, Y st (Y = {} implies X = {} ) & f tolerates g holds f = g by PARTFUN1: 66;

    theorem :: FUNCT_2:74

    for f,g be Function of X, X st f tolerates g holds f = g by PARTFUN1: 66;

    theorem :: FUNCT_2:75

    

     Th74: for f be PartFunc of X, Y holds for g be Function of X, Y st Y = {} implies X = {} holds f tolerates g iff for x be object st x in ( dom f) holds (f . x) = (g . x)

    proof

      let f be PartFunc of X, Y;

      let g be Function of X, Y;

      assume Y = {} implies X = {} ;

      then ( dom g) = X by Def1;

      hence thesis by PARTFUN1: 53;

    end;

    theorem :: FUNCT_2:76

    for f be PartFunc of X, X holds for g be Function of X, X holds f tolerates g iff for x be object st x in ( dom f) holds (f . x) = (g . x)

    proof

      let f be PartFunc of X, X;

      let g be Function of X, X;

      X = {} implies X = {} ;

      hence thesis by Th74;

    end;

    theorem :: FUNCT_2:77

    

     Th76: for f be PartFunc of X, Y st Y = {} implies X = {} holds ex g be Function of X, Y st f tolerates g

    proof

      let f be PartFunc of X, Y;

      assume

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

      then

      consider g be Function of X, Y such that

       A2: for x be object st x in ( dom f) holds (g . x) = (f . x) by Th70;

      take g;

      thus thesis by A1, A2, Th74;

    end;

    theorem :: FUNCT_2:78

    for f,g be PartFunc of X, X holds for h be Function of X, X st f tolerates h & g tolerates h holds f tolerates g by PARTFUN1: 67;

    theorem :: FUNCT_2:79

    for f,g be PartFunc of X, Y st (Y = {} implies X = {} ) & f tolerates g holds ex h be Function of X, Y st f tolerates h & g tolerates h

    proof

      let f,g be PartFunc of X, Y;

      assume (Y = {} implies X = {} ) & f tolerates g;

      then ex h be PartFunc of X, Y st h is total & f tolerates h & g tolerates h by PARTFUN1: 68;

      hence thesis;

    end;

    theorem :: FUNCT_2:80

    for f be PartFunc of X, Y holds for g be Function of X, Y st (Y = {} implies X = {} ) & f tolerates g holds g in ( TotFuncs f) by PARTFUN1:def 5;

    theorem :: FUNCT_2:81

    for f be PartFunc of X, X holds for g be Function of X, X st f tolerates g holds g in ( TotFuncs f) by PARTFUN1:def 5;

    theorem :: FUNCT_2:82

    

     Th81: for f be PartFunc of X, Y holds for g be set st g in ( TotFuncs f) holds g is Function of X, Y

    proof

      let f be PartFunc of X, Y;

      let g be set;

      assume g in ( TotFuncs f);

      then ex g9 be PartFunc of X, Y st g9 = g & g9 is total & f tolerates g9 by PARTFUN1:def 5;

      hence thesis;

    end;

    theorem :: FUNCT_2:83

    for f be PartFunc of X, Y holds ( TotFuncs f) c= ( Funcs (X,Y))

    proof

      let f be PartFunc of X, Y;

      per cases ;

        suppose Y = {} & X <> {} ;

        hence thesis;

      end;

        suppose

         A1: Y <> {} or X = {} ;

        let g be object;

        assume g in ( TotFuncs f);

        then g is Function of X, Y by Th81;

        hence thesis by A1, Th8;

      end;

    end;

    theorem :: FUNCT_2:84

    ( TotFuncs <: {} , X, Y:>) = ( Funcs (X,Y))

    proof

      per cases ;

        suppose

         A1: Y = {} & X <> {} ;

        then ( TotFuncs <: {} , X, Y:>) = {} ;

        hence thesis by A1;

      end;

        suppose

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

        for g be object holds g in ( TotFuncs <: {} , X, Y:>) iff g in ( Funcs (X,Y))

        proof

          let g be object;

          thus g in ( TotFuncs <: {} , X, Y:>) implies g in ( Funcs (X,Y))

          proof

            assume g in ( TotFuncs <: {} , X, Y:>);

            then g is Function of X, Y by Th81;

            hence thesis by A2, Th8;

          end;

          assume

           A3: g in ( Funcs (X,Y));

          then

          reconsider g9 = g as PartFunc of X, Y by Th65;

          

           A4: <: {} , X, Y:> tolerates g9 by PARTFUN1: 60;

          g is Function of X, Y by A3, Th65;

          hence thesis by A2, A4, PARTFUN1:def 5;

        end;

        hence thesis by TARSKI: 2;

      end;

    end;

    theorem :: FUNCT_2:85

    for f be Function of X, Y st Y = {} implies X = {} holds ( TotFuncs <:f, X, Y:>) = {f} by PARTFUN1: 72;

    theorem :: FUNCT_2:86

    for f be Function of X, X holds ( TotFuncs <:f, X, X:>) = {f} by PARTFUN1: 72;

    theorem :: FUNCT_2:87

    for f be PartFunc of X, {y} holds for g be Function of X, {y} holds ( TotFuncs f) = {g}

    proof

      let f be PartFunc of X, {y};

      let g be Function of X, {y};

      for h be object holds h in ( TotFuncs f) iff h = g

      proof

        let h be object;

        thus h in ( TotFuncs f) implies h = g

        proof

          assume h in ( TotFuncs f);

          then h is Function of X, {y} by Th81;

          hence thesis by Th50;

        end;

        f tolerates g by PARTFUN1: 61;

        hence thesis by PARTFUN1:def 5;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FUNCT_2:88

    for f,g be PartFunc of X, Y st g c= f holds ( TotFuncs f) c= ( TotFuncs g)

    proof

      let f,g be PartFunc of X, Y such that

       A1: g c= f;

      let h be object;

      assume

       A2: h in ( TotFuncs f);

      then

      reconsider h9 = h as PartFunc of X, Y by PARTFUN1: 69;

      

       A3: h9 is total by A2, PARTFUN1: 70;

      g tolerates h9 by A1, A2, PARTFUN1: 58, PARTFUN1: 71;

      hence thesis by A3, PARTFUN1:def 5;

    end;

    theorem :: FUNCT_2:89

    

     Th88: for f,g be PartFunc of X, Y st ( dom g) c= ( dom f) & ( TotFuncs f) c= ( TotFuncs g) holds g c= f

    proof

      let f,g be PartFunc of X, Y such that

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

      now

        per cases ;

          suppose Y = {} & X <> {} ;

          hence thesis;

        end;

          suppose

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

          thus ( TotFuncs f) c= ( TotFuncs g) implies g c= f

          proof

            assume

             A3: ( TotFuncs f) c= ( TotFuncs g);

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

            proof

              let x be object;

              consider h be Function of X, Y such that

               A4: f tolerates h by A2, Th76;

              h in ( TotFuncs f) by A2, A4, PARTFUN1:def 5;

              then

               A5: g tolerates h by A3, PARTFUN1: 71;

              assume x in ( dom g);

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

              hence thesis by A5, A2, A4, PARTFUN1: 67, PARTFUN1:def 4;

            end;

            hence thesis by A1, GRFUNC_1: 2;

          end;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_2:90

    

     Th89: for f,g be PartFunc of X, Y st ( TotFuncs f) c= ( TotFuncs g) & (for y holds Y <> {y}) holds g c= f

    proof

      let f,g be PartFunc of X, Y such that

       A1: ( TotFuncs f) c= ( TotFuncs g) and

       A2: for y holds Y <> {y};

      now

        per cases ;

          suppose Y = {} ;

          hence ( dom g) c= ( dom f);

        end;

          suppose

           A3: Y <> {} ;

          thus ( dom g) c= ( dom f)

          proof

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

            defpred P[ object] means $1 in ( dom f);

            let x be object such that

             A4: x in ( dom g) and

             A5: not x in ( dom f);

            

             A6: Y <> {(g . x)} by A2;

            (g . x) in Y by A4, PARTFUN1: 4;

            then

            consider y be object such that

             A7: y in Y and

             A8: y <> (g . x) by A6, ZFMISC_1: 35;

            deffunc G( object) = y;

            

             A9: for x9 be object st x9 in X holds ( P[x9] implies F(x9) in Y) & ( not P[x9] implies G(x9) in Y) by A7, PARTFUN1: 4;

            consider h be Function of X, Y such that

             A10: for x9 be object st x9 in X holds ( P[x9] implies (h . x9) = F(x9)) & ( not P[x9] implies (h . x9) = G(x9)) from Lambda1C( A9);

            f tolerates h

            proof

              let x9 be object;

              assume x9 in (( dom f) /\ ( dom h));

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

              hence thesis by A10;

            end;

            then

             A11: h in ( TotFuncs f) by A3, PARTFUN1:def 5;

            x in X by A4;

            then x in ( dom h) by A3, Def1;

            then

             A12: x in (( dom g) /\ ( dom h)) by A4, XBOOLE_0:def 4;

            (h . x) = y by A4, A5, A10;

            hence contradiction by A8, A11, A12, A1, PARTFUN1: 71, PARTFUN1:def 4;

          end;

        end;

      end;

      hence thesis by A1, Th88;

    end;

    theorem :: FUNCT_2:91

    for f,g be PartFunc of X, Y st (for y holds Y <> {y}) & ( TotFuncs f) = ( TotFuncs g) holds f = g by Th89;

    registration

      let A,B be non empty set;

      cluster -> non empty for Function of A, B;

      coherence by Def1, RELAT_1: 38;

    end

    begin

    scheme :: FUNCT_2:sch6

    LambdaSep1 { D,R() -> non empty set , A() -> Element of D() , B() -> Element of R() , F( object) -> Element of R() } :

ex f be Function of D(), R() st (f . A()) = B() & for x be Element of D() st x <> A() holds (f . x) = F(x);

      defpred P[ set, set] means ($1 = A() implies $2 = B()) & ($1 <> A() implies $2 = F($1));

      

       A1: for x be Element of D() holds ex y be Element of R() st P[x, y]

      proof

        let x be Element of D();

        x = A() implies thesis;

        hence thesis;

      end;

      consider f be Function of D(), R() such that

       A2: for x be Element of D() holds P[x, (f . x)] from FuncExD( A1);

      take f;

      thus thesis by A2;

    end;

    scheme :: FUNCT_2:sch7

    LambdaSep2 { D,R() -> non empty set , A1,A2() -> Element of D() , B1,B2() -> Element of R() , F( object) -> Element of R() } :

ex f be Function of D(), R() st (f . A1()) = B1() & (f . A2()) = B2() & for x be Element of D() st x <> A1() & x <> A2() holds (f . x) = F(x)

      provided

       A1: A1() <> A2();

      defpred P[ set, set] means ($1 = A1() implies $2 = B1()) & ($1 = A2() implies $2 = B2()) & ($1 <> A1() & $1 <> A2() implies $2 = F($1));

      

       A2: for x be Element of D() holds ex y be Element of R() st P[x, y]

      proof

        let x be Element of D();

        

         A3: x = A2() implies thesis by A1;

        x = A1() implies thesis by A1;

        hence thesis by A3;

      end;

      consider f be Function of D(), R() such that

       A4: for x be Element of D() holds P[x, (f . x)] from FuncExD( A2);

      take f;

      thus thesis by A4;

    end;

    theorem :: FUNCT_2:92

    for A,B be set holds for f be Function st f in ( Funcs (A,B)) holds ( dom f) = A & ( rng f) c= B

    proof

      let A,B be set;

      let f be Function;

      assume f in ( Funcs (A,B));

      then ex g be Function st f = g & ( dom g) = A & ( rng g) c= B by Def2;

      hence thesis;

    end;

    scheme :: FUNCT_2:sch8

    FunctRealEx { X() -> non empty set , Y() -> set , F( object) -> object } :

ex f be Function of X(), Y() st for x be Element of X() holds (f . x) = F(x)

      provided

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

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

      

       A2: for x be object st x in X() holds ex y be object st y in Y() & P[x, y] by A1;

      ex f be Function of X(), Y() st for x be object st x in X() holds P[x, (f . x)] from FuncEx1( A2);

      then

      consider f be Function of X(), Y() such that

       A3: for x be object st x in X() holds (f . x) = F(x);

      for x be Element of X() holds (f . x) = F(x) by A3;

      hence thesis;

    end;

    scheme :: FUNCT_2:sch9

    KappaMD { X,Y() -> non empty set , F( object) -> object } :

ex f be Function of X(), Y() st for x be Element of X() holds (f . x) = F(x)

      provided

       A1: for x be Element of X() holds F(x) is Element of Y();

       A2:

      now

        let x be Element of X();

        F(x) is Element of Y() by A1;

        hence F(x) in Y();

      end;

      consider f be Function of X(), Y() such that

       A3: for x be Element of X() holds (f . x) = F(x) from FunctRealEx( A2);

      take f;

      thus thesis by A3;

    end;

    definition

      let A,B,C be non empty set;

      let f be Function of A, [:B, C:];

      :: original: pr1

      redefine

      :: FUNCT_2:def5

      func pr1 f -> Function of A, B means

      : Def5: for x be Element of A holds (it . x) = ((f . x) `1 );

      coherence

      proof

        

         A1: ( dom ( pr1 f)) = ( dom f) by MCART_1:def 12;

        

         A2: ( rng ( pr1 f)) c= B

        proof

          let x be object;

          assume x in ( rng ( pr1 f));

          then

          consider y be object such that

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

          x = ((f . y) `1 ) & (f . y) in [:B, C:] by A1, A3, Th5, MCART_1:def 12;

          hence thesis by MCART_1: 10;

        end;

        ( dom ( pr1 f)) = A by A1, Def1;

        hence thesis by A2, Th2;

      end;

      compatibility

      proof

        let IT be Function of A, B;

        

         A4: ( dom ( pr1 f)) = ( dom f) by MCART_1:def 12;

        then

         A5: ( dom ( pr1 f)) = A by Def1;

        hence IT = ( pr1 f) implies for x be Element of A holds (IT . x) = ((f . x) `1 ) by A4, MCART_1:def 12;

        assume for x be Element of A holds (IT . x) = ((f . x) `1 );

        then

         A6: for x be object st x in ( dom f) holds (IT . x) = ((f . x) `1 );

        ( dom IT) = ( dom f) by A4, A5, Def1;

        hence thesis by A6, MCART_1:def 12;

      end;

      :: original: pr2

      redefine

      :: FUNCT_2:def6

      func pr2 f -> Function of A, C means

      : Def6: for x be Element of A holds (it . x) = ((f . x) `2 );

      coherence

      proof

        

         A7: ( dom ( pr2 f)) = ( dom f) by MCART_1:def 13;

        

         A8: ( rng ( pr2 f)) c= C

        proof

          let x be object;

          assume x in ( rng ( pr2 f));

          then

          consider y be object such that

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

          x = ((f . y) `2 ) & (f . y) in [:B, C:] by A7, A9, Th5, MCART_1:def 13;

          hence thesis by MCART_1: 10;

        end;

        ( dom ( pr2 f)) = A by A7, Def1;

        hence thesis by A8, Th2;

      end;

      compatibility

      proof

        let IT be Function of A, C;

        

         A10: ( dom ( pr2 f)) = ( dom f) by MCART_1:def 13;

        then

         A11: ( dom ( pr2 f)) = A by Def1;

        hence IT = ( pr2 f) implies for x be Element of A holds (IT . x) = ((f . x) `2 ) by A10, MCART_1:def 13;

        assume for x be Element of A holds (IT . x) = ((f . x) `2 );

        then

         A12: for x be object st x in ( dom f) holds (IT . x) = ((f . x) `2 );

        ( dom IT) = ( dom f) by A10, A11, Def1;

        hence thesis by A12, MCART_1:def 13;

      end;

    end

    definition

      let A1 be set, B1 be non empty set, A2 be set, B2 be non empty set, f1 be Function of A1, B1, f2 be Function of A2, B2;

      :: original: =

      redefine

      :: FUNCT_2:def7

      pred f1 = f2 means A1 = A2 & for a be Element of A1 holds (f1 . a) = (f2 . a);

      compatibility

      proof

        

         A1: ( dom f1) = A1 by Def1;

        hence f1 = f2 implies A1 = A2 & for a be Element of A1 holds (f1 . a) = (f2 . a) by Def1;

        assume that

         A2: A1 = A2 and

         A3: for a be Element of A1 holds (f1 . a) = (f2 . a);

        

         A4: ( dom f2) = A2 by Def1;

        for a be object st a in A1 holds (f1 . a) = (f2 . a) by A3;

        hence thesis by A1, A4, A2;

      end;

    end

    definition

      let A,B be set, f1,f2 be Function of A, B;

      :: original: =

      redefine

      :: FUNCT_2:def8

      pred f1 = f2 means for a be Element of A holds (f1 . a) = (f2 . a);

      compatibility by Th62;

    end

    theorem :: FUNCT_2:93

    for N be set, f be Function of N, ( bool N) holds ex R be Relation of N st for i be set st i in N holds ( Im (R,i)) = (f . i)

    proof

      let N be set, f be Function of N, ( bool N);

      deffunc F( set) = (f . $1);

      

       A1: for i be Element of N st i in ( [#] N) holds F(i) c= ( [#] N)

      proof

        let i be Element of N;

        assume i in ( [#] N);

        then (f . i) in ( bool N) by Th5;

        hence thesis;

      end;

      consider R be Relation of ( [#] N) such that

       A2: for i be Element of N st i in ( [#] N) holds ( Im (R,i)) = F(i) from RELSET_1:sch 3( A1);

      reconsider R as Relation of N;

      take R;

      thus thesis by A2;

    end;

    theorem :: FUNCT_2:94

    

     Th93: for A be Subset of X holds (( id X) " A) = A

    proof

      let A be Subset of X;

      

      thus A = (( id X) " (( id X) .: A)) by Th61

      .= (( id X) " A) by FUNCT_1: 92;

    end;

    reserve A,B for non empty set;

    theorem :: FUNCT_2:95

    for f be Function of A, B, A0 be Subset of A, B0 be Subset of B holds (f .: A0) c= B0 iff A0 c= (f " B0)

    proof

      let f be Function of A, B, A0 be Subset of A, B0 be Subset of B;

      thus (f .: A0) c= B0 implies A0 c= (f " B0)

      proof

        assume (f .: A0) c= B0;

        then

         A1: (f " (f .: A0)) c= (f " B0) by RELAT_1: 143;

        A0 c= (f " (f .: A0)) by Th41;

        hence thesis by A1;

      end;

      thus A0 c= (f " B0) implies (f .: A0) c= B0

      proof

        assume A0 c= (f " B0);

        then

         A2: (f .: A0) c= (f .: (f " B0)) by RELAT_1: 123;

        (f .: (f " B0)) c= B0 by FUNCT_1: 75;

        hence thesis by A2;

      end;

    end;

    theorem :: FUNCT_2:96

    for f be Function of A, B, A0 be non empty Subset of A, f0 be Function of A0, B st for c be Element of A st c in A0 holds (f . c) = (f0 . c) holds (f | A0) = f0

    proof

      let f be Function of A, B, A0 be non empty Subset of A, f0 be Function of A0, B such that

       A1: for c be Element of A st c in A0 holds (f . c) = (f0 . c);

      reconsider g = (f | A0) as Function of A0, B by Th32;

      for c be Element of A0 holds (g . c) = (f0 . c)

      proof

        let c be Element of A0;

        

        thus (g . c) = (f . c) by FUNCT_1: 49

        .= (f0 . c) by A1;

      end;

      hence thesis by Th62;

    end;

    theorem :: FUNCT_2:97

    for f be Function, A0,C be set st C c= A0 holds (f .: C) = ((f | A0) .: C)

    proof

      let f be Function, A0,C be set;

      assume

       A1: C c= A0;

      

      thus ((f | A0) .: C) = ((f * ( id A0)) .: C) by RELAT_1: 65

      .= (f .: (( id A0) .: C)) by RELAT_1: 126

      .= (f .: C) by A1, FUNCT_1: 92;

    end;

    theorem :: FUNCT_2:98

    for f be Function, A0,D be set st (f " D) c= A0 holds (f " D) = ((f | A0) " D)

    proof

      let f be Function, A0,D be set;

      assume

       A1: (f " D) c= A0;

      

      thus ((f | A0) " D) = ((f * ( id A0)) " D) by RELAT_1: 65

      .= (( id A0) " (f " D)) by RELAT_1: 146

      .= (f " D) by A1, Th93;

    end;

    scheme :: FUNCT_2:sch10

    MChoice { A() -> non empty set , B() -> non empty set , F( object) -> set } :

ex t be Function of A(), B() st for a be Element of A() holds (t . a) in F(a)

      provided

       A1: for a be Element of A() holds B() meets F(a);

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

      

       A2: for e be object st e in A() holds ex u be object st u in B() & P[e, u] by A1, XBOOLE_0: 3;

      consider t be Function such that

       A3: ( dom t) = A() & ( rng t) c= B() and

       A4: for e be object st e in A() holds P[e, (t . e)] from FUNCT_1:sch 6( A2);

      reconsider t as Function of A(), B() by A3, Def1, RELSET_1: 4;

      take t;

      let a be Element of A();

      thus thesis by A4;

    end;

    theorem :: FUNCT_2:99

    

     Th98: for X,D be non empty set, p be Function of X, D, i be Element of X holds (p /. i) = (p . i)

    proof

      let X,D be non empty set, p be Function of X, D, i be Element of X;

      i in X;

      then i in ( dom p) by Def1;

      hence thesis by PARTFUN1:def 6;

    end;

    registration

      let X,D be non empty set, p be Function of X, D, i be Element of X;

      identify p . i with p /. i;

      correctness by Th98;

    end

    theorem :: FUNCT_2:100

    for S,X be set, f be Function of S, X, A be Subset of X st X = {} implies S = {} holds ((f " A) ` ) = (f " (A ` ))

    proof

      let S,X be set, f be Function of S, X, A be Subset of X such that

       A1: X = {} implies S = {} ;

      (A /\ (A ` )) = {} by XBOOLE_0:def 7, XBOOLE_1: 79;

      

      then ((f " A) /\ (f " (A ` ))) = (f " ( {} X)) by FUNCT_1: 68

      .= {} ;

      then

       A2: (f " A) misses (f " (A ` ));

      ((f " A) \/ (f " (A ` ))) = (f " (A \/ (A ` ))) by RELAT_1: 140

      .= (f " ( [#] X)) by SUBSET_1: 10

      .= ( [#] S) by A1, Th39;

      

      then (((f " A) ` ) /\ ((f " (A ` )) ` )) = (( [#] S) ` ) by XBOOLE_1: 53

      .= ( {} S) by XBOOLE_1: 37;

      then ((f " A) ` ) misses ((f " (A ` )) ` );

      hence thesis by A2, SUBSET_1: 25;

    end;

    theorem :: FUNCT_2:101

    for X,Y,Z be set, D be non empty set, f be Function of X, D st Y c= X & (f .: Y) c= Z holds (f | Y) is Function of Y, Z

    proof

      let X,Y,Z be set, D be non empty set, f be Function of X, D;

      assume that

       A1: Y c= X and

       A2: (f .: Y) c= Z;

      ( dom f) = X by Def1;

      then

       A3: ( dom (f | Y)) = Y by A1, RELAT_1: 62;

       A4:

      now

        assume Z = {} ;

        then ( rng (f | Y)) = {} by A2, RELAT_1: 115;

        hence Y = {} by A3, RELAT_1: 42;

      end;

      ( rng (f | Y)) c= Z by A2, RELAT_1: 115;

      hence thesis by A3, A4, Def1, RELSET_1: 4;

    end;

    definition

      let T,S be non empty set;

      let f be Function of T, S;

      let G be Subset-Family of S;

      :: FUNCT_2:def9

      func f " G -> Subset-Family of T means

      : Def9: for A be Subset of T holds A in it iff ex B be Subset of S st B in G & A = (f " B);

      existence

      proof

        defpred P[ Subset of T] means ex B be Subset of S st B in G & $1 = (f " B);

        ex R be Subset-Family of T st for A be Subset of T holds A in R iff P[A] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Subset-Family of T such that

         A1: for A be Subset of T holds A in R1 iff ex B be Subset of S st B in G & A = (f " B) and

         A2: for A be Subset of T holds A in R2 iff ex B be Subset of S st B in G & A = (f " B);

        for x be object holds (x in R1 iff x in R2)

        proof

          let x be object;

          thus x in R1 implies x in R2

          proof

            assume

             A3: x in R1;

            then

            reconsider x as Subset of T;

            ex B be Subset of S st B in G & x = (f " B) by A1, A3;

            hence thesis by A2;

          end;

          assume

           A4: x in R2;

          then

          reconsider x as Subset of T;

          ex B be Subset of S st B in G & x = (f " B) by A2, A4;

          hence thesis by A1;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: FUNCT_2:102

    for T,S be non empty set, f be Function of T, S, A,B be Subset-Family of S st A c= B holds (f " A) c= (f " B)

    proof

      let T,S be non empty set;

      let f be Function of T, S;

      let A,B be Subset-Family of S;

      assume

       A1: A c= B;

      let x be object;

      assume

       A2: x in (f " A);

      then

      reconsider x as Subset of T;

      ex C be Subset of S st C in B & x = (f " C)

      proof

        consider C be Subset of S such that

         A3: C in A & x = (f " C) by A2, Def9;

        take C;

        thus thesis by A1, A3;

      end;

      hence thesis by Def9;

    end;

    definition

      let T,S be set;

      let f be Function of T, S;

      let G be Subset-Family of T;

      :: FUNCT_2:def10

      func f .: G -> Subset-Family of S means

      : Def10: for A be Subset of S holds A in it iff ex B be Subset of T st B in G & A = (f .: B);

      existence

      proof

        thus ex R be Subset-Family of S st for A be Subset of S holds A in R iff ex B be Subset of T st B in G & A = (f .: B)

        proof

          defpred P[ Subset of S] means ex B be Subset of T st B in G & $1 = (f .: B);

          ex R be Subset-Family of S st for A be Subset of S holds A in R iff P[A] from SUBSET_1:sch 3;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let R1,R2 be Subset-Family of S such that

         A1: for A be Subset of S holds A in R1 iff ex B be Subset of T st B in G & A = (f .: B) and

         A2: for A be Subset of S holds A in R2 iff ex B be Subset of T st B in G & A = (f .: B);

        for x be object holds (x in R1 iff x in R2)

        proof

          let x be object;

          thus x in R1 implies x in R2

          proof

            assume

             A3: x in R1;

            then

            reconsider x as Subset of S;

            ex B be Subset of T st B in G & x = (f .: B) by A1, A3;

            hence thesis by A2;

          end;

          assume

           A4: x in R2;

          then

          reconsider x as Subset of S;

          ex B be Subset of T st B in G & x = (f .: B) by A2, A4;

          hence thesis by A1;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: FUNCT_2:103

    for T,S be set, f be Function of T, S, A,B be Subset-Family of T st A c= B holds (f .: A) c= (f .: B)

    proof

      let T,S be set;

      let f be Function of T, S;

      let A,B be Subset-Family of T;

      assume

       A1: A c= B;

      let x be object;

      assume

       A2: x in (f .: A);

      then

      reconsider x as Subset of S;

      ex C be Subset of T st C in B & x = (f .: C)

      proof

        consider C be Subset of T such that

         A3: C in A & x = (f .: C) by A2, Def10;

        take C;

        thus thesis by A1, A3;

      end;

      hence thesis by Def10;

    end;

    theorem :: FUNCT_2:104

    for T,S be non empty set, f be Function of T, S, B be Subset-Family of S, P be Subset of S st (f .: (f " B)) is Cover of P holds B is Cover of P

    proof

      let T,S be non empty set;

      let f be Function of T, S;

      let B be Subset-Family of S;

      let P be Subset of S;

      assume (f .: (f " B)) is Cover of P;

      then

       A1: P c= ( union (f .: (f " B))) by SETFAM_1:def 11;

      P c= ( union B)

      proof

        let x be object;

        assume x in P;

        then

        consider Y be set such that

         A2: x in Y and

         A3: Y in (f .: (f " B)) by A1, TARSKI:def 4;

        ex Z be set st x in Z & Z in B

        proof

          reconsider Y as Subset of S by A3;

          consider Y1 be Subset of T such that

           A4: Y1 in (f " B) and

           A5: Y = (f .: Y1) by A3, Def10;

          consider Y2 be Subset of S such that

           A6: Y2 in B & Y1 = (f " Y2) by A4, Def9;

          

           A7: (f .: (f " Y2)) c= Y2 by FUNCT_1: 75;

          reconsider Y2 as set;

          take Y2;

          thus thesis by A2, A5, A6, A7;

        end;

        hence thesis by TARSKI:def 4;

      end;

      hence thesis by SETFAM_1:def 11;

    end;

    theorem :: FUNCT_2:105

    for T,S be non empty set, f be Function of T, S, B be Subset-Family of T, P be Subset of T st B is Cover of P holds (f " (f .: B)) is Cover of P

    proof

      let T,S be non empty set;

      let f be Function of T, S;

      let B be Subset-Family of T;

      let P be Subset of T;

      assume B is Cover of P;

      then

       A1: P c= ( union B) by SETFAM_1:def 11;

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

      proof

        let x be object;

        assume x in P;

        then

        consider Y be set such that

         A2: x in Y and

         A3: Y in B by A1, TARSKI:def 4;

        ex Z be set st x in Z & Z in (f " (f .: B))

        proof

          reconsider Y as Subset of T by A3;

          set Z = (f " (f .: Y));

          take Z;

          ( dom f) = T by Def1;

          then

           A4: Y c= (f " (f .: Y)) by FUNCT_1: 76;

          (f .: Y) in (f .: B) by A3, Def10;

          hence thesis by A2, A4, Def9;

        end;

        hence thesis by TARSKI:def 4;

      end;

      hence thesis by SETFAM_1:def 11;

    end;

    theorem :: FUNCT_2:106

    for T,S be non empty set, f be Function of T, S, Q be Subset-Family of S holds ( union (f .: (f " Q))) c= ( union Q)

    proof

      let T,S be non empty set;

      let f be Function of T, S;

      let Q be Subset-Family of S;

      let x be object;

      thus x in ( union (f .: (f " Q))) implies x in ( union Q)

      proof

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

        then

        consider A be set such that

         A1: x in A and

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

        reconsider A as Subset of S by A2;

        consider A1 be Subset of T such that

         A3: A1 in (f " Q) and

         A4: A = (f .: A1) by A2, Def10;

        consider A2 be Subset of S such that

         A5: A2 in Q & A1 = (f " A2) by A3, Def9;

        (f .: (f " A2)) c= A2 by FUNCT_1: 75;

        hence thesis by A1, A4, A5, TARSKI:def 4;

      end;

    end;

    theorem :: FUNCT_2:107

    for T,S be non empty set, f be Function of T, S, P be Subset-Family of T holds ( union P) c= ( union (f " (f .: P)))

    proof

      let T,S be non empty set;

      let f be Function of T, S;

      let P be Subset-Family of T;

      let x be object;

      assume x in ( union P);

      then

      consider A be set such that

       A1: x in A and

       A2: A in P by TARSKI:def 4;

      

       A3: A c= T by A2;

      reconsider A as Subset of T by A2;

      reconsider A1 = (f .: A) as Subset of S;

      reconsider A2 = (f " A1) as Subset of T;

      A c= ( dom f) by A3, Def1;

      then

       A4: A c= A2 by FUNCT_1: 76;

      A1 in (f .: P) by A2, Def10;

      then A2 in (f " (f .: P)) by Def9;

      hence thesis by A1, A4, TARSKI:def 4;

    end;

    definition

      let X,Z be set, Y be non empty set;

      let f be Function of X, Y;

      let p be Z -valued Function;

      assume

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

      :: FUNCT_2:def11

      func p /* f -> Function of X, Z equals

      : Def11: (p * f);

      coherence

      proof

        ( dom f) = X by Def1;

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

        then

         A2: (p * f) is total;

        ( rng (p * f)) c= Z;

        hence thesis by A2, RELSET_1: 4;

      end;

    end

    reserve Y for non empty set,

f for Function of X, Y,

p for PartFunc of Y, Z,

x for Element of X;

    theorem :: FUNCT_2:108

    

     Th107: X <> {} & ( rng f) c= ( dom p) implies ((p /* f) . x) = (p . (f . x))

    proof

      assume that

       A1: X <> {} and

       A2: ( rng f) c= ( dom p);

      (p /* f) = (p * f) by A2, Def11;

      hence thesis by A1, Th15;

    end;

    theorem :: FUNCT_2:109

    

     Th108: X <> {} & ( rng f) c= ( dom p) implies ((p /* f) . x) = (p /. (f . x))

    proof

      assume that

       A1: X <> {} and

       A2: ( rng f) c= ( dom p);

      

       A3: (f . x) in ( rng f) by A1, Th4;

      

      thus ((p /* f) . x) = (p . (f . x)) by A1, A2, Th107

      .= (p /. (f . x)) by A2, A3, PARTFUN1:def 6;

    end;

    reserve g for Function of X, X;

    theorem :: FUNCT_2:110

    ( rng f) c= ( dom p) implies ((p /* f) * g) = (p /* (f * g))

    proof

      

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

      assume

       A2: ( rng f) c= ( dom p);

      

      hence ((p /* f) * g) = ((p * f) * g) by Def11

      .= (p * (f * g)) by RELAT_1: 36

      .= (p /* (f * g)) by A2, A1, Def11, XBOOLE_1: 1;

    end;

    theorem :: FUNCT_2:111

    for X,Y be non empty set, f be Function of X, Y holds f is constant iff ex y be Element of Y st ( rng f) = {y}

    proof

      let X,Y be non empty set;

      let f be Function of X, Y;

      hereby

        consider x be object such that

         A1: x in ( dom f) by XBOOLE_0:def 1;

        set y = (f . x);

        reconsider y as Element of Y by A1, Th5;

        assume

         A2: f is constant;

        take y;

        for y9 be object holds y9 in ( rng f) iff y9 = y

        proof

          let y9 be object;

          hereby

            assume y9 in ( rng f);

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

            hence y9 = y by A2, A1;

          end;

          assume y9 = y;

          hence thesis by A1, Th4;

        end;

        hence ( rng f) = {y} by TARSKI:def 1;

      end;

      given y be Element of Y such that

       A3: ( rng f) = {y};

      let x,x9 be object;

      assume x in ( dom f);

      then

       A4: (f . x) in ( rng f) by Th4;

      assume x9 in ( dom f);

      then

       A5: (f . x9) in ( rng f) by Th4;

      

      thus (f . x) = y by A3, A4, TARSKI:def 1

      .= (f . x9) by A3, A5, TARSKI:def 1;

    end;

    theorem :: FUNCT_2:112

    for A,B be non empty set, x be Element of A, f be Function of A, B holds (f . x) in ( rng f)

    proof

      let A,B be non empty set, x be Element of A, f be Function of A, B;

      ( dom f) = A by Def1;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: FUNCT_2:113

    

     Th112: for A,B be set, f be Function of A, B st y in ( rng f) holds ex x be Element of A st y = (f . x)

    proof

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

      assume y in ( rng f);

      then

      consider x be object such that

       A1: x in A and

       A2: (f . x) = y by Th11;

      reconsider x as Element of A by A1;

      take x;

      thus thesis by A2;

    end;

    theorem :: FUNCT_2:114

    for A,B be non empty set, f be Function of A, B st for x be Element of A holds (f . x) in Z holds ( rng f) c= Z

    proof

      let A,B be non empty set, f be Function of A, B such that

       A1: for x be Element of A holds (f . x) in Z;

      let y be object;

      assume y in ( rng f);

      then ex x be Element of A st (f . x) = y by Th112;

      hence thesis by A1;

    end;

    reserve X,Y for non empty set,

Z,S,T for set,

f for Function of X, Y,

g for PartFunc of Y, Z,

x for Element of X;

    theorem :: FUNCT_2:115

    g is total implies ((g /* f) . x) = (g . (f . x))

    proof

      assume g is total;

      then ( dom g) = Y;

      then ( rng f) c= ( dom g);

      hence thesis by Th107;

    end;

    theorem :: FUNCT_2:116

    g is total implies ((g /* f) . x) = (g /. (f . x))

    proof

      assume g is total;

      then ( dom g) = Y;

      then ( rng f) c= ( dom g);

      hence thesis by Th108;

    end;

    theorem :: FUNCT_2:117

    

     Th116: ( rng f) c= ( dom (g | S)) implies ((g | S) /* f) = (g /* f)

    proof

      assume

       A1: ( rng f) c= ( dom (g | S));

      let x be Element of X;

      

       A2: ( dom (g | S)) c= ( dom g) by RELAT_1: 60;

      

       A3: (f . x) in ( rng f) by Th4;

      

      thus (((g | S) /* f) . x) = ((g | S) . (f . x)) by A1, Th107

      .= (g . (f . x)) by A1, A3, FUNCT_1: 47

      .= ((g /* f) . x) by A1, A2, Th107, XBOOLE_1: 1;

    end;

    theorem :: FUNCT_2:118

    ( rng f) c= ( dom (g | S)) & S c= T implies ((g | S) /* f) = ((g | T) /* f)

    proof

      assume

       A1: ( rng f) c= ( dom (g | S));

      assume S c= T;

      then (g | S) c= (g | T) by RELAT_1: 75;

      then

       A2: ( dom (g | S)) c= ( dom (g | T)) by RELAT_1: 11;

      

      thus ((g | S) /* f) = (g /* f) by A1, Th116

      .= ((g | T) /* f) by A1, A2, Th116, XBOOLE_1: 1;

    end;

    theorem :: FUNCT_2:119

    for H be Function of D, [:A, B:], d be Element of D holds (H . d) = [(( pr1 H) . d), (( pr2 H) . d)]

    proof

      let H be Function of D, [:A, B:], d be Element of D;

      

      thus (H . d) = [((H . d) `1 ), ((H . d) `2 )] by MCART_1: 21

      .= [((H . d) `1 ), (( pr2 H) . d)] by Def6

      .= [(( pr1 H) . d), (( pr2 H) . d)] by Def5;

    end;

    theorem :: FUNCT_2:120

    for A1,A2,B1,B2 be set holds for f be Function of A1, A2, g be Function of B1, B2 st f tolerates g holds (f /\ g) is Function of (A1 /\ B1), (A2 /\ B2)

    proof

      let A1,A2,B1,B2 be set;

      let f be Function of A1, A2, g be Function of B1, B2 such that

       A1: f tolerates g;

      

       A2: ( dom (f /\ g)) c= (( dom f) /\ ( dom g)) & (( dom f) /\ ( dom g)) c= (A1 /\ B1) by XBOOLE_1: 27, XTUPLE_0: 24;

       A3:

      now

        set a = the Element of (A1 /\ B1);

        assume that

         A4: ( dom f) = A1 and A1 <> {} and

         A5: ( dom g) = B1 and B1 <> {} ;

        hereby

          assume

           A6: (A1 /\ B1) <> {} ;

          then a in A1 by XBOOLE_0:def 4;

          then

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

          (f . a) = (g . a) & a in B1 by A1, A4, A5, A6, XBOOLE_0:def 4;

          then (f . a) in ( rng g) by A5, FUNCT_1:def 3;

          hence (A2 /\ B2) <> {} by A7, XBOOLE_0:def 4;

        end;

        thus ( dom (f /\ g)) = (A1 /\ B1)

        proof

          thus ( dom (f /\ g)) c= (A1 /\ B1) by A2;

          let a be object;

          assume

           A8: a in (A1 /\ B1);

          then a in A1 by XBOOLE_0:def 4;

          then

           A9: [a, (f . a)] in f by A4, FUNCT_1:def 2;

          (f . a) = (g . a) & a in B1 by A1, A4, A5, A8, XBOOLE_0:def 4;

          then [a, (f . a)] in g by A5, FUNCT_1:def 2;

          then [a, (f . a)] in (f /\ g) by A9, XBOOLE_0:def 4;

          hence thesis by XTUPLE_0:def 12;

        end;

      end;

      ( rng (f /\ g)) c= (( rng f) /\ ( rng g)) & (( rng f) /\ ( rng g)) c= (A2 /\ B2) by RELAT_1: 13, XBOOLE_1: 27;

      then

       A10: ( rng (f /\ g)) c= (A2 /\ B2);

      

       A11: A2 = {} or A2 <> {} ;

      

       A12: B2 = {} or B2 <> {} ;

       A13:

      now

        per cases ;

          case (A2 /\ B2) <> {} ;

          hence ( dom (f /\ g)) = (A1 /\ B1) by A12, A3, Def1, A11;

        end;

          case (A1 /\ B1) = {} ;

          hence ( dom (f /\ g)) = (A1 /\ B1) by A2;

        end;

          case (A2 /\ B2) = {} & (A1 /\ B1) <> {} ;

          hence (f /\ g) = {} by A12, A3, Def1, A11;

        end;

      end;

      thus thesis by A10, A13, Def1, RELSET_1: 4;

    end;

    registration

      let A,B be set;

      cluster ( Funcs (A,B)) -> functional;

      coherence

      proof

        let x be object;

        assume x in ( Funcs (A,B));

        then ex f be Function st x = f & ( dom f) = A & ( rng f) c= B by Def2;

        hence thesis;

      end;

    end

    definition

      let A,B be set;

      :: FUNCT_2:def12

      mode FUNCTION_DOMAIN of A,B -> non empty set means

      : Def12: for x be Element of it holds x is Function of A, B;

      existence

      proof

        take IT = { the Function of A, B};

        let g be Element of IT;

        thus thesis by TARSKI:def 1;

      end;

    end

    registration

      let A,B be set;

      cluster -> functional for FUNCTION_DOMAIN of A, B;

      coherence by Def12;

    end

    theorem :: FUNCT_2:121

    for f be Function of P, Q holds {f} is FUNCTION_DOMAIN of P, Q

    proof

      let f be Function of P, Q;

      for g be Element of {f} holds g is Function of P, Q by TARSKI:def 1;

      hence thesis by Def12;

    end;

    theorem :: FUNCT_2:122

    

     Th121: ( Funcs (P,B)) is FUNCTION_DOMAIN of P, B

    proof

      for f be Element of ( Funcs (P,B)) holds f is Function of P, B by Th65;

      hence thesis by Def12;

    end;

    definition

      let A be set, B be non empty set;

      :: original: Funcs

      redefine

      func Funcs (A,B) -> FUNCTION_DOMAIN of A, B ;

      coherence by Th121;

      let F be FUNCTION_DOMAIN of A, B;

      :: original: Element

      redefine

      mode Element of F -> Function of A, B ;

      coherence by Def12;

    end

    registration

      let I be set;

      cluster ( id I) -> total;

      coherence ;

    end

    definition

      let X, A;

      let F be Function of X, A;

      let x be set;

      assume

       A1: x in X;

      :: original: /.

      redefine

      :: FUNCT_2:def13

      func F /. x equals (F . x);

      compatibility

      proof

        let a be Element of A;

        x in ( dom F) by A1, Def1;

        hence thesis by PARTFUN1:def 6;

      end;

    end

    theorem :: FUNCT_2:123

    for X be set, Y be non empty set holds for f be Function of X, Y, g be X -valued Function holds ( dom (f * g)) = ( dom g)

    proof

      let X be set, Y be non empty set;

      let f be Function of X, Y;

      let g be X -valued Function;

      ( dom f) = X by Def1;

      then ( rng g) c= ( dom f);

      hence thesis by RELAT_1: 27;

    end;

    theorem :: FUNCT_2:124

    for X be non empty set, f be Function of X, X st for x be Element of X holds (f . x) = x holds f = ( id X);

    definition

      let O,E be set;

      mode Action of O,E is Function of O, ( Funcs (E,E));

    end

    theorem :: FUNCT_2:125

    for x be set, A be set holds for f,g be Function of {x}, A st (f . x) = (g . x) holds f = g

    proof

      let x be set, A be set;

      let f,g be Function of {x}, A such that

       A1: (f . x) = (g . x);

      now

        let y be object;

        assume y in {x};

        then y = x by TARSKI:def 1;

        hence (f . y) = (g . y) by A1;

      end;

      hence thesis;

    end;

    theorem :: FUNCT_2:126

    

     Th125: for A be set holds ( id A) in ( Funcs (A,A))

    proof

      let A be set;

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

      hence thesis by Def2;

    end;

    theorem :: FUNCT_2:127

    ( Funcs ( {} , {} )) = {( id {} )}

    proof

      hereby

        let f be object;

        assume f in ( Funcs ( {} , {} ));

        then

        reconsider f9 = f as Function of {} , {} by Th65;

        f9 = ( id {} );

        hence f in {( id {} )} by TARSKI:def 1;

      end;

      thus thesis by Th125, ZFMISC_1: 31;

    end;

    theorem :: FUNCT_2:128

    

     Th127: for A,B,C be set, f,g be Function st f in ( Funcs (A,B)) & g in ( Funcs (B,C)) holds (g * f) in ( Funcs (A,C))

    proof

      let A,B,C be set, f,g be Function;

      assume that

       A1: f in ( Funcs (A,B)) and

       A2: g in ( Funcs (B,C));

      

       A3: ex g9 be Function st g9 = g & ( dom g9) = B & ( rng g9) c= C by A2, Def2;

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

      then

       A4: ( rng (g * f)) c= C by A3;

      ex f9 be Function st f9 = f & ( dom f9) = A & ( rng f9) c= B by A1, Def2;

      then ( dom (g * f)) = A by A3, RELAT_1: 27;

      hence thesis by A4, Def2;

    end;

    theorem :: FUNCT_2:129

    for A,B,C be set st ( Funcs (A,B)) <> {} & ( Funcs (B,C)) <> {} holds ( Funcs (A,C)) <> {}

    proof

      let A,B,C be set such that

       A1: ( Funcs (A,B)) <> {} and

       A2: ( Funcs (B,C)) <> {} ;

      consider g be object such that

       A3: g in ( Funcs (B,C)) by A2, XBOOLE_0:def 1;

      ex f be object st f in ( Funcs (A,B)) by A1, XBOOLE_0:def 1;

      hence thesis by A3, Th127;

    end;

    theorem :: FUNCT_2:130

    for A be set holds {} is Function of A, {} by Def1, RELSET_1: 12;

    scheme :: FUNCT_2:sch11

    Lambda1 { X,Y() -> set , F( object) -> object } :

ex f be Function of X(), Y() st for x be set st x in X() holds (f . x) = F(x)

      provided

       A1: for x be set st x in X() holds F(x) in Y();

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

      

       A2: for x be object st x in X() holds ex y be object st y in Y() & P[x, y] by A1;

      consider f be Function of X(), Y() such that

       A3: for x be object st x in X() holds P[x, (f . x)] from FuncEx1( A2);

      take f;

      thus thesis by A3;

    end;