environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, ALGSTR_0, VECTSP_1, FUNCSDOM, BINOP_1, SUBSET_1, FUNCT_1, ZFMISC_1, XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1, GROUP_1, LATTICES, MESFUNC1, NAT_1, ARYTM_3, SUPINF_2, POLYNOM3, RLVECT_1, ARYTM_1, ALGSTR_1, FINSEQ_1, RFINSEQ, FINSEQ_3, XXREAL_0, ORDINAL4, PARTFUN1, CARD_3, REALSET1, TARSKI, UNIALG_2, RLSUB_1, SETFAM_1, POLYNOM1, ALGSEQ_1, POLYALG1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, REALSET1, STRUCT_0, ALGSTR_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSEQ_1, RFINSEQ, BINOP_1, NAT_D, GROUP_1, RLVECT_1, VFUNCT_1, VECTSP_1, NORMSP_1, POLYNOM1, ALGSTR_1, ALGSEQ_1, POLYNOM3, POLYNOM5, VECTSP_4, XXREAL_0;
definitions TARSKI, RLVECT_1, GROUP_1, VECTSP_1, ALGSTR_0;
theorems TARSKI, NAT_1, RLVECT_1, VECTSP_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, RFINSEQ, BINOP_1, POLYNOM1, POLYNOM3, ZFMISC_1, POLYNOM5, BINOM, RELAT_1, VECTSP_4, SETFAM_1, ALGSTR_1, XBOOLE_0, GROUP_1, XREAL_1, ORDINAL1, NORMSP_1, PARTFUN1, CARD_1, NAT_D;
schemes SUBSET_1, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, NAT_1, FINSEQ_1, REALSET1, STRUCT_0, VECTSP_1, FVSUM_1, POLYNOM3, POLYNOM5, BINOM, ORDINAL1, VFUNCT_1, FUNCT_2, RELAT_1;
constructors HIDDEN, BINOP_1, REALSET1, RFINSEQ, NAT_D, ALGSTR_1, VECTSP_4, POLYNOM3, POLYNOM5, REAL_1, RELSET_1, FUNCOP_1, FVSUM_1, VFUNCT_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities VECTSP_1, BINOP_1, REALSET1, STRUCT_0, ALGSTR_0;
expansions TARSKI, VECTSP_1;
definition
let L be non
empty doubleLoopStr ;
existence
ex b1 being non empty strict AlgebraStr over L st
( ( for x being set holds
( x in the carrier of b1 iff x is sequence of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b1
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b1 = 0_. L & 1. b1 = 1_. L )
uniqueness
for b1, b2 being non empty strict AlgebraStr over L st ( for x being set holds
( x in the carrier of b1 iff x is sequence of L ) ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b1
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b1
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b1 = 0_. L & 1. b1 = 1_. L & ( for x being set holds
( x in the carrier of b2 iff x is sequence of L ) ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b2
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b2
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b2 = 0_. L & 1. b2 = 1_. L holds
b1 = b2
end;
theorem
for
L being
1-sorted for
A,
B being
AlgebraStr over
L st
A is
Subalgebra of
B &
B is
Subalgebra of
A holds
AlgebraStr(# the
carrier of
A, the
addF of
A, the
multF of
A, the
ZeroF of
A, the
OneF of
A, the
lmult of
A #)
= AlgebraStr(# the
carrier of
B, the
addF of
B, the
multF of
B, the
ZeroF of
B, the
OneF of
B, the
lmult of
B #)
theorem Th14:
for
L being
1-sorted for
A,
B being
AlgebraStr over
L st
AlgebraStr(# the
carrier of
A, the
addF of
A, the
multF of
A, the
ZeroF of
A, the
OneF of
A, the
lmult of
A #)
= AlgebraStr(# the
carrier of
B, the
addF of
B, the
multF of
B, the
ZeroF of
B, the
OneF of
B, the
lmult of
B #) holds
A is
Subalgebra of
B