environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, ORDINAL4, NAT_1, XXREAL_0, ARYTM_3, PRE_POLY, CARD_1, FUNCOP_1, PARTFUN1, SUBSET_1, ARYTM_1, FUNCT_4, ORDINAL1, PBOOLE, FINSET_1, ORDERS_1, VECTSP_1, ZFMISC_1, ALGSTR_0, POLYNOM2, GROUP_1, POLYNOM1, SUPINF_2, RLVECT_1, ALGSEQ_1, LATTICES, POLYNOM3, STRUCT_0, CARD_3, CARD_FIL, QUOFIELD, MSSUBFAM, IDEAL_1, PRELAMB, BINOP_1, FUNCT_2, HILBASIS, RECDEF_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, PBOOLE, RELAT_1, FINSET_1, FUNCT_1, PARTFUN1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, RELSET_1, FUNCT_2, FUNCOP_1, FINSEQ_1, FUNCT_4, BINOP_1, XXREAL_2, MCART_1, FINSEQOP, FINSEQ_2, FUNCT_7, PRE_POLY, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, VFUNCT_1, GROUP_1, VECTSP_1, NORMSP_1, POLYNOM1, POLYNOM2, POLYNOM3, ALGSEQ_1, NAT_D, IDEAL_1, TOPS_2, GRCAT_1, WSIERP_1, ORDERS_1, GROUP_6, QUOFIELD, RECDEF_1, MATRLIN;
definitions TARSKI, IDEAL_1, VECTSP_1, GROUP_6;
theorems TARSKI, ZFMISC_1, RLVECT_1, FUNCT_1, FUNCT_2, POLYNOM1, NAT_1, AXIOMS, FVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, POLYNOM3, FUNCOP_1, ALGSEQ_1, INT_1, FUNCT_7, IDEAL_1, POLYNOM4, FUNCT_4, RELAT_1, CARD_1, MATRLIN, CARD_3, ORDINAL1, WAYBEL_1, ORDERS_1, FINSET_1, FINSEQOP, POLYNOM2, TOPS_2, FINSEQ_5, GROUP_1, XBOOLE_0, XBOOLE_1, RLVECT_2, XREAL_1, XXREAL_0, NORMSP_1, PARTFUN1, XXREAL_2, NAT_D, XREAL_0, PRE_POLY, PBOOLE, AFINSQ_1;
schemes NAT_1, RECDEF_1, FUNCT_1, FUNCT_2, FINSEQ_2, FUNCT_7;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, CARD_5, PRE_CIRC, STRUCT_0, VECTSP_1, ALGSTR_1, WAYBEL_2, GCD_1, PRE_POLY, POLYNOM1, POLYNOM2, POLYNOM3, IDEAL_1, VALUED_0, ALGSTR_0, XXREAL_2, VFUNCT_1, FUNCT_2, RELSET_1, MOD_4, RINGCAT1;
constructors HIDDEN, FINSEQOP, NAT_D, REAL_1, WSIERP_1, TOPS_2, ALGSEQ_1, GRCAT_1, GROUP_6, MATRIX_1, TRIANG_1, QUOFIELD, POLYNOM2, POLYNOM3, IDEAL_1, RECDEF_1, XXREAL_2, DOMAIN_1, BINARITH, RELSET_1, FUNCT_7, MATRLIN, VFUNCT_1, FUNCT_4, MOD_4, RINGCAT1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FUNCOP_1, POLYNOM3, CARD_1, STRUCT_0, ORDINAL1;
expansions TARSKI, FUNCT_2, IDEAL_1, VECTSP_1, GROUP_6;
theorem Th4:
for
i,
j being
set for
b1,
b2 being
bag of
j for
b19,
b29 being
bag of
i st
b19 = b1 | i &
b29 = b2 | i &
b1 divides b2 holds
b19 divides b29
theorem Th5:
for
i,
j being
set for
b1,
b2 being
bag of
j for
b19,
b29 being
bag of
i st
b19 = b1 | i &
b29 = b2 | i holds
(
(b1 -' b2) | i = b19 -' b29 &
(b1 + b2) | i = b19 + b29 )
definition
let R be non
trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ;
let n be
Nat;
existence
ex b1 being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st
for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b1 . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
uniqueness
for b1, b2 being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st ( for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b1 . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ) & ( for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b2 . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) ) holds
b1 = b2
end;
definition
let R be non
trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ;
let n be
Nat;
existence
ex b1 being Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) st
for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b1 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
uniqueness
for b1, b2 being Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) st ( for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b1 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ) & ( for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b2 . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ) holds
b1 = b2
end;