funcop_1.miz

    begin

    reserve f,g,h for Function,

A for set;

    theorem :: FUNCOP_1:1



     Th1: ( delta A) = <:( id A), ( id A):>

    proof



      thus ( delta A) = (( id [:A, A:]) * ( delta A)) by FUNCT_2: 17

      .= ( [:( id A), ( id A):] * ( delta A)) by FUNCT_3: 69

      .= <:( id A), ( id A):> by FUNCT_3: 78;

    end;

    reserve F for Function,

B,x,y,y1,y2,z for set;

    definition

      let f;

      :: FUNCOP_1:def1

      func f ~ -> Function means

      : Def1: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (for y,z be object st (f . x) = [y, z] holds (it . x) = [z, y]) & ((f . x) = (it . x) or ex y,z be object st (f . x) = [y, z]);

      existence

      proof

        defpred P[ object, object] means (for y,z be object st (f . $1) = [y, z] holds $2 = [z, y]) & ((f . $1) = $2 or ex y,z be object st (f . $1) = [y, z]);

         A1:

        now

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

          now

            per cases ;

              case

               A2: ex y,z be object st (f . x) = [y, z];

              then

              consider y,z be object such that

               A3: (f . x) = [y, z];

              take y1 = [z, y];

              thus for y,z be object st (f . x) = [y, z] holds y1 = [z, y]

              proof

                let y9,z9 be object;

                assume

                 A4: (f . x) = [y9, z9];

                then z = z9 by A3, XTUPLE_0: 1;

                hence thesis by A3, A4, XTUPLE_0: 1;

              end;

              thus (f . x) = y1 or ex y,z be object st (f . x) = [y, z] by A2;

            end;

              case

               A5: not ex y,z be object st (f . x) = [y, z];

              reconsider y1 = (f . x) as set;

              take y1;

              thus (for y,z be object st (f . x) = [y, z] holds y1 = [z, y]) & ((f . x) = y1 or ex y,z be object st (f . x) = [y, z]) by A5;

            end;

          end;

          hence ex y be object st P[x, y];

        end;

         A6:

        now

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

          assume that

           A7: P[x, y1] and

           A8: P[x, y2];

          now

            per cases ;

              suppose ex y,z be object st (f . x) = [y, z];

              then

              consider y,z be object such that

               A9: (f . x) = [y, z];

              y1 = [z, y] by A7, A9;

              hence y1 = y2 by A8, A9;

            end;

              suppose not ex y,z be object st (f . x) = [y, z];

              hence y1 = y2 by A7, A8;

            end;

          end;

          hence y1 = y2;

        end;

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

      end;

      uniqueness

      proof

        defpred P[ Function] means for x be object st x in ( dom f) holds (for y,z be object st (f . x) = [y, z] holds ($1 . x) = [z, y]) & ((f . x) = ($1 . x) or ex y,z be object st (f . x) = [y, z]);

        let g1,g2 be Function such that

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

         A11: P[g1] and

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

         A13: P[g2];

        now

          let x be object;

          assume

           A14: x in ( dom f);

          now

            per cases ;

              suppose ex y,z be object st (f . x) = [y, z];

              then

              consider y,z be object such that

               A15: (f . x) = [y, z];

              (g1 . x) = [z, y] by A11, A14, A15;

              hence (g1 . x) = (g2 . x) by A13, A14, A15;

            end;

              suppose

               A16: not ex y,z be object st (f . x) = [y, z];

              then (g1 . x) = (f . x) by A11, A14;

              hence (g1 . x) = (g2 . x) by A13, A14, A16;

            end;

          end;

          hence (g1 . x) = (g2 . x);

        end;

        hence thesis by A10, A12;

      end;

      involutiveness

      proof

        let g,f be Function;

        assume that

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

         A18: for x be object st x in ( dom f) holds (for y,z be object st (f . x) = [y, z] holds (g . x) = [z, y]) & ((f . x) = (g . x) or ex y,z be object st (f . x) = [y, z]);

        thus ( dom f) = ( dom g) by A17;

        let x be object;

        assume

         A19: x in ( dom g);

        thus for y,z be object st (g . x) = [y, z] holds (f . x) = [z, y]

        proof

          let y,z be object such that

           A20: (g . x) = [y, z];

          per cases ;

            suppose ex z,y be object st (f . x) = [z, y];

            then

            consider y1,y2 be object such that

             A21: (f . x) = [y1, y2];



             A22: (g . x) = [y2, y1] by A17, A18, A19, A21;

            then y = y2 by A20, XTUPLE_0: 1;

            hence thesis by A20, A21, A22, XTUPLE_0: 1;

          end;

            suppose not ex z,y be object st (f . x) = [z, y];

            then (f . x) = (g . x) by A17, A18, A19;

            hence thesis by A17, A18, A19, A20;

          end;

        end;

        assume (g . x) <> (f . x);

        then

        consider y,z be object such that

         A23: (f . x) = [y, z] by A17, A18, A19;

        take z, y;

        thus thesis by A17, A18, A19, A23;

      end;

    end

    theorem :: FUNCOP_1:2



     Th2: <:f, g:> = ( <:g, f:> ~ )

    proof



       A1: ( dom <:f, g:>) = (( dom g) /\ ( dom f)) by FUNCT_3:def 7

      .= ( dom <:g, f:>) by FUNCT_3:def 7;

       A2:

      now

        let x be object;

        assume

         A3: x in ( dom <:f, g:>);

        then

         A4: ( <:g, f:> . x) = [(g . x), (f . x)] by A1, FUNCT_3:def 7;



        thus ( <:f, g:> . x) = [(f . x), (g . x)] by A3, FUNCT_3:def 7

        .= (( <:g, f:> ~ ) . x) by A1, A3, A4, Def1;

      end;

      ( dom <:f, g:>) = ( dom ( <:g, f:> ~ )) by A1, Def1;

      hence thesis by A2;

    end;

    theorem :: FUNCOP_1:3



     Th3: ((f | A) ~ ) = ((f ~ ) | A)

    proof



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

      .= (( dom (f ~ )) /\ A) by Def1

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

       A2:

      now

        let x be object such that

         A3: x in ( dom ((f ~ ) | A));



         A4: ( dom (f | A)) c= ( dom f) by RELAT_1: 60;

        now

          per cases ;

            suppose ex y,z be object st ((f | A) . x) = [y, z];

            then

            consider y,z be object such that

             A5: ((f | A) . x) = [y, z];



             A6: (f . x) = [y, z] by A1, A3, A5, FUNCT_1: 47;



            thus (((f | A) ~ ) . x) = [z, y] by A1, A3, A5, Def1

            .= ((f ~ ) . x) by A1, A3, A4, A6, Def1

            .= (((f ~ ) | A) . x) by A3, FUNCT_1: 47;

          end;

            suppose

             A7: not ex y,z be object st ((f | A) . x) = [y, z];



             A8: ((f | A) . x) = (f . x) by A1, A3, FUNCT_1: 47;

            (((f | A) ~ ) . x) = ((f | A) . x) by A1, A3, A7, Def1;



            hence (((f | A) ~ ) . x) = ((f ~ ) . x) by A1, A3, A4, A7, A8, Def1

            .= (((f ~ ) | A) . x) by A3, FUNCT_1: 47;

          end;

        end;

        hence (((f | A) ~ ) . x) = (((f ~ ) | A) . x);

      end;

      ( dom ((f | A) ~ )) = ( dom (f | A)) by Def1;

      hence thesis by A1, A2;

    end;

    theorem :: FUNCOP_1:4

    (( delta A) ~ ) = ( delta A)

    proof



      thus (( delta A) ~ ) = ( <:( id A), ( id A):> ~ ) by Th1

      .= <:( id A), ( id A):> by Th2

      .= ( delta A) by Th1;

    end;

    theorem :: FUNCOP_1:5



     Th5: ( <:f, g:> | A) = <:(f | A), g:>

    proof



       A1: ( dom ( <:f, g:> | A)) = (( dom <:f, g:>) /\ A) by RELAT_1: 61

      .= ((( dom f) /\ ( dom g)) /\ A) by FUNCT_3:def 7

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

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

      now



         A2: ( dom ( <:f, g:> | A)) c= ( dom <:f, g:>) by RELAT_1: 60;

        let x be object such that

         A3: x in ( dom ( <:f, g:> | A));



         A4: x in ( dom (f | A)) by A1, A3, XBOOLE_0:def 4;



        thus (( <:f, g:> | A) . x) = ( <:f, g:> . x) by A3, FUNCT_1: 47

        .= [(f . x), (g . x)] by A3, A2, FUNCT_3:def 7

        .= [((f | A) . x), (g . x)] by A4, FUNCT_1: 47;

      end;

      hence thesis by A1, FUNCT_3:def 7;

    end;

    theorem :: FUNCOP_1:6



     Th6: ( <:f, g:> | A) = <:f, (g | A):>

    proof



      thus ( <:f, g:> | A) = (( <:g, f:> ~ ) | A) by Th2

      .= (( <:g, f:> | A) ~ ) by Th3

      .= ( <:(g | A), f:> ~ ) by Th5

      .= <:f, (g | A):> by Th2;

    end;

    definition

      let A be set, z be object;

      :: FUNCOP_1:def2

      func A --> z -> set equals [:A, {z}:];

      coherence ;

    end

    registration

      let A be set, z be object;

      cluster (A --> z) -> Function-like Relation-like;

      coherence

      proof

        thus (A --> z) is Function-like

        proof

          let x,y1,y2 be object;

          assume that

           A1: [x, y1] in (A --> z) and

           A2: [x, y2] in (A --> z);

          y1 in {z} by A1, ZFMISC_1: 87;

          then

           A3: y1 = z by TARSKI:def 1;

          y2 in {z} by A2, ZFMISC_1: 87;

          hence thesis by A3, TARSKI:def 1;

        end;

        thus for x be object st x in (A --> z) holds ex y1,y2 be object st [y1, y2] = x by RELAT_1:def 1;

      end;

    end

    reserve x,z for object;

    theorem :: FUNCOP_1:7



     Th7: x in A implies ((A --> z) . x) = z

    proof

      assume

       A1: x in A;

      z in {z} by TARSKI:def 1;

      then [x, z] in (A --> z) by A1, ZFMISC_1: 87;

      hence thesis by FUNCT_1: 1;

    end;

    registration

      let A be non empty set, x be object, a be Element of A;

      reduce ((A --> x) . a) to x;

      reducibility by Th7;

    end

    theorem :: FUNCOP_1:8

    A <> {} implies ( rng (A --> x)) = {x} by RELAT_1: 160;

    theorem :: FUNCOP_1:9



     Th9: ( rng f) = {x} implies f = (( dom f) --> x)

    proof

      assume

       A1: ( rng f) = {x};

      then ( dom f) <> {} by RELAT_1: 42;

      then ( dom (( dom f) --> x)) = ( dom f) & ( rng (( dom f) --> x)) = {x} by RELAT_1: 160;

      hence thesis by A1, FUNCT_1: 7;

    end;

    registration

      let x be object;

      cluster ( {} --> x) -> empty;

      coherence by ZFMISC_1: 90;

    end

    registration

      let x be object;

      let A be empty set;

      cluster (A --> x) -> empty;

      coherence ;

    end

    registration

      let x be object;

      let A be non empty set;

      cluster (A --> x) -> non empty;

      coherence ;

    end

    theorem :: FUNCOP_1:10

    ( dom ( {} --> x)) = {} & ( rng ( {} --> x)) = {} ;

    theorem :: FUNCOP_1:11



     Th11: (for z st z in ( dom f) holds (f . z) = x) implies f = (( dom f) --> x)

    proof

      assume

       A1: for z st z in ( dom f) holds (f . z) = x;

      now

        per cases ;

          suppose

           A2: ( dom f) = {} ;

          thus thesis by A2;

        end;

          suppose

           A3: ( dom f) <> {} ;

          set z = the Element of ( dom f);

          now

            let y be object;

            thus y in {x} implies ex y1 be object st y1 in ( dom f) & y = (f . y1)

            proof

              assume y in {x};

              then y = x by TARSKI:def 1;

              then (f . z) = y by A1, A3;

              hence thesis by A3;

            end;

            assume ex y1 be object st y1 in ( dom f) & y = (f . y1);

            then y = x by A1;

            hence y in {x} by TARSKI:def 1;

          end;

          then ( rng f) = {x} by FUNCT_1:def 3;

          hence thesis by Th9;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCOP_1:12



     Th12: ((A --> x) | B) = ((A /\ B) --> x)

    proof



       A1: A = {} or A <> {} ;



       A2: (A /\ B) = {} or (A /\ B) <> {} ;



       A3: ( dom ((A --> x) | B)) = (( dom (A --> x)) /\ B) by RELAT_1: 61

      .= (A /\ B) by A1, RELAT_1: 160

      .= ( dom ((A /\ B) --> x)) by A2, RELAT_1: 160;

      now

        let z be object such that

         A4: z in ( dom ((A /\ B) --> x));

        (A /\ B) = {} or (A /\ B) <> {} ;

        then

         A5: z in (A /\ B) by A4, RELAT_1: 160;

        then

         A6: z in A by XBOOLE_0:def 4;



        thus (((A --> x) | B) . z) = ((A --> x) . z) by A3, A4, FUNCT_1: 47

        .= x by A6, Th7

        .= (((A /\ B) --> x) . z) by A5, Th7;

      end;

      hence thesis by A3;

    end;

    theorem :: FUNCOP_1:13



     Th13: ( dom (A --> x)) = A & ( rng (A --> x)) c= {x}

    proof

      now

        per cases ;

          suppose

           A1: A = {} ;

          thus thesis by A1;

        end;

          suppose A <> {} ;

          hence thesis by RELAT_1: 160;

        end;

      end;

      hence thesis;

    end;

    registration

      let X be set, a be object;

      reduce ( dom (X --> a)) to X;

      reducibility by Th13;

    end

    registration

      let D be set;

      cluster (D --> {} ) -> empty-yielding;

      coherence by Th13;

    end

    theorem :: FUNCOP_1:14



     Th14: x in B implies ((A --> x) " B) = A

    proof

      assume

       A1: x in B;

      now

        per cases ;

          suppose

           A2: A = {} ;

          thus thesis by A2;

        end;

          suppose A <> {} ;

          then

           A3: ( rng (A --> x)) = {x} by RELAT_1: 160;

           {x} c= B by A1, ZFMISC_1: 31;

          then ( {x} /\ B) = {x} by XBOOLE_1: 28;



          hence ((A --> x) " B) = ((A --> x) " {x}) by A3, RELAT_1: 133

          .= ( dom (A --> x)) by A3, RELAT_1: 134

          .= A;

        end;

      end;

      hence thesis;

    end;

    theorem :: FUNCOP_1:15

    ((A --> x) " {x}) = A

    proof

      x in {x} by TARSKI:def 1;

      hence thesis by Th14;

    end;

    theorem :: FUNCOP_1:16

     not x in B implies ((A --> x) " B) = {}

    proof

      assume

       A1: not x in B;

      ( rng (A --> x)) c= {x} by Th13;

      then ( rng (A --> x)) misses B by A1, XBOOLE_1: 63, ZFMISC_1: 50;

      hence thesis by RELAT_1: 138;

    end;

    theorem :: FUNCOP_1:17

    x in ( dom h) implies (h * (A --> x)) = (A --> (h . x))

    proof

      assume

       A1: x in ( dom h);

       A2:

      now

        let z be object;

        assume

         A3: z in ( dom (h * (A --> x)));

        then z in ( dom (A --> x)) by FUNCT_1: 11;

        then

         A4: z in A;



        thus ((h * (A --> x)) . z) = (h . ((A --> x) . z)) by A3, FUNCT_1: 12

        .= (h . x) by A4, Th7

        .= ((A --> (h . x)) . z) by A4, Th7;

      end;

      ( dom (h * (A --> x))) = ((A --> x) " ( dom h)) by RELAT_1: 147

      .= A by A1, Th14

      .= ( dom (A --> (h . x)));

      hence thesis by A2;

    end;

    theorem :: FUNCOP_1:18

    A <> {} & x in ( dom h) implies ( dom (h * (A --> x))) <> {}

    proof

      assume that

       A1: A <> {} and

       A2: x in ( dom h);

      set y = the Element of A;



       A3: y in ( dom (A --> x)) by A1;

      ((A --> x) . y) = x by A1, Th7;

      hence thesis by A2, A3, FUNCT_1: 11;

    end;

    theorem :: FUNCOP_1:19

    ((A --> x) * h) = ((h " A) --> x)

    proof



       A1: ( dom ((A --> x) * h)) = (h " ( dom (A --> x))) by RELAT_1: 147

      .= (h " A);

      now

        let z be object;

        assume

         A3: z in ( dom ((A --> x) * h));

        then (h . z) in ( dom (A --> x)) by FUNCT_1: 11;

        then

         A4: (h . z) in A;



        thus (((A --> x) * h) . z) = ((A --> x) . (h . z)) by A3, FUNCT_1: 12

        .= x by A4, Th7

        .= (((h " A) --> x) . z) by A1, A3, Th7;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCOP_1:20

    ((A --> [x, y]) ~ ) = (A --> [y, x])

    proof



       A1: ( dom ((A --> [x, y]) ~ )) = ( dom (A --> [x, y])) by Def1;

      then

       A2: ( dom ((A --> [x, y]) ~ )) = A;

      now

        let z be object;

        assume

         A4: z in ( dom ((A --> [x, y]) ~ ));

        then ((A --> [x, y]) . z) = [x, y] by A2, Th7;



        hence (((A --> [x, y]) ~ ) . z) = [y, x] by A1, A4, Def1

        .= ((A --> [y, x]) . z) by A2, A4, Th7;

      end;

      hence thesis by A2;

    end;

    definition

      let F, f, g;

      :: FUNCOP_1:def3

      func F .: (f,g) -> set equals (F * <:f, g:>);

      correctness ;

    end

    registration

      let F, f, g;

      cluster (F .: (f,g)) -> Function-like Relation-like;

      coherence ;

    end



     Lm1: x in ( dom (F * <:f, g:>)) implies ((F * <:f, g:>) . x) = (F . ((f . x),(g . x)))

    proof

      assume

       A1: x in ( dom (F * <:f, g:>));

      then

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



      thus ((F * <:f, g:>) . x) = (F . ( <:f, g:> . x)) by A1, FUNCT_1: 12

      .= (F . ((f . x),(g . x))) by A2, FUNCT_3:def 7;

    end;

    theorem :: FUNCOP_1:21

    for h st ( dom h) = ( dom (F .: (f,g))) & for z be set st z in ( dom (F .: (f,g))) holds (h . z) = (F . ((f . z),(g . z))) holds h = (F .: (f,g))

    proof

      let h;

      assume that

       A1: ( dom h) = ( dom (F .: (f,g))) and

       A2: for z be set st z in ( dom (F .: (f,g))) holds (h . z) = (F . ((f . z),(g . z)));

      now

        let z be object;

        assume

         A3: z in ( dom (F .: (f,g)));



        hence (h . z) = (F . ((f . z),(g . z))) by A2

        .= ((F .: (f,g)) . z) by A3, Lm1;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCOP_1:22

    x in ( dom (F .: (f,g))) implies ((F .: (f,g)) . x) = (F . ((f . x),(g . x))) by Lm1;

    theorem :: FUNCOP_1:23



     Th23: (f | A) = (g | A) implies ((F .: (f,h)) | A) = ((F .: (g,h)) | A)

    proof

      assume

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



      thus ((F .: (f,h)) | A) = (F * ( <:f, h:> | A)) by RELAT_1: 83

      .= (F * <:(f | A), h:>) by Th5

      .= (F * ( <:g, h:> | A)) by A1, Th5

      .= ((F .: (g,h)) | A) by RELAT_1: 83;

    end;

    theorem :: FUNCOP_1:24



     Th24: (f | A) = (g | A) implies ((F .: (h,f)) | A) = ((F .: (h,g)) | A)

    proof

      assume

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



      thus ((F .: (h,f)) | A) = (F * ( <:h, f:> | A)) by RELAT_1: 83

      .= (F * <:h, (f | A):>) by Th6

      .= (F * ( <:h, g:> | A)) by A1, Th6

      .= ((F .: (h,g)) | A) by RELAT_1: 83;

    end;

    theorem :: FUNCOP_1:25



     Th25: ((F .: (f,g)) * h) = (F .: ((f * h),(g * h)))

    proof



      thus ((F .: (f,g)) * h) = (F * ( <:f, g:> * h)) by RELAT_1: 36

      .= (F .: ((f * h),(g * h))) by FUNCT_3: 55;

    end;

    definition

      let F, f, x;

      :: FUNCOP_1:def4

      func F [:] (f,x) -> set equals (F * <:f, (( dom f) --> x):>);

      correctness ;

    end

    registration

      let F, f, x;

      cluster (F [:] (f,x)) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: FUNCOP_1:26

    (F [:] (f,x)) = (F .: (f,(( dom f) --> x)));

    theorem :: FUNCOP_1:27



     Th27: x in ( dom (F [:] (f,z))) implies ((F [:] (f,z)) . x) = (F . ((f . x),z))

    proof



       A1: ( dom <:f, (( dom f) --> z):>) = (( dom f) /\ ( dom (( dom f) --> z))) by FUNCT_3:def 7;

      assume

       A2: x in ( dom (F [:] (f,z)));

      then x in ( dom <:f, (( dom f) --> z):>) by FUNCT_1: 11;

      then

       A3: x in ( dom f) by A1;



      thus ((F [:] (f,z)) . x) = (F . ((f . x),((( dom f) --> z) . x))) by A2, Lm1

      .= (F . ((f . x),z)) by A3, Th7;

    end;

    theorem :: FUNCOP_1:28

    (f | A) = (g | A) implies ((F [:] (f,x)) | A) = ((F [:] (g,x)) | A)

    proof

      assume

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

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

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



      then

       A2: ((( dom f) --> x) | A) = ((( dom g) /\ A) --> x) by Th12

      .= ((( dom g) --> x) | A) by Th12;



      thus ((F [:] (f,x)) | A) = ((F .: (f,(( dom f) --> x))) | A)

      .= ((F .: (g,(( dom f) --> x))) | A) by A1, Th23

      .= ((F .: (g,(( dom g) --> x))) | A) by A2, Th24

      .= ((F [:] (g,x)) | A);

    end;

    theorem :: FUNCOP_1:29



     Th29: ((F [:] (f,x)) * h) = (F [:] ((f * h),x))

    proof

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

      then

       A2: ( dom ((( dom f) --> x) * h)) = ( dom (f * h)) by RELAT_1: 163;

       A3:

      now

        let z;

        assume

         A4: z in ( dom ((( dom f) --> x) * h));

        then

         A5: (h . z) in ( dom (( dom f) --> x)) by FUNCT_1: 11;



        thus (((( dom f) --> x) * h) . z) = ((( dom f) --> x) . (h . z)) by A4, FUNCT_1: 12

        .= x by A5, Th7;

      end;



      thus ((F [:] (f,x)) * h) = ((F .: (f,(( dom f) --> x))) * h)

      .= (F .: ((f * h),((( dom f) --> x) * h))) by Th25

      .= (F [:] ((f * h),x)) by A2, A3, Th11;

    end;

    theorem :: FUNCOP_1:30

    ((F [:] (f,x)) * ( id A)) = (F [:] ((f | A),x))

    proof



      thus ((F [:] (f,x)) * ( id A)) = (F [:] ((f * ( id A)),x)) by Th29

      .= (F [:] ((f | A),x)) by RELAT_1: 65;

    end;

    definition

      let F, x, g;

      :: FUNCOP_1:def5

      func F [;] (x,g) -> set equals (F * <:(( dom g) --> x), g:>);

      correctness ;

    end

    registration

      let F, x, g;

      cluster (F [;] (x,g)) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: FUNCOP_1:31

    (F [;] (x,g)) = (F .: ((( dom g) --> x),g));

    theorem :: FUNCOP_1:32



     Th32: x in ( dom (F [;] (z,f))) implies ((F [;] (z,f)) . x) = (F . (z,(f . x)))

    proof



       A1: ( dom <:(( dom f) --> z), f:>) = (( dom (( dom f) --> z)) /\ ( dom f)) by FUNCT_3:def 7;

      assume

       A2: x in ( dom (F [;] (z,f)));

      then x in ( dom <:(( dom f) --> z), f:>) by FUNCT_1: 11;

      then

       A3: x in ( dom f) by A1;



      thus ((F [;] (z,f)) . x) = (F . (((( dom f) --> z) . x),(f . x))) by A2, Lm1

      .= (F . (z,(f . x))) by A3, Th7;

    end;

    theorem :: FUNCOP_1:33

    (f | A) = (g | A) implies ((F [;] (x,f)) | A) = ((F [;] (x,g)) | A)

    proof

      assume

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

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

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



      then

       A2: ((( dom f) --> x) | A) = ((( dom g) /\ A) --> x) by Th12

      .= ((( dom g) --> x) | A) by Th12;



      thus ((F [;] (x,f)) | A) = ((F .: ((( dom f) --> x),f)) | A)

      .= ((F .: ((( dom f) --> x),g)) | A) by A1, Th24

      .= ((F .: ((( dom g) --> x),g)) | A) by A2, Th23

      .= ((F [;] (x,g)) | A);

    end;

    theorem :: FUNCOP_1:34



     Th34: ((F [;] (x,f)) * h) = (F [;] (x,(f * h)))

    proof

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

      then

       A2: ( dom ((( dom f) --> x) * h)) = ( dom (f * h)) by RELAT_1: 163;

       A3:

      now

        let z;

        assume

         A4: z in ( dom ((( dom f) --> x) * h));

        then

         A5: (h . z) in ( dom (( dom f) --> x)) by FUNCT_1: 11;



        thus (((( dom f) --> x) * h) . z) = ((( dom f) --> x) . (h . z)) by A4, FUNCT_1: 12

        .= x by A5, Th7;

      end;



      thus ((F [;] (x,f)) * h) = ((F .: ((( dom f) --> x),f)) * h)

      .= (F .: (((( dom f) --> x) * h),(f * h))) by Th25

      .= (F [;] (x,(f * h))) by A2, A3, Th11;

    end;

    theorem :: FUNCOP_1:35

    ((F [;] (x,f)) * ( id A)) = (F [;] (x,(f | A)))

    proof



      thus ((F [;] (x,f)) * ( id A)) = (F [;] (x,(f * ( id A)))) by Th34

      .= (F [;] (x,(f | A))) by RELAT_1: 65;

    end;

    reserve X for non empty set,

Y for set,

F for BinOp of X,

f,g,h for Function of Y, X,

x,x1,x2 for Element of X;

    theorem :: FUNCOP_1:36



     Th36: (F .: (f,g)) is Function of Y, X

    proof

      (F * <:f, g:>) is Function of Y, X;

      hence thesis;

    end;

    definition

      let X be non empty set, Z be set;

      let F be BinOp of X, f,g be Function of Z, X;

      :: original: .:

      redefine

      func F .: (f,g) -> Function of Z, X ;

      coherence by Th36;

    end

    reserve Y for non empty set,

F for BinOp of X,

f,g,h for Function of Y, X,

x,x1,x2 for Element of X;

    theorem :: FUNCOP_1:37



     Th37: for z be Element of Y holds ((F .: (f,g)) . z) = (F . ((f . z),(g . z)))

    proof

      let z be Element of Y;

      ( dom (F .: (f,g))) = Y by FUNCT_2:def 1;

      hence thesis by Lm1;

    end;

    theorem :: FUNCOP_1:38



     Th38: for h be Function of Y, X holds (for z be Element of Y holds (h . z) = (F . ((f . z),(g . z)))) implies h = (F .: (f,g))

    proof

      let h be Function of Y, X;

      assume

       A1: for z be Element of Y holds (h . z) = (F . ((f . z),(g . z)));

      now

        let z be Element of Y;



        thus (h . z) = (F . ((f . z),(g . z))) by A1

        .= ((F .: (f,g)) . z) by Th37;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUNCOP_1:39

    for g be Function of X, X holds ((F .: (( id X),g)) * f) = (F .: (f,(g * f)))

    proof

      let g be Function of X, X;



      thus ((F .: (( id X),g)) * f) = (F .: ((( id X) * f),(g * f))) by Th25

      .= (F .: (f,(g * f))) by FUNCT_2: 17;

    end;

    theorem :: FUNCOP_1:40

    for g be Function of X, X holds ((F .: (g,( id X))) * f) = (F .: ((g * f),f))

    proof

      let g be Function of X, X;



      thus ((F .: (g,( id X))) * f) = (F .: ((g * f),(( id X) * f))) by Th25

      .= (F .: ((g * f),f)) by FUNCT_2: 17;

    end;

    theorem :: FUNCOP_1:41

    ((F .: (( id X),( id X))) * f) = (F .: (f,f))

    proof



      thus ((F .: (( id X),( id X))) * f) = (F .: ((( id X) * f),(( id X) * f))) by Th25

      .= (F .: ((( id X) * f),f)) by FUNCT_2: 17

      .= (F .: (f,f)) by FUNCT_2: 17;

    end;

    theorem :: FUNCOP_1:42

    for g be Function of X, X holds ((F .: (( id X),g)) . x) = (F . (x,(g . x)))

    proof

      let g be Function of X, X;



      thus ((F .: (( id X),g)) . x) = (F . ((( id X) . x),(g . x))) by Th37

      .= (F . (x,(g . x)));

    end;

    theorem :: FUNCOP_1:43

    for g be Function of X, X holds ((F .: (g,( id X))) . x) = (F . ((g . x),x))

    proof

      let g be Function of X, X;



      thus ((F .: (g,( id X))) . x) = (F . ((g . x),(( id X) . x))) by Th37

      .= (F . ((g . x),x));

    end;

    theorem :: FUNCOP_1:44

    ((F .: (( id X),( id X))) . x) = (F . (x,x))

    proof



      thus ((F .: (( id X),( id X))) . x) = (F . ((( id X) . x),(( id X) . x))) by Th37

      .= (F . ((( id X) . x),x))

      .= (F . (x,x));

    end;

    theorem :: FUNCOP_1:45



     Th45: x in B implies (A --> x) is Function of A, B

    proof



       A1: ( rng (A --> x)) c= {x} by Th13;



       A2: ( dom (A --> x)) = A;

      assume

       A3: x in B;

      then {x} c= B by ZFMISC_1: 31;

      then ( rng (A --> x)) c= B by A1;

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

    end;

    definition

      let I be set, i be object;

      :: original: -->

      redefine

      func I --> i -> Function of I, {i} ;

      coherence

      proof

        ( dom (I --> i)) = I & ( rng (I --> i)) c= {i} by Th13;

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

      end;

    end

    definition

      let B be non empty set, A be set, b be Element of B;

      :: original: -->

      redefine

      func A --> b -> Function of A, B ;

      coherence by Th45;

    end

    theorem :: FUNCOP_1:46

    (A --> x) is Function of A, X;

    reserve Y for set,

F for BinOp of X,

f,g,h for Function of Y, X,

x,x1,x2 for Element of X;

    theorem :: FUNCOP_1:47



     Th47: (F [:] (f,x)) is Function of Y, X

    proof

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

      then

      reconsider g = (( dom f) --> x) as Function of Y, X;

      (F * <:f, g:>) is Function of Y, X;

      hence thesis;

    end;

    definition

      let X be non empty set, Z be set;

      let F be BinOp of X, f be Function of Z, X, x be Element of X;

      :: original: [:]

      redefine

      func F [:] (f,x) -> Function of Z, X ;

      coherence by Th47;

    end

    reserve Y for non empty set,

F for BinOp of X,

f,g,h for Function of Y, X,

x,x1,x2 for Element of X;

    theorem :: FUNCOP_1:48



     Th48: for y be Element of Y holds ((F [:] (f,x)) . y) = (F . ((f . y),x))

    proof

      let y be Element of Y;

      ( dom (F [:] (f,x))) = Y by FUNCT_2:def 1;

      hence thesis by Th27;

    end;

    theorem :: FUNCOP_1:49



     Th49: (for y be Element of Y holds (g . y) = (F . ((f . y),x))) implies g = (F [:] (f,x))

    proof

      assume

       A1: for y be Element of Y holds (g . y) = (F . ((f . y),x));

      now

        let y be Element of Y;



        thus (g . y) = (F . ((f . y),x)) by A1

        .= ((F [:] (f,x)) . y) by Th48;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: FUNCOP_1:50

    ((F [:] (( id X),x)) * f) = (F [:] (f,x))

    proof



      thus ((F [:] (( id X),x)) * f) = (F [:] ((( id X) * f),x)) by Th29

      .= (F [:] (f,x)) by FUNCT_2: 17;

    end;

    theorem :: FUNCOP_1:51

    ((F [:] (( id X),x)) . x) = (F . (x,x))

    proof



      thus ((F [:] (( id X),x)) . x) = (F . ((( id X) . x),x)) by Th48

      .= (F . (x,x));

    end;

    reserve Y for set,

F for BinOp of X,

f,g,h for Function of Y, X,

x,x1,x2 for Element of X;

    theorem :: FUNCOP_1:52



     Th52: (F [;] (x,g)) is Function of Y, X

    proof

      ( dom g) = Y by FUNCT_2:def 1;

      then

      reconsider f = (( dom g) --> x) as Function of Y, X;

      (F * <:f, g:>) is Function of Y, X;

      hence thesis;

    end;

    definition

      let X be non empty set, Z be set;

      let F be BinOp of X, x be Element of X;

      let g be Function of Z, X;

      :: original: [;]

      redefine

      func F [;] (x,g) -> Function of Z, X ;

      coherence by Th52;

    end

    reserve Y for non empty set,

F for BinOp of X,

f,g,h for Function of Y, X,

x,x1,x2 for Element of X;

    theorem :: FUNCOP_1:53



     Th53: for y be Element of Y holds ((F [;] (x,f)) . y) = (F . (x,(f . y)))

    proof

      let y be Element of Y;

      ( dom (F [;] (x,f))) = Y by FUNCT_2:def 1;

      hence thesis by Th32;

    end;

    theorem :: FUNCOP_1:54



     Th54: (for y be Element of Y holds (g . y) = (F . (x,(f . y)))) implies g = (F [;] (x,f))

    proof

      assume

       A1: for y be Element of Y holds (g . y) = (F . (x,(f . y)));

      now

        let y be Element of Y;



        thus (g . y) = (F . (x,(f . y))) by A1

        .= ((F [;] (x,f)) . y) by Th53;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    reserve Y for set,

F for BinOp of X,

f,g,h for Function of Y, X,

x,x1,x2 for Element of X;

    theorem :: FUNCOP_1:55

    ((F [;] (x,( id X))) * f) = (F [;] (x,f))

    proof



      thus ((F [;] (x,( id X))) * f) = (F [;] (x,(( id X) * f))) by Th34

      .= (F [;] (x,f)) by FUNCT_2: 17;

    end;

    theorem :: FUNCOP_1:56

    ((F [;] (x,( id X))) . x) = (F . (x,x))

    proof



      thus ((F [;] (x,( id X))) . x) = (F . (x,(( id X) . x))) by Th53

      .= (F . (x,x));

    end;

    theorem :: FUNCOP_1:57

    for X,Y,Z be non empty set holds for f be Function of X, [:Y, Z:] holds for x be Element of X holds ((f ~ ) . x) = [((f . x) `2 ), ((f . x) `1 )]

    proof

      let X,Y,Z be non empty set;

      let f be Function of X, [:Y, Z:];

      let x be Element of X;

      x in X;

      then

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

      (f . x) = [((f . x) `1 ), ((f . x) `2 )] by MCART_1: 22;

      hence thesis by A1, Def1;

    end;

    definition

      let X,Y,Z be non empty set;

      let f be Function of X, [:Y, Z:];

      :: original: rng

      redefine

      func rng f -> Relation of Y, Z ;

      coherence by RELAT_1:def 19;

    end

    definition

      let X,Y,Z be non empty set;

      let f be Function of X, [:Y, Z:];

      :: original: ~

      redefine

      func f ~ -> Function of X, [:Z, Y:] ;

      coherence

      proof



         A1: ( rng (f ~ )) c= [:Z, Y:]

        proof

          let x be object;

          assume x in ( rng (f ~ ));

          then

          consider y be object such that

           A2: y in ( dom (f ~ )) and

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



           A4: y in ( dom f) by A2, Def1;

          then

          reconsider y as Element of X;



           A5: (f . y) = [((f . y) `1 ), ((f . y) `2 )] by MCART_1: 21;

          then ((f ~ ) . y) = [((f . y) `2 ), ((f . y) `1 )] by A4, Def1;

          hence thesis by A3, A5, ZFMISC_1: 88;

        end;

        X = ( dom f) by FUNCT_2:def 1

        .= ( dom (f ~ )) by Def1;

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

      end;

    end

    theorem :: FUNCOP_1:58

    for X,Y,Z be non empty set holds for f be Function of X, [:Y, Z:] holds ( rng (f ~ )) = (( rng f) ~ )

    proof

      let X,Y,Z be non empty set;

      let f be Function of X, [:Y, Z:];

      let x,y be object;

      thus [x, y] in ( rng (f ~ )) implies [x, y] in (( rng f) ~ )

      proof

        assume [x, y] in ( rng (f ~ ));

        then

        consider z be object such that

         A1: z in ( dom (f ~ )) and

         A2: [x, y] = ((f ~ ) . z) by FUNCT_1:def 3;



         A3: z in ( dom f) by A1, Def1;

        (f . z) = (((f ~ ) ~ ) . z)

        .= [y, x] by A1, A2, Def1;

        then [y, x] in ( rng f) by A3, FUNCT_1:def 3;

        hence thesis by RELAT_1:def 7;

      end;

      assume [x, y] in (( rng f) ~ );

      then [y, x] in ( rng f) by RELAT_1:def 7;

      then

      consider z be object such that

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

      z in ( dom (f ~ )) & ((f ~ ) . z) = [x, y] by A4, Def1;

      hence thesis by FUNCT_1:def 3;

    end;

    reserve y for Element of Y;

    theorem :: FUNCOP_1:59

    F is associative implies (F [:] ((F [;] (x1,f)),x2)) = (F [;] (x1,(F [:] (f,x2))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x3 = (f . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F [:] ((F [;] (x1,f)),x2)) . y) = (F . (((F [;] (x1,f)) . y),x2)) by A2, Th48

          .= (F . ((F . (x1,x3)),x2)) by A2, Th53

          .= (F . (x1,(F . (x3,x2)))) by A1

          .= (F . (x1,((F [:] (f,x2)) . y))) by A2, Th48;

        end;

        hence thesis by A2, Th54;

      end;

    end;

    theorem :: FUNCOP_1:60

    F is associative implies (F .: ((F [:] (f,x)),g)) = (F .: (f,(F [;] (x,g))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x1 = (f . y), x2 = (g . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F .: ((F [:] (f,x)),g)) . y) = (F . (((F [:] (f,x)) . y),(g . y))) by A2, Th37

          .= (F . ((F . (x1,x)),x2)) by A2, Th48

          .= (F . (x1,(F . (x,x2)))) by A1

          .= (F . ((f . y),((F [;] (x,g)) . y))) by A2, Th53;

        end;

        hence thesis by A2, Th38;

      end;

    end;

    theorem :: FUNCOP_1:61

    F is associative implies (F .: ((F .: (f,g)),h)) = (F .: (f,(F .: (g,h))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x1 = (f . y), x2 = (g . y), x3 = (h . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F .: ((F .: (f,g)),h)) . y) = (F . (((F .: (f,g)) . y),(h . y))) by A2, Th37

          .= (F . ((F . ((f . y),(g . y))),(h . y))) by A2, Th37

          .= (F . (x1,(F . (x2,x3)))) by A1

          .= (F . ((f . y),((F .: (g,h)) . y))) by A2, Th37;

        end;

        hence thesis by A2, Th38;

      end;

    end;

    theorem :: FUNCOP_1:62

    F is associative implies (F [;] ((F . (x1,x2)),f)) = (F [;] (x1,(F [;] (x2,f))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x3 = (f . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F [;] ((F . (x1,x2)),f)) . y) = (F . ((F . (x1,x2)),(f . y))) by A2, Th53

          .= (F . (x1,(F . (x2,x3)))) by A1

          .= (F . (x1,((F [;] (x2,f)) . y))) by A2, Th53;

        end;

        hence thesis by A2, Th54;

      end;

    end;

    theorem :: FUNCOP_1:63

    F is associative implies (F [:] (f,(F . (x1,x2)))) = (F [:] ((F [:] (f,x1)),x2))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x3 = (f . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F [:] (f,(F . (x1,x2)))) . y) = (F . ((f . y),(F . (x1,x2)))) by A2, Th48

          .= (F . ((F . (x3,x1)),x2)) by A1

          .= (F . (((F [:] (f,x1)) . y),x2)) by A2, Th48;

        end;

        hence thesis by A2, Th49;

      end;

    end;

    theorem :: FUNCOP_1:64

    F is commutative implies (F [;] (x,f)) = (F [:] (f,x))

    proof

      assume

       A1: F is commutative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x1 = (f . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F [;] (x,f)) . y) = (F . (x,x1)) by A2, Th53

          .= (F . ((f . y),x)) by A1;

        end;

        hence thesis by A2, Th49;

      end;

    end;

    theorem :: FUNCOP_1:65

    F is commutative implies (F .: (f,g)) = (F .: (g,f))

    proof

      assume

       A1: F is commutative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x1 = (f . y), x2 = (g . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F .: (f,g)) . y) = (F . (x1,x2)) by A2, Th37

          .= (F . ((g . y),(f . y))) by A1;

        end;

        hence thesis by A2, Th38;

      end;

    end;

    theorem :: FUNCOP_1:66

    F is idempotent implies (F .: (f,f)) = f

    proof

      assume

       A1: F is idempotent;

      per cases ;

        suppose

         A2: Y = {} ;



        hence (F .: (f,f)) = {}

        .= f by A2;

      end;

        suppose

         A3: Y <> {} ;

        now

          let y;

          reconsider x = (f . y) as Element of X by A3, FUNCT_2: 5;



          thus (f . y) = (F . (x,x)) by A1

          .= (F . ((f . y),(f . y)));

        end;

        hence thesis by A3, Th38;

      end;

    end;

    reserve Y for non empty set,

F for BinOp of X,

f for Function of Y, X,

x for Element of X,

y for Element of Y;

    theorem :: FUNCOP_1:67

    F is idempotent implies ((F [;] ((f . y),f)) . y) = (f . y)

    proof

      assume

       A1: F is idempotent;



      thus ((F [;] ((f . y),f)) . y) = (F . ((f . y),(f . y))) by Th53

      .= (f . y) by A1;

    end;

    theorem :: FUNCOP_1:68

    F is idempotent implies ((F [:] (f,(f . y))) . y) = (f . y)

    proof

      assume

       A1: F is idempotent;



      thus ((F [:] (f,(f . y))) . y) = (F . ((f . y),(f . y))) by Th48

      .= (f . y) by A1;

    end;

    theorem :: FUNCOP_1:69

    for F,f,g be Function st [:( rng f), ( rng g):] c= ( dom F) holds ( dom (F .: (f,g))) = (( dom f) /\ ( dom g))

    proof

      let F,f,g be Function such that

       A1: [:( rng f), ( rng g):] c= ( dom F);

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



      hence ( dom (F .: (f,g))) = ( dom <:f, g:>) by A1, RELAT_1: 27, XBOOLE_1: 1

      .= (( dom f) /\ ( dom g)) by FUNCT_3:def 7;

    end;

    definition

      let IT be Function;

      :: FUNCOP_1:def6

      attr IT is Function-yielding means

      : Def6: for x be object st x in ( dom IT) holds (IT . x) is Function;

    end

    registration

      cluster Function-yielding for Function;

      existence

      proof

        take ( the set --> the Function);

        let x be object;

        thus thesis;

      end;

    end

    registration

      let B be Function-yielding Function, j be object;

      cluster (B . j) -> Function-like Relation-like;

      coherence

      proof

        per cases ;

          suppose j in ( dom B);

          hence thesis by Def6;

        end;

          suppose not j in ( dom B);

          hence thesis by FUNCT_1:def 2;

        end;

      end;

    end

    registration

      let F be Function-yielding Function, f be Function;

      cluster (F * f) -> Function-yielding;

      coherence

      proof

        thus (F * f) is Function-yielding

        proof

          let x be object;

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

          then ((F * f) . x) = (F . (f . x)) by FUNCT_1: 12;

          hence thesis;

        end;

      end;

    end

    registration

      let B;

      let c be non empty set;

      cluster (B --> c) -> non-empty;

      coherence

      proof

         not {} in ( rng (B --> c)) by TARSKI:def 1;

        hence thesis;

      end;

    end

    theorem :: FUNCOP_1:70

    (( [:X, Y:] --> z) . (x,y)) = z by Th7, ZFMISC_1: 87;

    reserve a,b,c for set;

    definition

      let a,b,c be object;

      :: FUNCOP_1:def7

      func (a,b) .--> c -> Function equals ( { [a, b]} --> c);

      coherence ;

    end

    theorem :: FUNCOP_1:71

    for a,b,c be object holds (((a,b) .--> c) . (a,b)) = c

    proof

      let a,b,c be object;

       [a, b] in { [a, b]} by TARSKI:def 1;

      hence thesis by Th7;

    end;

    definition

      let x,y,a,b be object;

      :: FUNCOP_1:def8

      func IFEQ (x,y,a,b) -> object equals

      : Def8: a if x = y

      otherwise b;

      correctness ;

    end

    definition

      let x,y be object;

      let a,b be set;

      :: original: IFEQ

      redefine

      func IFEQ (x,y,a,b) -> set ;

      correctness

      proof

        x = y or x <> y;

        hence thesis by Def8;

      end;

    end

    definition

      let D be set;

      let x,y be object, a,b be Element of D;

      :: original: IFEQ

      redefine

      func IFEQ (x,y,a,b) -> Element of D ;

      coherence

      proof

        x = y or x <> y;

        hence thesis by Def8;

      end;

    end

    definition

      let x,y be object;

      :: FUNCOP_1:def9

      func x .--> y -> set equals ( {x} --> y);

      coherence ;

    end

    registration

      let x,y be object;

      cluster (x .--> y) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let x,y be object;

      cluster (x .--> y) -> one-to-one;

      coherence

      proof

        let x1,x2 be object;

        set f = (x .--> y);

        assume that

         A1: x1 in ( dom f) and

         A2: x2 in ( dom f);

        x1 = x by A1, TARSKI:def 1;

        hence thesis by A2, TARSKI:def 1;

      end;

    end

    theorem :: FUNCOP_1:72



     Th72: for x,y be object holds ((x .--> y) . x) = y

    proof

      let x,y be object;

      x in {x} by TARSKI:def 1;

      hence thesis by Th7;

    end;

    theorem :: FUNCOP_1:73

    for a,b be object, f be Function holds (a .--> b) c= f iff a in ( dom f) & (f . a) = b

    proof

      let a,b be object, f be Function;



       A1: ( dom (a .--> b)) = {a};



       A2: a in ( dom (a .--> b)) by TARSKI:def 1;

      hereby

        assume

         A3: (a .--> b) c= f;

        then {a} c= ( dom f) by A1, GRFUNC_1: 2;

        hence a in ( dom f) by ZFMISC_1: 31;



        thus (f . a) = ((a .--> b) . a) by A2, A3, GRFUNC_1: 2

        .= b by Th72;

      end;

      assume that

       A4: a in ( dom f) and

       A5: (f . a) = b;

       A6:

      now

        let x be object;

        assume x in ( dom (a .--> b));

        then x = a by TARSKI:def 1;

        hence ((a .--> b) . x) = (f . x) by A5, Th72;

      end;

      ( dom (a .--> b)) c= ( dom f) by A4, ZFMISC_1: 31;

      hence thesis by A6, GRFUNC_1: 2;

    end;

    notation

      let o,m,r be object;

      synonym (o,m) :-> r for (o,m) .--> r;

    end



     Lm2: for o,m,r be object holds ((o,m) :-> r) is Function of [: {o}, {m}:], {r}

    proof

      let o,m,r be object;

       [: {o}, {m}:] = { [o, m]} by ZFMISC_1: 29;

      hence thesis;

    end;

    definition

      let o,m,r be object;

      :: original: :->

      redefine

      :: FUNCOP_1:def10

      func (o,m) :-> r -> Function of [: {o}, {m}:], {r} means not contradiction;

      coherence by Lm2;

      compatibility

      proof

        let f be Function of [: {o}, {m}:], {r};

        ((o,m) .--> r) is Function of [: {o}, {m}:], {r} by Lm2;

        hence thesis by FUNCT_2: 51;

      end;

    end

    reserve x,y,z for object;

    theorem :: FUNCOP_1:74

    x in ( dom (x .--> y)) by TARSKI:def 1;

    theorem :: FUNCOP_1:75

    z in ( dom (x .--> y)) implies z = x by TARSKI:def 1;

    theorem :: FUNCOP_1:76

     not x in A implies ((x .--> y) | A) = {}

    proof

      assume not x in A;

      then ( dom (x .--> y)) misses A by ZFMISC_1: 50;

      hence thesis by RELAT_1: 66;

    end;

    notation

      let x,y be object;

      synonym x :-> y for x .--> y;

    end

    definition

      let m,o be object;

      :: original: :->

      redefine

      func m :-> o -> Function of {m}, {o} ;

      coherence ;

    end

    theorem :: FUNCOP_1:77

    for x be Element of {a} holds for y be Element of {b} holds (((a,b) :-> c) . (x,y)) = c by TARSKI:def 1;

    registration

      let f be Function-yielding Function, C be set;

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

      coherence

      proof

        let i be object;

        (f . i) is Function;

        hence thesis by FUNCT_1: 47;

      end;

    end

    registration

      let A be set;

      let f be Function;

      cluster (A --> f) -> Function-yielding;

      coherence ;

    end

    registration

      let X be set, a be object;

      cluster (X --> a) -> constant;

      coherence

      proof

        let x,y be object;

        assume that

         A1: x in ( dom (X --> a)) and

         A2: y in ( dom (X --> a));



        thus ((X --> a) . x) = a by A1, Th7

        .= ((X --> a) . y) by A2, Th7;

      end;

    end

    registration

      cluster non empty constant for Function;

      existence

      proof

        take ( { {} } --> {} );

        thus thesis;

      end;

      let X be set, Y be non empty set;

      cluster constant for Function of X, Y;

      existence

      proof

        take (X --> the Element of Y);

        thus thesis;

      end;

    end

    registration

      let f be constant Function, X be set;

      cluster (f | X) -> constant;

      coherence

      proof

        let x,y be object;



         A1: ( dom (f | X)) c= ( dom f) by RELAT_1: 60;

        assume that

         A2: x in ( dom (f | X)) and

         A3: y in ( dom (f | X));



        thus ((f | X) . x) = (f . x) by A2, FUNCT_1: 47

        .= (f . y) by A1, A2, A3, FUNCT_1:def 10

        .= ((f | X) . y) by A3, FUNCT_1: 47;

      end;

    end

    theorem :: FUNCOP_1:78

    for f be non empty constant Function holds ex y st for x st x in ( dom f) holds (f . x) = y

    proof

      let f be non empty constant Function;

      consider y be object such that

       A1: y in ( rng f) by XBOOLE_0:def 1;

      take y;

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

      hence thesis by FUNCT_1:def 10;

    end;

    theorem :: FUNCOP_1:79

    for X be non empty set, x be set holds ( the_value_of (X --> x)) = x

    proof

      let X be non empty set, x be set;

      set f = (X --> x);

      ex i be set st i in ( dom f) & ( the_value_of f) = (f . i) by FUNCT_1:def 12;

      hence thesis by Th7;

    end;

    theorem :: FUNCOP_1:80

    for f be constant Function holds f = (( dom f) --> ( the_value_of f))

    proof

      let f be constant Function;

      thus ( dom (( dom f) --> ( the_value_of f))) = ( dom f);

      let x be object;

      assume

       A1: x in ( dom f);

      then f <> {} & ((( dom f) --> ( the_value_of f)) . x) = ( the_value_of f) by Th7;

      hence thesis by A1, FUNCT_1:def 12;

    end;

    registration

      let X be set, Y be non empty set;

      cluster total for PartFunc of X, Y;

      existence

      proof

        consider y be object such that

         A1: y in Y by XBOOLE_0:def 1;

        reconsider y as Element of Y by A1;

        take (X --> y);

        thus thesis;

      end;

    end

    registration

      let I be set, A be object;

      cluster (I --> A) -> I -defined;

      coherence ;

    end

    registration

      let I,A be object;

      cluster (I .--> A) -> {I} -defined;

      coherence ;

    end

    theorem :: FUNCOP_1:81

    ((A --> x) .: B) c= {x};

    registration

      let I be set, f be Function;

      cluster (I .--> f) -> Function-yielding;

      coherence ;

    end

    registration

      let I be set;

      cluster total for I -defined non-empty Function;

      existence

      proof

        take (I --> { {} });

        thus thesis;

      end;

    end

    theorem :: FUNCOP_1:82



     Th82: (x .--> y) is_isomorphism_of ( { [x, x]}, { [y, y]})

    proof

      set F = (x .--> y);

      set R = { [x, x]};

      set S = { [y, y]};



       A1: ( field R) = {x} by RELAT_1: 173;

      hence ( dom F) = ( field R);

      ( field S) = {y} by RELAT_1: 173;

      hence ( rng F) = ( field S) by RELAT_1: 160;

      thus F is one-to-one;

      let a,b be object;

      hereby

        assume [a, b] in R;

        then [a, b] = [x, x] by TARSKI:def 1;

        then

         A2: a = x & b = x by XTUPLE_0: 1;

        hence a in ( field R) & b in ( field R) by A1, TARSKI:def 1;

        (F . x) = y by Th72;

        hence [(F . a), (F . b)] in S by A2, TARSKI:def 1;

      end;

      assume a in ( field R) & b in ( field R);

      then a = x & b = x by A1, TARSKI:def 1;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: FUNCOP_1:83

    ( { [x, x]}, { [y, y]}) are_isomorphic

    proof

      take (x .--> y);

      thus thesis by Th82;

    end;

    registration

      let I be set, A be object;

      cluster (I --> A) -> total;

      coherence ;

    end

    theorem :: FUNCOP_1:84

    for f be Function st x in ( dom f) holds (x .--> (f . x)) c= f

    proof

      let f be Function;

      assume x in ( dom f);

      then { [x, (f . x)]} c= f by ZFMISC_1: 31, FUNCT_1: 1;

      hence thesis by ZFMISC_1: 29;

    end;

    registration

      let A be non empty set;

      let x be set, i be Element of A;

      cluster (x .--> i) -> A -valued;

      coherence

      proof

        ( rng (x .--> i)) = {i} by RELAT_1: 160;

        hence ( rng (x .--> i)) c= A by ZFMISC_1: 31;

      end;

    end

    reserve Y for set,

f,g for Function of Y, X,

x for Element of X,

y for Element of Y;

    theorem :: FUNCOP_1:85

    F is associative implies (F .: ((F [;] (x,f)),g)) = (F [;] (x,(F .: (f,g))))

    proof

      assume

       A1: F is associative;

      per cases ;

        suppose Y = {} ;

        hence thesis;

      end;

        suppose

         A2: Y <> {} ;

        now

          let y;

          reconsider x1 = (f . y), x2 = (g . y) as Element of X by A2, FUNCT_2: 5;



          thus ((F [;] (x,(F .: (f,g)))) . y) = (F . (x,((F .: (f,g)) . y))) by A2, Th53

          .= (F . (x,(F . (x1,x2)))) by A2, Th37

          .= (F . ((F . (x,x1)),x2)) by A1

          .= (F . (((F [;] (x,f)) . y),(g . y))) by A2, Th53;

        end;

        hence thesis by A2, Th38;

      end;

    end;

    registration

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

      cluster (A --> x) -> B -valued;

      coherence ;

    end

    registration

      let A be non empty set, x be Element of A, y be object;

      cluster (x .--> y) -> A -defined;

      coherence by ZFMISC_1: 31;

    end

    theorem :: FUNCOP_1:86

    for x,y,A be set st x in A holds ((x .--> y) | A) = (x .--> y)

    proof

      let x,y,A be set;

      assume x in A;

      then ( dom (x .--> y)) c= A by ZFMISC_1: 31;

      hence thesis by RELAT_1: 68;

    end;

    registration

      let Y be functional set;

      cluster Y -valued -> Function-yielding for Function;

      coherence ;

    end

    definition

      let IT be Function;

      :: FUNCOP_1:def11

      attr IT is Relation-yielding means for x be set st x in ( dom IT) holds (IT . x) is Relation;

    end

    registration

      cluster Function-yielding -> Relation-yielding for Function;

      coherence ;

    end

    registration

      cluster empty -> Function-yielding for Function;

      coherence ;

    end

    theorem :: FUNCOP_1:87

    for X,Y be set, x,y be object holds (X --> x) tolerates (Y --> y) iff x = y or X misses Y

    proof

      let X,Y be set;

      let x,y be object;

      set f = (X --> x), g = (Y --> y);

      thus f tolerates g implies x = y or X misses Y

      proof

        assume that

         A3: for z be object st z in (( dom f) /\ ( dom g)) holds (f . z) = (g . z) and

         A4: x <> y;

        assume X meets Y;

        then

        consider z be object such that

         A5: z in X and

         A6: z in Y by XBOOLE_0: 3;



         A7: (f . z) = x by A5, Th7;



         A8: (g . z) = y by A6, Th7;

        z in (X /\ Y) by A5, A6, XBOOLE_0:def 4;

        hence thesis by A3, A4, A7, A8;

      end;

      assume

       A9: x = y or X misses Y;

      let z be object;

      assume

       A10: z in (( dom f) /\ ( dom g));

      then

       A11: z in Y;



       A12: z in X by A10, XBOOLE_0:def 4;

      then (f . z) = x by Th7;

      hence thesis by A9, A12, A11, Th7, XBOOLE_0: 3;

    end;

    reserve x,y,z,A for set;

    theorem :: FUNCOP_1:88



     Th88: ( rng (x .--> y)) = {y}

    proof

      ( dom (x .--> y)) = {x};



      hence ( rng (x .--> y)) = {((x .--> y) . x)} by FUNCT_1: 4

      .= {y} by Th72;

    end;

    theorem :: FUNCOP_1:89

    z in A implies ((A --> x) * (y .--> z)) = (y .--> x)

    proof

      assume

       A1: z in A;



       A2: ( dom (y .--> z)) = {y}

      .= ( dom (y .--> x));

      ( rng (y .--> z)) = {z} by Th88;

      then ( rng (y .--> z)) c= ( dom (A --> x)) by A1, ZFMISC_1: 31;

      hence ( dom ((A --> x) * (y .--> z))) = ( dom (y .--> x)) by A2, RELAT_1: 27;

      let e be object;

      assume

       A3: e in ( dom ((A --> x) * (y .--> z)));



      thus (((A --> x) * (y .--> z)) . e) = ((A --> x) . ((y .--> z) . e)) by A3, FUNCT_1: 12

      .= ((A --> x) . z) by A3, Th7

      .= x by A1, Th7

      .= ((y .--> x) . e) by A3, Th7;

    end;

    registration

      let f be Function-yielding Function;

      let a,b be object;

      cluster (f . (a,b)) -> Function-like Relation-like;

      coherence ;

    end

    registration

      let Y be set;

      let X,Z be non empty set;

      cluster -> Function-yielding for Function of X, ( Funcs (Y,Z));

      coherence ;

    end