environ
vocabularies HIDDEN, FINSEQ_1, FUNCT_1, RELAT_1, CARD_3, TARSKI, BINOP_2, FINSET_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, ALGSTR_0, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, RLVECT_1, SUPINF_2, PRVECT_1, INT_3, XCMPLX_0, INT_1, INT_6, ZFMISC_1, VECTSP_1, FUNCSDOM, GROUP_6, GROUP_14, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, CARD_1, XTUPLE_0, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, CARD_3, FINSEQ_1, RVSUM_1, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, VECTSP_1, GR_CY_1, PRVECT_1, INT_3, INT_6, PRVECT_3, WSIERP_1, MOD_4;
definitions PRVECT_1;
theorems FUNCT_1, CARD_3, FUNCT_2, TARSKI, FINSEQ_2, XREAL_1, ORDINAL1, FINSEQ_1, FINSEQ_3, NAT_1, XBOOLE_0, RELAT_1, XXREAL_0, RLVECT_1, RVSUM_1, RELSET_1, ALGSTR_0, PRVECT_1, PRVECT_3, ZFMISC_1, SUBSET_1, CARD_1, INT_1, INT_3, INT_6, GR_CY_1, FINSEQ_5, NAT_D, PARTFUN3, CARD_2, STIRL2_1, WELLORD2, TOPGEN_5, MOD_4, VECTSP_1, XTUPLE_0, NDIFF_5;
schemes NAT_1, BINOP_1, FUNCT_2;
registrations XBOOLE_0, XREAL_0, STRUCT_0, ORDINAL1, NAT_1, FUNCT_2, CARD_1, CARD_3, XXREAL_0, RELSET_1, FINSEQ_1, MEMBERED, FUNCT_1, VALUED_0, ALGSTR_0, PRVECT_1, INT_1, INT_6, RLVECT_1, PRVECT_3, RELAT_1, SUBSET_1;
constructors HIDDEN, REALSET1, MONOID_0, PRALG_1, GROUP_4, GROUP_7, FUNCT_7, RELSET_1, REAL_1, SQUARE_1, RUSUB_4, ALGSTR_1, CARD_2, PRVECT_2, NAT_D, LOPBAN_1, XTUPLE_0, BINOP_2, FINSEQ_4, FINSEQOP, PRVECT_3, SETWISEO, BINOM, INT_3, INT_6, POLYNOM1, WELLORD2, WSIERP_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities FINSEQ_1, BINOP_1, ALGSTR_0, STRUCT_0, PRVECT_1, PRVECT_3, INT_3, CARD_1, ORDINAL1;
expansions ALGSTR_0;
theorem Th4:
for
G,
F being
AbGroup holds
( ( for
x being
set holds
(
x is
Element of
(product <*G,F*>) iff ex
x1 being
Element of
G ex
x2 being
Element of
F st
x = <*x1,x2*> ) ) & ( for
x,
y being
Element of
(product <*G,F*>) for
x1,
y1 being
Element of
G for
x2,
y2 being
Element of
F st
x = <*x1,x2*> &
y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> ) &
0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for
x being
Element of
(product <*G,F*>) for
x1 being
Element of
G for
x2 being
Element of
F st
x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) )
theorem
for
G,
F being
AbGroup holds
( ( for
x being
set holds
(
x is
Element of
[:G,F:] iff ex
x1 being
Element of
G ex
x2 being
Element of
F st
x = [x1,x2] ) ) & ( for
x,
y being
Element of
[:G,F:] for
x1,
y1 being
Element of
G for
x2,
y2 being
Element of
F st
x = [x1,x2] &
y = [y1,y2] holds
x + y = [(x1 + y1),(x2 + y2)] ) &
0. [:G,F:] = [(0. G),(0. F)] & ( for
x being
Element of
[:G,F:] for
x1 being
Element of
G for
x2 being
Element of
F st
x = [x1,x2] holds
- x = [(- x1),(- x2)] ) )
theorem Th11:
for
n being non
zero Nat holds
( not
addLoopStr(# the
carrier of
(INT.Ring n), the
addF of
(INT.Ring n), the
ZeroF of
(INT.Ring n) #) is
empty &
addLoopStr(# the
carrier of
(INT.Ring n), the
addF of
(INT.Ring n), the
ZeroF of
(INT.Ring n) #) is
Abelian &
addLoopStr(# the
carrier of
(INT.Ring n), the
addF of
(INT.Ring n), the
ZeroF of
(INT.Ring n) #) is
right_complementable &
addLoopStr(# the
carrier of
(INT.Ring n), the
addF of
(INT.Ring n), the
ZeroF of
(INT.Ring n) #) is
add-associative &
addLoopStr(# the
carrier of
(INT.Ring n), the
addF of
(INT.Ring n), the
ZeroF of
(INT.Ring n) #) is
right_zeroed )
Lm1:
for m being non zero Nat
for x being Integer holds x mod m in Segm m