environ
vocabularies HIDDEN, STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1, FUNCT_1, FINSEQ_1, RELAT_1, ORDINAL4, XBOOLE_0, ALGSTR_1, SETWISEO, FUNCOP_1, ZFMISC_1, GROUP_1, FINSEQOP, MESFUNC1, VECTSP_1, TARSKI, REALSET1, MCART_1, NUMBERS, BINOP_2, REAL_1, ARYTM_3, CARD_1, GR_CY_1, INT_1, PARTFUN1, FUNCT_2, MONOID_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XTUPLE_0, MCART_1, DOMAIN_1, BINOP_2, REALSET1, STRUCT_0, RELAT_1, FINSEQOP, FUNCT_1, FINSEQ_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_2, INT_1, GROUP_1, VECTSP_1, SETWISEO, FUNCOP_1, GR_CY_1, ALGSTR_0;
definitions TARSKI, BINOP_1, SETWISEO, FINSEQOP, GROUP_1, STRUCT_0, XBOOLE_0, VECTSP_1;
theorems TARSKI, NAT_1, INT_1, FINSEQ_1, BINOP_1, GROUP_1, SETWISEO, MCART_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCOP_1, PARTFUN1, GR_CY_1, GRFUNC_1, RELAT_1, RELSET_1, XCMPLX_1, NUMBERS, BINOP_2, ORDINAL1;
schemes FUNCT_2, BINOP_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, NUMBERS, BINOP_2, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0, GROUP_1, ALGSTR_0, GR_CY_1, XREAL_0, NAT_1;
constructors HIDDEN, RELAT_2, PARTFUN1, BINOP_1, SETWISEO, BINOP_2, FINSEQOP, REALSET1, VECTSP_2, GR_CY_1, RELSET_1, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities BINOP_1, STRUCT_0, REALSET1, ALGSTR_0, FUNCOP_1;
expansions TARSKI, BINOP_1, FINSEQOP, GROUP_1, VECTSP_1;
deffunc H1( 1-sorted ) -> set = the carrier of $1;
deffunc H2( multMagma ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the multF of $1;
Lm1:
for G being non empty multMagma holds
( G is associative iff for a, b, c being Element of G holds (a * b) * c = a * (b * c) )
;
Lm2:
for G being non empty multMagma holds
( G is invertible iff ( G is left-invertible & G is right-invertible ) )
by Th1;
Lm3:
for G being non empty multMagma holds
( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) )
Lm4:
for G being non empty multMagma st G is associative & G is invertible holds
G is Group-like
deffunc H3( multLoopStr ) -> Element of the carrier of $1 = 1. $1;
:: INT.Group is unital commutative associative cancelable invertible;