:: Group and Field Definitions :: by J\'ozef Bia{\l}as :: :: Received October 27, 1989 :: Copyright (c) 1990-2018 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, BOOLE; begin theorem :: REALSET1:1 for X,x being set holds for F being Function of [:X,X:],X holds x in [:X,X:] implies F.x in X; definition let X be set; let F be BinOp of X; mode Preserv of F -> Subset of X means :: REALSET1:def 1 for x being set holds x in [: it,it:] implies F.x in it; 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 Preserv of F holds F ||A is BinOp of A; definition let X be set; let F be BinOp of X; let A be Preserv of F; redefine func F||A -> BinOp of A; end; definition let X be non trivial set; let F be BinOp of X; let x be Element of X; pred F is_Bin_Op_Preserv x means :: REALSET1:def 3 X\{x} is Preserv of F & F||X\{x} is BinOp of X\{x}; end; ::\$CT 2 theorem :: REALSET1:5 for X being set holds for A being Subset of X holds ex F being BinOp of X st for x being set holds x in [:A,A:] implies F.x in A; definition let X be set; let A be Subset of X; mode Presv of X,A -> BinOp of X means :: REALSET1:def 4 for x being set holds x in [:A, A:] implies it.x in A; end; theorem :: REALSET1:6 for X being set, A being Subset of X, F being Presv of X,A holds F||A is BinOp of A; definition let X be set; let A be Subset of X; let F be Presv of X,A; func F|||A -> BinOp of A equals :: REALSET1:def 5 F||A; end; definition let A be set; let x be Element of A; mode DnT of x,A -> BinOp of A means :: REALSET1:def 6 for y being set holds y in [:A\{x },A\{x}:] implies it.y in A\{x}; end; theorem :: REALSET1:7 for A being non trivial set holds for x being Element of A holds for F being DnT of x,A holds F||(A\{x}) is BinOp of A\{x}; definition let A be non trivial set; let x be Element of A; let F be DnT of x,A; func F!(A,x) -> BinOp of A\{x} equals :: REALSET1:def 7 F||(A\{x}); end;