REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V41() V46() V47() Element of bool REAL
bool REAL is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal V41() V46() V47() set
bool omega is non empty non trivial V41() set
bool NAT is non empty non trivial V41() set
COMPLEX is set
K356() is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding Function-like one-to-one constant functional V41() V42() V45() V46() V48( {} ) V53() V54() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative V41() V46() V53() V54() Element of NAT
{{},1} is non empty V41() V45() set
K434() is set
bool K434() is non empty set
K435() is Element of bool K434()
K475() is non empty V171() L13()
the carrier of K475() is non empty set
K438( the carrier of K475()) is non empty M34( the carrier of K475())
K474(K475()) is Element of bool K438( the carrier of K475())
bool K438( the carrier of K475()) is non empty set
[:K474(K475()),NAT:] is Relation-like set
bool [:K474(K475()),NAT:] is non empty set
[:NAT,K474(K475()):] is Relation-like set
bool [:NAT,K474(K475()):] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative V41() V46() V53() V54() Element of NAT
K347(2,K356()) is M18(K356())
[:K347(2,K356()),K356():] is Relation-like set
bool [:K347(2,K356()),K356():] is non empty set
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative V41() V46() V53() V54() Element of NAT
K347(3,K356()) is M18(K356())
[:K347(3,K356()),K356():] is Relation-like set
bool [:K347(3,K356()),K356():] is non empty set
K531() is Relation-like K347(2,K356()) -defined K356() -valued Function-like quasi_total Element of bool [:K347(2,K356()),K356():]
[:NAT,NAT:] is non empty non trivial Relation-like V41() set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like V41() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial V41() set
Nat_Lattice is non empty V239() V246() V249() L23()
the carrier of Nat_Lattice is non empty set
NATPLUS is non empty Element of bool NAT
[:NATPLUS,NATPLUS:] is non empty Relation-like set
[:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty Relation-like set
bool [:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty set
Seg 1 is Element of bool NAT
{1} is non empty trivial V41() V45() V48(1) set
Seg 2 is Element of bool NAT
{1,2} is non empty V41() V45() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding Function-like one-to-one constant functional V41() V42() V45() V46() V48( {} ) V53() V54() Element of NAT
{{}} is non empty trivial functional V41() V45() V48(1) set
meet {} is set
[:{},{}:] is Relation-like V41() set
bool [:{},{}:] is non empty V41() V45() set
X is set
[:NAT,X:] is Relation-like set
bool [:NAT,X:] is non empty set
Y is Relation-like NAT -defined X -valued Function-like quasi_total Element of bool [:NAT,X:]
f is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative V41() V46() V53() V54() set
Y | f is Relation-like NAT -defined f -defined NAT -defined X -valued Function-like V41() Element of bool [:NAT,X:]
dom Y is Element of bool NAT
dom (Y | f) is V41() Element of bool f
bool f is non empty V41() V45() set
Y is set
X is set
<%> X is T-Sequence-like Relation-like X -valued Function-like V41() set
X is non empty set
X ^omega is set
[:(X ^omega),X:] is Relation-like set
bool [:(X ^omega),X:] is non empty set
Y is Relation-like X ^omega -defined X -valued Function-like total quasi_total Element of bool [:(X ^omega),X:]
f is T-Sequence-like Relation-like X -valued Function-like V41() set
Y . f is set
Y is set
X is set
the_universe_of X is set
f is set
[:Y,f:] is Relation-like set
the_transitive-closure_of X is set
Tarski-Class (the_transitive-closure_of X) is set
F2() is Relation-like Function-like set
proj1 F2() is set
F3() is Relation-like Function-like set
proj1 F3() is set
X is T-Sequence-like Relation-like Function-like set
proj1 X is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
y is T-Sequence-like Relation-like Function-like set
X | f is T-Sequence-like Relation-like proj2 X -valued Function-like set
proj2 X is set
X . f is set
F1(y) is set
Y is T-Sequence-like Relation-like Function-like set
proj1 Y is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
y is T-Sequence-like Relation-like Function-like set
Y | f is T-Sequence-like Relation-like proj2 Y -valued Function-like set
proj2 Y is set
Y . f is set
F1(y) is set
X is T-Sequence-like Relation-like Function-like set
proj1 X is epsilon-transitive epsilon-connected ordinal set
Y is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative V41() V46() V53() V54() set
X . Y is set
X | Y is T-Sequence-like Relation-like proj2 X -valued Function-like V41() set
proj2 X is set
F1((X | Y)) is set
f is epsilon-transitive epsilon-connected ordinal set
X . f is set
X | f is T-Sequence-like Relation-like proj2 X -valued Function-like set
F1((X | f)) is set
F1() is non empty set
[:NAT,F1():] is non empty non trivial Relation-like V41() set
bool [:NAT,F1():] is non empty non trivial V41() set
F3() is non empty Relation-like NAT -defined F1() -valued Function-like total quasi_total Element of bool [:NAT,F1():]
F4() is non empty Relation-like NAT -defined F1() -valued Function-like total quasi_total Element of bool [:NAT,F1():]
X is Relation-like Function-like set
proj1 X is set
f is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative V41() V46() V53() V54() set
X . f is set
X | f is Relation-like Function-like V41() set
(F1(),(X | f)) is T-Sequence-like Relation-like F1() -valued Function-like V41() set
F2((F1(),(X | f))) is Element of F1()
F3() | f is T-Sequence-like Relation-like NAT -defined f -defined NAT -defined F1() -valued Function-like V41() Element of bool [:NAT,F1():]
F2((F3() | f)) is Element of F1()
Y is Relation-like Function-like set
proj1 Y is set
f is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative V41() V46() V53() V54() set
Y . f is set
Y | f is Relation-like Function-like V41() set
(F1(),(Y | f)) is T-Sequence-like Relation-like F1() -valued Function-like V41() set
F2((F1(),(Y | f))) is Element of F1()
F4() | f is T-Sequence-like Relation-like NAT -defined f -defined NAT -defined F1() -valued Function-like V41() Element of bool [:NAT,F1():]
F2((F4() | f)) is Element of F1()
F1() is non empty set
[:NAT,F1():] is non empty non trivial Relation-like V41() set
bool [:NAT,F1():] is non empty non trivial V41() set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
Y is set
f is set
X . f is set
y is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative V41() V46() V53() V54() set
X | y is Relation-like Function-like V41() set
(F1(),(X | y)) is T-Sequence-like Relation-like F1() -valued Function-like V41() set
F2((F1(),(X | y))) is Element of F1()
Y is non empty Relation-like NAT -defined F1() -valued Function-like total quasi_total Element of bool [:NAT,F1():]
f is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative V41() V46() V53() V54() set
Y . f is set
Y | f is T-Sequence-like Relation-like NAT -defined f -defined NAT -defined F1() -valued Function-like V41() Element of bool [:NAT,F1():]
F2((Y | f)) is Element of F1()
X . f is set
(F1(),(Y | f)) is T-Sequence-like Relation-like F1() -valued Function-like V41() set
F2((F1(),(Y | f))) is Element of F1()
[:[:{},{}:],{}:] is Relation-like V41() set
bool [:[:{},{}:],{}:] is non empty V41() V45() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding [:{},{}:] -defined {} -valued Function-like one-to-one constant functional quasi_total V41() V42() V45() V46() V48( {} ) V53() V54() Element of bool [:[:{},{}:],{}:] is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding [:{},{}:] -defined {} -valued Function-like one-to-one constant functional quasi_total V41() V42() V45() V46() V48( {} ) V53() V54() Element of bool [:[:{},{}:],{}:]
multMagma(# {}, the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding [:{},{}:] -defined {} -valued Function-like one-to-one constant functional quasi_total V41() V42() V45() V46() V48( {} ) V53() V54() Element of bool [:[:{},{}:],{}:] #) is strict multMagma
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
X is multMagma
the carrier of X is set
nabla the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V258() V260() V265() Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
f is Element of the carrier of X
y is Element of the carrier of X
Class ((nabla the carrier of X),y) is Element of bool the carrier of X
bool the carrier of X is non empty set
x is Element of the carrier of X
c6 is Element of the carrier of X
Class ((nabla the carrier of X),c6) is Element of bool the carrier of X
f * x is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,x) is Element of the carrier of X
y * c6 is Element of the carrier of X
the multF of X . (y,c6) is Element of the carrier of X
Class ((nabla the carrier of X),(y * c6)) is Element of bool the carrier of X
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
nabla the carrier of X is Relation-like the carrier of X -defined the carrier of X -defined the carrier of X -valued the carrier of X -valued total total quasi_total quasi_total V258() V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() Element of bool [: the carrier of X, the carrier of X:]
f is Element of the carrier of X
Class (Y,f) is Element of bool the carrier of X
bool the carrier of X is non empty set
y is Element of the carrier of X
Class (Y,y) is Element of bool the carrier of X
x is Element of the carrier of X
Class (Y,x) is Element of bool the carrier of X
c6 is Element of the carrier of X
Class (Y,c6) is Element of bool the carrier of X
f * x is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,x) is Element of the carrier of X
Class (Y,(f * x)) is Element of bool the carrier of X
y * c6 is Element of the carrier of X
the multF of X . (y,c6) is Element of the carrier of X
Class (Y,(y * c6)) is Element of bool the carrier of X
f * x is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,x) is Element of the carrier of X
y * c6 is Element of the carrier of X
the multF of X . (y,c6) is Element of the carrier of X
Class (Y,(y * c6)) is Element of bool the carrier of X
Class (Y,(f * x)) is Element of bool the carrier of X
f is Element of the carrier of X
y is Element of the carrier of X
Class (Y,y) is Element of bool the carrier of X
x is Element of the carrier of X
c6 is Element of the carrier of X
Class (Y,c6) is Element of bool the carrier of X
f * x is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,x) is Element of the carrier of X
y * c6 is Element of the carrier of X
the multF of X . (y,c6) is Element of the carrier of X
Class (Y,(y * c6)) is Element of bool the carrier of X
Class (Y,f) is Element of bool the carrier of X
Class (Y,x) is Element of bool the carrier of X
Class (Y,(f * x)) is Element of bool the carrier of X
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
Class Y is with_non-empty_elements a_partition of the carrier of X
[:(Class Y),(Class Y):] is Relation-like set
[:[:(Class Y),(Class Y):],(Class Y):] is Relation-like set
bool [:[:(Class Y),(Class Y):],(Class Y):] is non empty set
f is non empty set
y is Element of f
x is Element of f
c6 is set
Class (Y,c6) is Element of bool the carrier of X
bool the carrier of X is non empty set
w2 is set
Class (Y,w2) is Element of bool the carrier of X
w1 is Element of the carrier of X
v1 is Element of the carrier of X
w1 * v1 is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (w1,v1) is Element of the carrier of X
Class (Y,(w1 * v1)) is Element of bool the carrier of X
v2 is Element of f
c11 is Element of Class Y
w9 is Element of Class Y
z2 is Element of the carrier of X
Class (Y,z2) is Element of bool the carrier of X
z1 is Element of the carrier of X
Class (Y,z1) is Element of bool the carrier of X
z2 * z1 is Element of the carrier of X
the multF of X . (z2,z1) is Element of the carrier of X
Class (Y,(z2 * z1)) is Element of bool the carrier of X
[:f,f:] is non empty Relation-like set
[:[:f,f:],f:] is non empty Relation-like set
bool [:[:f,f:],f:] is non empty set
y is non empty Relation-like [:f,f:] -defined f -valued Function-like total quasi_total Element of bool [:[:f,f:],f:]
x is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
c6 is Element of Class Y
w2 is Element of the carrier of X
Class (Y,w2) is Element of bool the carrier of X
bool the carrier of X is non empty set
w1 is Element of Class Y
v1 is Element of the carrier of X
Class (Y,v1) is Element of bool the carrier of X
x . (c6,w1) is Element of Class Y
w2 * v1 is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (w2,v1) is Element of the carrier of X
Class (Y,(w2 * v1)) is Element of bool the carrier of X
the Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):] is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
f is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
y is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
x is set
c6 is set
f . (x,c6) is set
y . (x,c6) is set
w1 is Element of Class Y
v1 is set
Class (Y,v1) is Element of bool the carrier of X
bool the carrier of X is non empty set
w2 is Element of Class Y
v2 is set
Class (Y,v2) is Element of bool the carrier of X
f . (w1,w2) is Element of Class Y
c11 is Element of the carrier of X
w9 is Element of the carrier of X
c11 * w9 is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (c11,w9) is Element of the carrier of X
Class (Y,(c11 * w9)) is Element of bool the carrier of X
y is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
x is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
c6 is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
w1 is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
w2 is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
v1 is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
Class Y is with_non-empty_elements a_partition of the carrier of X
(X,Y) is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
[:(Class Y),(Class Y):] is Relation-like set
[:[:(Class Y),(Class Y):],(Class Y):] is Relation-like set
bool [:[:(Class Y),(Class Y):],(Class Y):] is non empty set
multMagma(# (Class Y),(X,Y) #) is strict multMagma
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
(X,Y) is multMagma
Class Y is with_non-empty_elements a_partition of the carrier of X
(X,Y) is Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
[:(Class Y),(Class Y):] is Relation-like set
[:[:(Class Y),(Class Y):],(Class Y):] is Relation-like set
bool [:[:(Class Y),(Class Y):],(Class Y):] is non empty set
multMagma(# (Class Y),(X,Y) #) is strict multMagma
X is non empty multMagma
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
(X,Y) is strict multMagma
Class Y is non empty with_non-empty_elements a_partition of the carrier of X
(X,Y) is non empty Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
[:(Class Y),(Class Y):] is non empty Relation-like set
[:[:(Class Y),(Class Y):],(Class Y):] is non empty Relation-like set
bool [:[:(Class Y),(Class Y):],(Class Y):] is non empty set
multMagma(# (Class Y),(X,Y) #) is strict multMagma
X is non empty multMagma
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
(X,Y) is non empty strict multMagma
Class Y is non empty with_non-empty_elements a_partition of the carrier of X
(X,Y) is non empty Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
[:(Class Y),(Class Y):] is non empty Relation-like set
[:[:(Class Y),(Class Y):],(Class Y):] is non empty Relation-like set
bool [:[:(Class Y),(Class Y):],(Class Y):] is non empty set
multMagma(# (Class Y),(X,Y) #) is strict multMagma
the carrier of (X,Y) is non empty set
[: the carrier of X, the carrier of (X,Y):] is non empty Relation-like set
bool [: the carrier of X, the carrier of (X,Y):] is non empty set
f is set
y is Element of the carrier of X
Class (Y,y) is Element of bool the carrier of X
bool the carrier of X is non empty set
x is set
f is Relation-like Function-like set
proj1 f is set
proj2 f is set
y is set
x is set
f . x is set
c6 is Element of the carrier of X
Class (Y,c6) is Element of bool the carrier of X
bool the carrier of X is non empty set
y is non empty Relation-like the carrier of X -defined the carrier of (X,Y) -valued Function-like total quasi_total Element of bool [: the carrier of X, the carrier of (X,Y):]
x is Element of the carrier of X
y . x is Element of the carrier of (X,Y)
Class (Y,x) is Element of bool the carrier of X
bool the carrier of X is non empty set
c6 is Element of the carrier of X
Class (Y,c6) is Element of bool the carrier of X
f is non empty Relation-like the carrier of X -defined the carrier of (X,Y) -valued Function-like total quasi_total Element of bool [: the carrier of X, the carrier of (X,Y):]
y is non empty Relation-like the carrier of X -defined the carrier of (X,Y) -valued Function-like total quasi_total Element of bool [: the carrier of X, the carrier of (X,Y):]
x is Element of the carrier of X
f . x is Element of the carrier of (X,Y)
Class (Y,x) is Element of bool the carrier of X
bool the carrier of X is non empty set
y . x is Element of the carrier of (X,Y)
X is non empty multMagma
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
(X,Y) is non empty strict multMagma
Class Y is non empty with_non-empty_elements a_partition of the carrier of X
(X,Y) is non empty Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
[:(Class Y),(Class Y):] is non empty Relation-like set
[:[:(Class Y),(Class Y):],(Class Y):] is non empty Relation-like set
bool [:[:(Class Y),(Class Y):],(Class Y):] is non empty set
multMagma(# (Class Y),(X,Y) #) is strict multMagma
(X,Y) is non empty Relation-like the carrier of X -defined the carrier of (X,Y) -valued Function-like total quasi_total Element of bool [: the carrier of X, the carrier of (X,Y):]
the carrier of (X,Y) is non empty set
[: the carrier of X, the carrier of (X,Y):] is non empty Relation-like set
bool [: the carrier of X, the carrier of (X,Y):] is non empty set
f is Element of the carrier of X
y is Element of the carrier of X
f * y is Element of the carrier of X
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,y) is Element of the carrier of X
(X,Y) . (f * y) is Element of the carrier of (X,Y)
(X,Y) . f is Element of the carrier of (X,Y)
(X,Y) . y is Element of the carrier of (X,Y)
((X,Y) . f) * ((X,Y) . y) is Element of the carrier of (X,Y)
the multF of (X,Y) is non empty Relation-like [: the carrier of (X,Y), the carrier of (X,Y):] -defined the carrier of (X,Y) -valued Function-like total quasi_total Element of bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):]
[: the carrier of (X,Y), the carrier of (X,Y):] is non empty Relation-like set
[:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty Relation-like set
bool [:[: the carrier of (X,Y), the carrier of (X,Y):], the carrier of (X,Y):] is non empty set
the multF of (X,Y) . (((X,Y) . f),((X,Y) . y)) is Element of the carrier of (X,Y)
Class (Y,f) is Element of bool the carrier of X
bool the carrier of X is non empty set
Class (Y,y) is Element of bool the carrier of X
(X,Y) . (((X,Y) . f),((X,Y) . y)) is set
Class (Y,(f * y)) is Element of bool the carrier of X
X is non empty multMagma
the carrier of X is non empty set
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
(X,Y) is non empty strict multMagma
Class Y is non empty with_non-empty_elements a_partition of the carrier of X
(X,Y) is non empty Relation-like [:(Class Y),(Class Y):] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(Class Y),(Class Y):],(Class Y):]
[:(Class Y),(Class Y):] is non empty Relation-like set
[:[:(Class Y),(Class Y):],(Class Y):] is non empty Relation-like set
bool [:[:(Class Y),(Class Y):],(Class Y):] is non empty set
multMagma(# (Class Y),(X,Y) #) is strict multMagma
the carrier of (X,Y) is non empty set
(X,Y) is non empty Relation-like the carrier of X -defined the carrier of (X,Y) -valued Function-like total quasi_total multiplicative Element of bool [: the carrier of X, the carrier of (X,Y):]
[: the carrier of X, the carrier of (X,Y):] is non empty Relation-like set
bool [: the carrier of X, the carrier of (X,Y):] is non empty set
rng (X,Y) is non empty Element of bool the carrier of (X,Y)
bool the carrier of (X,Y) is non empty set
f is set
y is set
Class (Y,y) is Element of bool the carrier of X
bool the carrier of X is non empty set
dom (X,Y) is non empty Element of bool the carrier of X
x is Element of the carrier of X
(X,Y) . x is Element of the carrier of (X,Y)
Class (Y,x) is Element of bool the carrier of X
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like [: the carrier of X, the carrier of X:] -valued Function-like set
proj1 Y is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:] : for b2 being set
for b3, b4 being Element of the carrier of X holds
( not b2 in proj1 Y or not Y . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
meet { b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:] : for b2 being set
for b3, b4 being Element of the carrier of X holds
( not b2 in proj1 Y or not Y . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
y is set
x is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
bool {} is non empty V41() V45() set
nabla the carrier of X is Relation-like the carrier of X -defined the carrier of X -defined the carrier of X -valued the carrier of X -valued total total quasi_total quasi_total V258() V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
y is set
Y . y is set
x is Element of the carrier of X
c6 is Element of the carrier of X
[x,c6] is V26() set
{x,c6} is non empty V41() set
{x} is non empty trivial V41() V48(1) set
{{x,c6},{x}} is non empty V41() V45() set
Class ((nabla the carrier of X),c6) is Element of bool the carrier of X
bool the carrier of X is non empty set
bool [: the carrier of X, the carrier of X:] is non empty Element of bool (bool [: the carrier of X, the carrier of X:])
bool (bool [: the carrier of X, the carrier of X:]) is non empty set
y is set
x is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
y is Element of bool (bool [: the carrier of X, the carrier of X:])
x is set
c6 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
Y is Relation-like [: the carrier of X, the carrier of X:] -valued Function-like set
proj1 Y is set
(X,Y) is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() Element of bool [: the carrier of X, the carrier of X:]
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:] : for b2 being set
for b3, b4 being Element of the carrier of X holds
( not b2 in proj1 Y or not Y . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
meet { b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:] : for b2 being set
for b3, b4 being Element of the carrier of X holds
( not b2 in proj1 Y or not Y . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
f is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
y is set
X is multMagma
the carrier of X is set
[: the carrier of X, the carrier of X:] is Relation-like set
Y is Relation-like [: the carrier of X, the carrier of X:] -valued Function-like set
(X,Y) is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() Element of bool [: the carrier of X, the carrier of X:]
bool [: the carrier of X, the carrier of X:] is non empty set
proj1 Y is set
{ b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:] : for b2 being set
for b3, b4 being Element of the carrier of X holds
( not b2 in proj1 Y or not Y . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
meet { b1 where b1 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:] : for b2 being set
for b3, b4 being Element of the carrier of X holds
( not b2 in proj1 Y or not Y . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
y is Element of the carrier of X
x is Element of the carrier of X
Class ((X,Y),x) is Element of bool the carrier of X
bool the carrier of X is non empty set
c6 is Element of the carrier of X
w1 is Element of the carrier of X
Class ((X,Y),w1) is Element of bool the carrier of X
y * c6 is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (y,c6) is Element of the carrier of X
x * w1 is Element of the carrier of X
the multF of X . (x,w1) is Element of the carrier of X
Class ((X,Y),(x * w1)) is Element of bool the carrier of X
[x,y] is V26() set
{x,y} is non empty V41() set
{x} is non empty trivial V41() V48(1) set
{{x,y},{x}} is non empty V41() V45() set
[w1,c6] is V26() set
{w1,c6} is non empty V41() set
{w1} is non empty trivial V41() V48(1) set
{{w1,c6},{w1}} is non empty V41() V45() set
[(x * w1),(y * c6)] is V26() set
{(x * w1),(y * c6)} is non empty V41() set
{(x * w1)} is non empty trivial V41() V48(1) set
{{(x * w1),(y * c6)},{(x * w1)}} is non empty V41() V45() set
w2 is set
v1 is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() (X) Element of bool [: the carrier of X, the carrier of X:]
Class (v1,x) is Element of bool the carrier of X
Class (v1,w1) is Element of bool the carrier of X
Class (v1,(x * w1)) is Element of bool the carrier of X
X is set
Y is set
[:X,Y:] is Relation-like set
bool [:X,Y:] is non empty set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined Y -valued Function-like quasi_total Element of bool [:X,Y:]
y is set
f . y is set
y is set
f . y is set
x is set
f . x is set
y is set
f . y is set
x is set
f . x is set
c6 is set
f . c6 is set
y is Relation-like X -defined X -valued total quasi_total V260() V265() Element of bool [:X,X:]
y is Relation-like X -defined X -valued total quasi_total V260() V265() Element of bool [:X,X:]
x is Relation-like X -defined X -valued total quasi_total V260() V265() Element of bool [:X,X:]
c6 is set
w1 is set
[c6,w1] is V26() set
{c6,w1} is non empty V41() set
{c6} is non empty trivial V41() V48(1) set
{{c6,w1},{c6}} is non empty V41() V45() set
f . c6 is set
f . w1 is set
w2 is set
v1 is set
f . w2 is set
f . v1 is set
[w2,v1] is V26() set
{w2,v1} is non empty V41() set
{w2} is non empty trivial V41() V48(1) set
{{w2,v1},{w2}} is non empty V41() V45() set
c6 is set
w1 is set
[c6,w1] is V26() set
{c6,w1} is non empty V41() set
{c6} is non empty trivial V41() V48(1) set
{{c6,w1},{c6}} is non empty V41() V45() set
f . c6 is set
f . w1 is set
w2 is set
v1 is set
f . w2 is set
f . v1 is set
[w2,v1] is V26() set
{w2,v1} is non empty V41() set
{w2} is non empty trivial V41() V48(1) set
{{w2,v1},{w2}} is non empty V41() V45() set
X is non empty multMagma
the carrier of X is non empty set
Y is non empty multMagma
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
bool [: the carrier of X, the carrier of Y:] is non empty set
f is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total Element of bool [: the carrier of X, the carrier of Y:]
( the carrier of X, the carrier of Y,f) is Relation-like the carrier of X -defined the carrier of X -valued total quasi_total V260() V265() Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
bool [: the carrier of X, the carrier of X:] is non empty set
x is Element of the carrier of X
c6 is Element of the carrier of X
Class (( the carrier of X, the carrier of Y,f),c6) is Element of bool the carrier of X
bool the carrier of X is non empty set
w1 is Element of the carrier of X
w2 is Element of the carrier of X
Class (( the carrier of X, the carrier of Y,f),w2) is Element of bool the carrier of X
x * w1 is Element of the carrier of X
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (x,w1) is Element of the carrier of X
c6 * w2 is Element of the carrier of X
the multF of X . (c6,w2) is Element of the carrier of X
Class (( the carrier of X, the carrier of Y,f),(c6 * w2)) is Element of bool the carrier of X
[c6,x] is V26() set
{c6,x} is non empty V41() set
{c6} is non empty trivial V41() V48(1) set
{{c6,x},{c6}} is non empty V41() V45() set
[w2,w1] is V26() set
{w2,w1} is non empty V41() set
{w2} is non empty trivial V41() V48(1) set
{{w2,w1},{w2}} is non empty V41() V45() set
f . w2 is Element of the carrier of Y
f . w1 is Element of the carrier of Y
f . (c6 * w2) is Element of the carrier of Y
f . c6 is Element of the carrier of Y
(f . c6) * (f . w2) is Element of the carrier of Y
the multF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the multF of Y . ((f . c6),(f . w2)) is Element of the carrier of Y
f . x is Element of the carrier of Y
(f . x) * (f . w1) is Element of the carrier of Y
the multF of Y . ((f . x),(f . w1)) is Element of the carrier of Y
f . (x * w1) is Element of the carrier of Y
[(c6 * w2),(x * w1)] is V26() set
{(c6 * w2),(x * w1)} is non empty V41() set
{(c6 * w2)} is non empty trivial V41() V48(1) set
{{(c6 * w2),(x * w1)},{(c6 * w2)}} is non empty V41() V45() set
X is non empty multMagma
the carrier of X is non empty set
Y is non empty multMagma
the carrier of Y is non empty set
[: the carrier of Y, the carrier of X:] is non empty Relation-like set
bool [: the carrier of Y, the carrier of X:] is non empty set
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
f is non empty Relation-like the carrier of Y -defined the carrier of X -valued Function-like total quasi_total Element of bool [: the carrier of Y, the carrier of X:]
( the carrier of Y, the carrier of X,f) is Relation-like the carrier of Y -defined the carrier of Y -valued total quasi_total V260() V265() Element of bool [: the carrier of Y, the carrier of Y:]
bool [: the carrier of Y, the carrier of Y:] is non empty set
{ [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } is set
id { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } is Relation-like { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } -defined { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } -valued Function-like one-to-one total quasi_total Element of bool [: { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } , { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } :]
[: { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } , { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } :] is Relation-like set
bool [: { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } , { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } :] is non empty set
dom (id { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } ) is Element of bool { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 }
bool { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } is non empty set
rng (id { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } ) is Element of bool { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 }
c6 is set
w1 is set
(id { [b1,b2] where b1, b2 is Element of the carrier of Y : f . b1 = f . b2 } ) . w1 is set
w2 is Element of the carrier of Y
v1 is Element of the carrier of Y
[w2,v1] is V26() set
{w2,v1} is non empty V41() set
{w2} is non empty trivial V41() V48(1) set
{{w2,v1},{w2}} is non empty V41() V45() set
f . w2 is Element of the carrier of X
f . v1 is Element of the carrier of X
c6 is Relation-like [: the carrier of Y, the carrier of Y:] -valued Function-like set
(Y,c6) is Relation-like the carrier of Y -defined the carrier of Y -valued total quasi_total V260() V265() (Y) Element of bool [: the carrier of Y, the carrier of Y:]
proj1 c6 is set
{ b1 where b1 is Relation-like the carrier of Y -defined the carrier of Y -valued total quasi_total V260() V265() (Y) Element of bool [: the carrier of Y, the carrier of Y:] : for b2 being set
for b3, b4 being Element of the carrier of Y holds
( not b2 in proj1 c6 or not c6 . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
meet { b1 where b1 is Relation-like the carrier of Y -defined the carrier of Y -valued total quasi_total V260() V265() (Y) Element of bool [: the carrier of Y, the carrier of Y:] : for b2 being set
for b3, b4 being Element of the carrier of Y holds
( not b2 in proj1 c6 or not c6 . b2 = [b3,b4] or b3 in Class (b1,b4) ) } is set
w1 is Relation-like the carrier of Y -defined the carrier of Y -valued total quasi_total V260() V265() (Y) Element of bool [: the carrier of Y, the carrier of Y:]
w2 is set
c6 . w2 is set
v1 is Element of the carrier of Y
v2 is Element of the carrier of Y
[v1,v2] is V26() set
{v1,v2} is non empty V41() set
{v1} is non empty trivial V41() V48(1) set
{{v1,v2},{v1}} is non empty V41() V45() set
Class (w1,v2) is Element of bool the carrier of Y
bool the carrier of Y is non empty set
c11 is Element of the carrier of Y
w9 is Element of the carrier of Y
[c11,w9] is V26() set
{c11,w9} is non empty V41() set
{c11} is non empty trivial V41() V48(1) set
{{c11,w9},{c11}} is non empty V41() V45() set
f . c11 is Element of the carrier of X
f . w9 is Element of the carrier of X
w2 is set
v1 is set
v2 is set
[v1,v2] is V26() set
{v1,v2} is non empty V41() set
{v1} is non empty trivial V41() V48(1) set
{{v1,v2},{v1}} is non empty V41() V45() set
f . v1 is set
f . v2 is set
z1 is set
z2 is Relation-like the carrier of Y -defined the carrier of Y -valued total quasi_total V260() V265() (Y) Element of bool [: the carrier of Y, the carrier of Y:]
c11 is Element of the carrier of Y
w9 is Element of the carrier of Y
[c11,w9] is V26() set
{c11,w9} is non empty V41() set
{c11} is non empty trivial V41() V48(1) set
{{c11,w9},{c11}} is non empty V41() V45() set
c6 . [c11,w9] is set
Class (z2,w9) is Element of bool the carrier of Y
bool the carrier of Y is non empty set
X is multMagma
the carrier of X is set
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the empty trivial V63() {} -element multMagma is empty trivial V63() {} -element multMagma
the carrier of the empty trivial V63() {} -element multMagma is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding Function-like one-to-one constant functional V41() V42() V45() V46() V48( {} ) V53() V54() set
f is set
[:f,f:] is Relation-like set
the multF of the empty trivial V63() {} -element multMagma is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding [: the carrier of the empty trivial V63() {} -element multMagma , the carrier of the empty trivial V63() {} -element multMagma :] -defined the carrier of the empty trivial V63() {} -element multMagma -valued Function-like one-to-one constant functional quasi_total V41() V42() V45() V46() V48( {} ) V53() V54() Element of bool [:[: the carrier of the empty trivial V63() {} -element multMagma , the carrier of the empty trivial V63() {} -element multMagma :], the carrier of the empty trivial V63() {} -element multMagma :]
[: the carrier of the empty trivial V63() {} -element multMagma , the carrier of the empty trivial V63() {} -element multMagma :] is Relation-like V41() set
[:[: the carrier of the empty trivial V63() {} -element multMagma , the carrier of the empty trivial V63() {} -element multMagma :], the carrier of the empty trivial V63() {} -element multMagma :] is Relation-like V41() set
bool [:[: the carrier of the empty trivial V63() {} -element multMagma , the carrier of the empty trivial V63() {} -element multMagma :], the carrier of the empty trivial V63() {} -element multMagma :] is non empty V41() V45() set
the multF of X | {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative Relation-like non-empty empty-yielding {} -defined [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like one-to-one constant functional V41() V42() V45() V46() V48( {} ) V53() V54() Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
y is set
the multF of X | y is Relation-like [: the carrier of X, the carrier of X:] -defined y -defined [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
the multF of X || the carrier of the empty trivial V63() {} -element multMagma is Relation-like Function-like set
X is multMagma
the carrier of X is set
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
multMagma(# the carrier of X, the multF of X #) is strict multMagma
the multF of multMagma(# the carrier of X, the multF of X #) is Relation-like [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] -defined the carrier of multMagma(# the carrier of X, the multF of X #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):]
the carrier of multMagma(# the carrier of X, the multF of X #) is set
[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] is Relation-like set
[:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):] is Relation-like set
bool [:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):] is non empty set
the multF of multMagma(# the carrier of X, the multF of X #) | [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] is Relation-like [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] -defined [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] -defined the carrier of multMagma(# the carrier of X, the multF of X #) -valued Function-like Element of bool [:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):]
the multF of X || the carrier of multMagma(# the carrier of X, the multF of X #) is Relation-like Function-like set
f is (X)
X is non empty multMagma
the carrier of X is non empty set
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
multMagma(# the carrier of X, the multF of X #) is strict multMagma
the multF of multMagma(# the carrier of X, the multF of X #) is Relation-like [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] -defined the carrier of multMagma(# the carrier of X, the multF of X #) -valued Function-like quasi_total Element of bool [:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):]
the carrier of multMagma(# the carrier of X, the multF of X #) is set
[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] is Relation-like set
[:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):] is Relation-like set
bool [:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):] is non empty set
the multF of multMagma(# the carrier of X, the multF of X #) | [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] is Relation-like [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] -defined [: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):] -defined the carrier of multMagma(# the carrier of X, the multF of X #) -valued Function-like Element of bool [:[: the carrier of multMagma(# the carrier of X, the multF of X #), the carrier of multMagma(# the carrier of X, the multF of X #):], the carrier of multMagma(# the carrier of X, the multF of X #):]
the multF of X || the carrier of multMagma(# the carrier of X, the multF of X #) is Relation-like Function-like set
f is (X)
X is multMagma
Y is (X)
the carrier of Y is set
the multF of Y is Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
multMagma(# the carrier of Y, the multF of Y #) is strict multMagma
f is (X)
the carrier of f is set
the multF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is Relation-like set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is Relation-like set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
multMagma(# the carrier of f, the multF of f #) is strict multMagma
the multF of f || the carrier of Y is Relation-like Function-like set
the multF of Y || the carrier of f is Relation-like Function-like set
( the multF of Y || the carrier of f) || the carrier of Y is Relation-like Function-like set
the multF of Y | [: the carrier of f, the carrier of f:] is Relation-like [: the carrier of Y, the carrier of Y:] -defined [: the carrier of f, the carrier of f:] -defined [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
( the multF of Y | [: the carrier of f, the carrier of f:]) || the carrier of Y is Relation-like Function-like set
( the multF of Y | [: the carrier of f, the carrier of f:]) | [: the carrier of Y, the carrier of Y:] is Relation-like [: the carrier of Y, the carrier of Y:] -defined [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
X is multMagma
the carrier of X is set
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
multMagma(# the carrier of X, the multF of X #) is strict multMagma
Y is (X)
the carrier of Y is set
the multF of Y is Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
multMagma(# the carrier of Y, the multF of Y #) is strict multMagma
the multF of X | [: the carrier of X, the carrier of X:] is Relation-like [: the carrier of X, the carrier of X:] -defined [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
the multF of X || the carrier of X is Relation-like Function-like set
f is (X)
the multF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
the carrier of f is set
[: the carrier of f, the carrier of f:] is Relation-like set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is Relation-like set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
the multF of Y || the carrier of f is Relation-like Function-like set
X is multMagma
the carrier of X is set
bool the carrier of X is non empty set
X is multMagma
the carrier of X is set
bool the carrier of X is non empty set
Y is Element of bool the carrier of X
f is Element of the carrier of X
y is Element of the carrier of X
f * y is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,y) is Element of the carrier of X
X is multMagma
the carrier of X is set
bool the carrier of X is non empty set
Y is (X)
the carrier of Y is set
f is Element of the carrier of X
y is Element of the carrier of X
f * y is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,y) is Element of the carrier of X
[f,y] is V26() set
{f,y} is non empty V41() set
{f} is non empty trivial V41() V48(1) set
{{f,y},{f}} is non empty V41() V45() set
[: the carrier of Y, the carrier of Y:] is Relation-like set
x is Element of the carrier of Y
c6 is Element of the carrier of Y
x * c6 is Element of the carrier of Y
the multF of Y is Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the multF of Y . (x,c6) is Element of the carrier of Y
[x,c6] is V26() set
{x,c6} is non empty V41() set
{x} is non empty trivial V41() V48(1) set
{{x,c6},{x}} is non empty V41() V45() set
the multF of Y . [x,c6] is set
the multF of X || the carrier of Y is Relation-like Function-like set
( the multF of X || the carrier of Y) . [x,c6] is set
the multF of X | [: the carrier of Y, the carrier of Y:] is Relation-like [: the carrier of X, the carrier of X:] -defined [: the carrier of Y, the carrier of Y:] -defined [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
( the multF of X | [: the carrier of Y, the carrier of Y:]) . [f,y] is set
the multF of X . [f,y] is set
X is multMagma
the carrier of X is set
bool the carrier of X is non empty set
Y is (X)
the carrier of Y is set
f is Element of bool the carrier of X
X is multMagma
the carrier of X is set
bool the carrier of X is non empty set
Y is Relation-like Function-like set
proj1 Y is set
meet Y is set
f is set
proj2 Y is set
meet (proj2 Y) is set
y is set
Y . y is set
f is Element of the carrier of X
y is Element of the carrier of X
f * y is Element of the carrier of X
the multF of X is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,y) is Element of the carrier of X
proj2 Y is set
meet (proj2 Y) is set
proj2 Y is set
meet (proj2 Y) is set
x is set
c6 is set
Y . c6 is set
X is non empty multMagma
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is Element of bool the carrier of X
Y * Y is Element of bool the carrier of X
f is set
y is Element of the carrier of X
x is Element of the carrier of X
y * x is Element of the carrier of X
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (y,x) is Element of the carrier of X
f is Element of the carrier of X
y is Element of the carrier of X
f * y is Element of the carrier of X
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (f,y) is Element of the carrier of X
X is non empty multMagma
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is non empty multMagma
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty Relation-like set
bool [: the carrier of X, the carrier of Y:] is non empty set
bool the carrier of Y is non empty set
f is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total Element of bool [: the carrier of X, the carrier of Y:]
y is (X) Element of bool the carrier of X
f .: y is Element of bool the carrier of Y
x is Element of the carrier of Y
c6 is Element of the carrier of Y
x * c6 is Element of the carrier of Y
the multF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the multF of Y . (x,c6) is Element of the carrier of Y
dom f is non empty Element of bool the carrier of X
w1 is set
f . w1 is set
w2 is set
f . w2 is set
v1 is Element of the carrier of X
v2 is Element of the carrier of X
v1 * v2 is Element of the carrier of X
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X . (v1,v2) is Element of the carrier of X
f . (v1 * v2) is Element of the carrier of Y
X is non empty multMagma
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is non empty multMagma
the carrier of Y is non empty set
[: the carrier of Y, the carrier of X:] is non empty Relation-like set
bool [: the carrier of Y, the carrier of X:] is non empty set
bool the carrier of Y is non empty set
f is non empty Relation-like the carrier of Y -defined the carrier of X -valued Function-like total quasi_total Element of bool [: the carrier of Y, the carrier of X:]
y is (X) Element of bool the carrier of X
f " y is Element of bool the carrier of Y
x is Element of the carrier of Y
c6 is Element of the carrier of Y
x * c6 is Element of the carrier of Y
the multF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty Relation-like set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty Relation-like set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the multF of Y . (x,c6) is Element of the carrier of Y
dom f is non empty Element of bool the carrier of Y
f . x is Element of the carrier of X
f . c6 is Element of the carrier of X
(f . x) * (f . c6) is Element of the carrier of X
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty Relation-like set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty Relation-like set
bool [:[: the carrier of X, the