environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, ARYTM_3, NEWTON, CARD_1, XXREAL_0, PREPOWER, NAT_1, RELAT_1, ARYTM_1, INT_1, FUNCT_2, XBOOLE_0, FUNCT_1, TARSKI, FUNCT_4, FUNCOP_1, FINSET_1, FINSEQ_1, PARTFUN1, CARD_3, ORDINAL4, EQREL_1, ZFMISC_1, GROUP_1, GROUP_5, STRUCT_0, GROUP_2, GROUP_3, VECTSP_1, RLVECT_5, RLVECT_3, RLSUB_1, SUPINF_2, FINSEQ_2, RLVECT_2, VALUED_1, VECTSP_2, ALGSTR_0, REALSET1, MESFUNC1, BINOP_1, RLVECT_1, LATTICES, UNIROOTS, COMPLFLD, POLYNOM2, COMPLEX1, WEDDWITT, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1, XXREAL_0, XREAL_0, INT_1, INT_2, NAT_1, NAT_D, FINSET_1, BINOP_1, RELAT_1, REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, RVSUM_1, COMPLFLD, POLYNOM4, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, GROUP_2, PREPOWER, FUNCT_4, UNIROOTS, VECTSP_6, VECTSP_7, GROUP_3, GROUP_5, MATRLIN, VECTSP_9, EQREL_1, FUNCOP_1, VECTSP_4, WSIERP_1, NEWTON;
definitions TARSKI, VECTSP_1, FUNCT_1, RLVECT_1, GROUP_1, ALGSTR_0;
theorems GROUP_1, CARD_1, FINSEQ_1, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, VECTSP_1, PREPOWER, COMPLFLD, INT_1, RVSUM_1, FINSEQ_3, FINSEQ_2, FINSEQ_4, INT_2, ABSVALUE, WSIERP_1, NAT_2, PEPIN, FUNCT_7, RLVECT_1, NEWTON, FINSET_1, FUNCOP_1, VECTSP_2, CARD_2, MATRLIN, WELLORD2, FUNCT_5, AFINSQ_1, FUNCT_4, GROUP_2, VECTSP_4, VECTSP_7, VECTSP_9, EQREL_1, GROUP_3, FRAENKEL, VECTSP_6, GROUP_5, UNIROOTS, XCMPLX_0, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, STRUCT_0, PARTFUN1, ALGSTR_0, XTUPLE_0;
schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, EQREL_1, FINSEQ_2, NEWTON, STRUCT_0, VECTSP_1, COMPLFLD, GROUP_2, MONOID_0, UNIROOTS, VALUED_0, ALGSTR_0, PREPOWER, RVSUM_1;
constructors HIDDEN, WELLORD2, BINOP_1, FUNCT_4, NAT_D, NEWTON, PREPOWER, WSIERP_1, REALSET2, VECTSP_6, VECTSP_7, GROUP_5, MONOID_0, POLYNOM4, UPROOTS, UNIROOTS, BINOP_2, VECTSP_9, RELSET_1, REAL_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities VECTSP_1, BINOP_1, REALSET1, GROUP_3, GROUP_2, STRUCT_0, ALGSTR_0, FUNCOP_1, ORDINAL1, CARD_1;
expansions TARSKI, VECTSP_1, FUNCT_1, GROUP_1, GROUP_2, STRUCT_0;
theorem Th2:
for
a,
k,
r being
Nat for
x being
Real st 1
< x &
0 < k holds
x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))
definition
let R be
Skew-Field;
existence
ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] )
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of R:] holds
b1 = b2
;
end;
definition
let R be
Skew-Field;
let s be
Element of
R;
existence
ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] )
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] holds
b1 = b2
;
end;