:: ALGSTR_4 semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty non trivial V41() set
bool NAT is non empty non trivial V41() set

K356() is set

{{},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

bool [:K474(K475()),NAT:] is non empty set

bool [:NAT,K474(K475()):] is non empty set

K347(2,K356()) is M18(K356())
[:K347(2,K356()),K356():] is Relation-like set
bool [:K347(2,K356()),K356():] is non empty set

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():]
is non empty non trivial Relation-like V41() set
is non empty non trivial Relation-like V41() set
bool 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

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

is non empty trivial functional V41() V45() V48(1) set

bool is non empty V41() V45() set
X is set

bool [:NAT,X:] is non empty set

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 non empty set
X ^omega is set
[:(),X:] is Relation-like set
bool [:(),X:] is non empty set

Y . f is set
Y is set
X is set

f is set
[:Y,f:] is Relation-like set

proj1 F2() is set

proj1 F3() is set

proj2 X is set
X . f is set
F1(y) is set

proj2 Y is set
Y . f is set
F1(y) is set

X . Y is set

proj2 X is set
F1((X | Y)) is set

X . f is 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():]

proj1 X is set

X . f is set

(F1(),(X | f)) is T-Sequence-like Relation-like F1() -valued Function-like V41() set
F2((F1(),(X | f))) is Element of F1()

F2((F3() | f)) is Element of F1()

proj1 Y is set

Y . 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()

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

proj1 X is set
proj2 X is set
Y is set
f is set
X . f is 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 . f is set

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()

bool is non empty V41() V45() set

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
[:(),():] is Relation-like set
[:[:(),():],():] is Relation-like set
bool [:[:(),():],():] 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

x is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
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 [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():] is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
f is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
y is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
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 [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
x is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
c6 is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
w1 is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
w2 is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
v1 is Relation-like [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
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 [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
[:(),():] is Relation-like set
[:[:(),():],():] is Relation-like set
bool [:[:(),():],():] is non empty set
multMagma(# (),(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 [:(),():] -defined Class Y -valued Function-like quasi_total Element of bool [:[:(),():],():]
[:(),():] is Relation-like set
[:[:(),():],():] is Relation-like set
bool [:[:(),():],():] is non empty set
multMagma(# (),(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 [:(),():] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(),():],():]
[:(),():] is non empty Relation-like set
[:[:(),():],():] is non empty Relation-like set
bool [:[:(),():],():] is non empty set
multMagma(# (),(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 [:(),():] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(),():],():]
[:(),():] is non empty Relation-like set
[:[:(),():],():] is non empty Relation-like set
bool [:[:(),():],():] is non empty set
multMagma(# (),(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

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 [:(),():] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(),():],():]
[:(),():] is non empty Relation-like set
[:[:(),():],():] is non empty Relation-like set
bool [:[:(),():],():] is non empty set
multMagma(# (),(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 [:(),():] -defined Class Y -valued Function-like total quasi_total Element of bool [:[:(),():],():]
[:(),():] is non empty Relation-like set
[:[:(),():],():] is non empty Relation-like set
bool [:[:(),():],():] is non empty set
multMagma(# (),(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

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

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

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

proj1 Y is set
meet Y is set
f is set
proj2 Y is set
meet () 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 () is set
proj2 Y is set
meet () 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