environ
vocabularies HIDDEN, SUBSET_1, XBOOLE_0, BINOP_1, FUNCT_1, MULTOP_1, FUNCSDOM, VECTSP_1, VECTSP_2, RLVECT_2, RLSUB_1, FINSEQ_1, RMOD_3, ARYTM_1, ARYTM_3, ZFMISC_1, RLVECT_3, SUPINF_2, GROUP_1, TARSKI, CARD_3, MOD_3, STRUCT_0, RLSUB_2, INCSP_1, PARTFUN1, PRELAMB, SETWISEO, LATTICES, QC_LANG1, FINSEQ_4, ALGSTR_0, RLVECT_1, RELAT_1, LMOD_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, ALGSTR_0, FUNCT_2, BINOP_1, FINSEQ_1, SETWISEO, SETWOP_2, LATTICES, MULTOP_1, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, LMOD_6;
definitions RLVECT_1, XBOOLE_0, ALGSTR_0;
theorems BINOP_1, FUNCT_2, RLVECT_1, VECTSP_7, LMOD_6, MOD_3, MULTOP_1, SETWISEO, SUBSET_1, TARSKI, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, ZFMISC_1, XBOOLE_0, XBOOLE_1, ALGSTR_0;
schemes BINOP_1, DOMAIN_1, FUNCT_2, BINOP_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, LATTICES, VECTSP_1, VECTSP_4, VECTSP_5, LATTICE2, ALGSTR_0;
constructors HIDDEN, BINOP_1, DOMAIN_1, SETWISEO, MULTOP_1, FINSOP_1, LATTICES, VECTSP_6, VECTSP_7, LMOD_6, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities STRUCT_0, ALGSTR_0;
expansions STRUCT_0;
scheme
ElementEq{
F1()
-> set ,
P1[
object ] } :
for
X1,
X2 being
Element of
F1() st ( for
x being
object holds
(
x in X1 iff
P1[
x] ) ) & ( for
x being
object holds
(
x in X2 iff
P1[
x] ) ) holds
X1 = X2
scheme
TriOpEq{
F1()
-> non
empty set ,
F2(
Element of
F1(),
Element of
F1(),
Element of
F1())
-> object } :
for
f1,
f2 being
TriOp of
F1() st ( for
a,
b,
c being
Element of
F1() holds
f1 . (
a,
b,
c)
= F2(
a,
b,
c) ) & ( for
a,
b,
c being
Element of
F1() holds
f2 . (
a,
b,
c)
= F2(
a,
b,
c) ) holds
f1 = f2
scheme
QuaOpEq{
F1()
-> non
empty set ,
F2(
Element of
F1(),
Element of
F1(),
Element of
F1(),
Element of
F1())
-> object } :
for
f1,
f2 being
QuaOp of
F1() st ( for
a,
b,
c,
d being
Element of
F1() holds
f1 . (
a,
b,
c,
d)
= F2(
a,
b,
c,
d) ) & ( for
a,
b,
c,
d being
Element of
F1() holds
f2 . (
a,
b,
c,
d)
= F2(
a,
b,
c,
d) ) holds
f1 = f2
scheme
Fr4{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3()
-> set ,
F4()
-> Element of
F1(),
F5(
object )
-> set ,
P1[
object ,
object ],
P2[
object ,
object ] } :
(
F4()
in F5(
F3()) iff for
b being
Element of
F2() st
b in F3() holds
P1[
F4(),
b] )
provided
A1:
F5(
F3())
= { a where a is Element of F1() : P2[a,F3()] }
and A2:
(
P2[
F4(),
F3()] iff for
b being
Element of
F2() st
b in F3() holds
P1[
F4(),
b] )
Lm1:
for G being AbGroup
for a, b, c being Element of G holds
( - (a - b) = (- a) - (- b) & (a - b) + c = (a + c) - b )
Lm2:
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds
( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )