:: Group and Field Definitions
::  by J\'ozef Bia{\l}as
::
:: Received October 27, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, ZFMISC_1, XBOOLE_0, RELAT_1, TARSKI, BINOP_1, SUBSET_1,
      MCART_1, REALSET1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, DOMAIN_1, FUNCOP_1, FUNCT_3;
 constructors BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, RELSET_1, SETFAM_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, ZFMISC_1, FUNCT_2;
 requirements SUBSET;


begin

theorem :: REALSET1:1
  for X,x being set,
      F being Function of [:X,X:],X st
    x in [:X,X:] holds F.x in X;

definition
  let X be set;
  let F be BinOp of X;
  let A be Subset of X;
  attr A is F-binopclosed means
:: REALSET1:def 1
    for x being 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;
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;
  func R || A -> set equals
:: REALSET1:def 2
  R | [:A,A:];
end;

registration
  let R be Relation;
  let A be set;
  cluster R || A -> Relation-like;
end;

registration
  let R be Function;
  let A be set;
  cluster R || A -> Function-like;
end;

theorem :: REALSET1:2
  for X being set, F being BinOp of X,
      A being F-binopclosed Subset of X holds
    F || A is BinOp of A;

definition
  let X be set;
  let F be BinOp of X;
  let A be F-binopclosed Subset of X;
  redefine func F || A -> BinOp of A;
end;

::$CT 2

theorem :: REALSET1:5
  for X being set
  for A being Subset of X holds A is pr1(X,X)-binopclosed;

definition
::$CD
  let X be set;
  let A be Subset of X;
  let F be BinOp of X;
  attr F is A-subsetpreserving means
:: REALSET1:def 4
    for x being 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;
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
  for X being set,
      A being Subset of X,
      F being A-subsetpreserving BinOp of X holds
    F||A is BinOp of A;

definition
  let X be set;
  let A be Subset of X;
  let F be A-subsetpreserving BinOp of X;
  func F|||A -> BinOp of A equals
:: REALSET1:def 5
  F||A;
end;

theorem :: REALSET1:7
  for A being non trivial set
  for x being Element of A
  for F being (A \ {x})-subsetpreserving BinOp of A holds
    F||(A\{x}) is BinOp of A \ {x};

definition
::$CD
  let A be non trivial set;
  let x be Element of A;
  let F be (A \ {x})-subsetpreserving BinOp of A;
  func F!(A,x) -> BinOp of A\{x} equals
:: REALSET1:def 7
  F || (A\{x});
end;