realset1.miz

    begin

    theorem :: REALSET1:1



     Th1: for X,x be set, F be Function of [:X, X:], X st x in [:X, X:] holds (F . x) in X

    proof

      let X,x be set;

      let F be Function of [:X, X:], X;



       A1: ( dom F) = [:X, X:] by PARTFUN1:def 2;

      assume x in [:X, X:];

      then ( rng F) c= X & (F . x) in ( rng F) by A1, FUNCT_1:def 3, RELAT_1:def 19;

      hence thesis;

    end;

    definition

      let X be set;

      let F be BinOp of X;

      let A be Subset of X;

      :: REALSET1:def1

      attr A is F -binopclosed means

      : Def1: for x be set holds x in [:A, A:] implies (F . x) in A;

    end

    registration

      let X be set;

      let F be BinOp of X;

      cluster F -binopclosed for Subset of X;

      existence

      proof

        X c= X;

        then

        reconsider Z = X as Subset of X;

        take Z;

        thus thesis by Th1;

      end;

    end

    definition

      let X be set;

      let F be BinOp of X;

      mode Preserv of F is F -binopclosed Subset of X;

    end

    definition

      let R be Relation;

      let A be set;

      :: REALSET1:def2

      func R || A -> set equals (R | [:A, A:]);

      coherence ;

    end

    registration

      let R be Relation;

      let A be set;

      cluster (R || A) -> Relation-like;

      coherence ;

    end

    registration

      let R be Function;

      let A be set;

      cluster (R || A) -> Function-like;

      coherence ;

    end

    theorem :: REALSET1:2



     Th2: for X be set, F be BinOp of X, A be F -binopclosed Subset of X holds (F || A) is BinOp of A

    proof

      let X be set, F be BinOp of X, A be F -binopclosed Subset of X;

      ( dom F) = [:X, X:] by PARTFUN1:def 2;

      then

       A1: ( dom (F || A)) = [:A, A:] by RELAT_1: 62, ZFMISC_1: 96;

      for x be object holds x in [:A, A:] implies ((F || A) . x) in A

      proof

        let x be object;

        assume

         A2: x in [:A, A:];

        then ((F || A) . x) = (F . x) by A1, FUNCT_1: 47;

        hence thesis by A2, Def1;

      end;

      hence thesis by A1, FUNCT_2: 3;

    end;

    definition

      let X be set;

      let F be BinOp of X;

      let A be F -binopclosed Subset of X;

      :: original: ||

      redefine

      func F || A -> BinOp of A ;

      coherence by Th2;

    end

    ::$Canceled

    theorem :: REALSET1:5



     Th3: for X be set holds for A be Subset of X holds A is ( pr1 (X,X)) -binopclosed

    proof

      let X be set;

      let A be Subset of X;

      set S = ( pr1 (X,X));

      for x be set holds x in [:A, A:] implies (S . x) in A

      proof

        let x be set;

        assume x in [:A, A:];

        then

        consider p,q be object such that

         A1: p in A & q in A and

         A2: x = [p, q] by ZFMISC_1:def 2;

        (S . x) = (S . (p,q)) by A2;

        hence thesis by A1, FUNCT_3:def 4;

      end;

      hence thesis;

    end;

    definition

      ::$Canceled

      let X be set;

      let A be Subset of X;

      let F be BinOp of X;

      :: REALSET1:def4

      attr F is A -subsetpreserving means

      : Def4: for x be set holds x in [:A, A:] implies (F . x) in A;

    end

    registration

      let X be set;

      let A be Subset of X;

      cluster A -subsetpreserving for BinOp of X;

      existence

      proof

        take F = ( pr1 (X,X));

        A is F -binopclosed by Th3;

        hence thesis;

      end;

    end

    definition

      let X be set;

      let A be Subset of X;

      mode Presv of X,A is A -subsetpreserving BinOp of X;

    end

    theorem :: REALSET1:6



     Th4: for X be set, A be Subset of X, F be A -subsetpreserving BinOp of X holds (F || A) is BinOp of A

    proof

      let X be set;

      let A be Subset of X;

      let F be A -subsetpreserving BinOp of X;

      ( dom F) = [:X, X:] by PARTFUN1:def 2;

      then

       A1: ( dom (F || A)) = [:A, A:] by RELAT_1: 62, ZFMISC_1: 96;

      for x be object holds x in [:A, A:] implies ((F || A) . x) in A

      proof

        let x be object;

        assume

         A2: x in [:A, A:];

        then ((F || A) . x) = (F . x) by A1, FUNCT_1: 47;

        hence thesis by A2, Def4;

      end;

      hence thesis by A1, FUNCT_2: 3;

    end;

    definition

      let X be set;

      let A be Subset of X;

      let F be A -subsetpreserving BinOp of X;

      :: REALSET1:def5

      func F ||| A -> BinOp of A equals (F || A);

      coherence by Th4;

    end

    theorem :: REALSET1:7



     Th5: for A be non trivial set holds for x be Element of A holds for F be (A \ {x}) -subsetpreserving BinOp of A holds (F || (A \ {x})) is BinOp of (A \ {x})

    proof

      let A be non trivial set;

      let x be Element of A;

      let F be (A \ {x}) -subsetpreserving BinOp of A;

      ( dom F) = [:A, A:] by FUNCT_2:def 1;

      then

       A1: ( dom (F || (A \ {x}))) = [:(A \ {x}), (A \ {x}):] by RELAT_1: 62, ZFMISC_1: 96;

      for y be object holds y in [:(A \ {x}), (A \ {x}):] implies ((F || (A \ {x})) . y) in (A \ {x})

      proof

        let y be object;

        assume

         A2: y in [:(A \ {x}), (A \ {x}):];

        then ((F || (A \ {x})) . y) = (F . y) by A1, FUNCT_1: 47;

        hence thesis by A2, Def4;

      end;

      hence thesis by A1, FUNCT_2: 3;

    end;

    definition

      ::$Canceled

      let A be non trivial set;

      let x be Element of A;

      let F be (A \ {x}) -subsetpreserving BinOp of A;

      :: REALSET1:def7

      func F ! (A,x) -> BinOp of (A \ {x}) equals (F || (A \ {x}));

      coherence by Th5;

    end