:: ALGSTR_4 semantic presentation

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

F

proj1 F

F

proj1 F

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

F

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

F

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

F

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

F

F

[:NAT,F

bool [:NAT,F

F

F

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

(F

F

F

F

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

(F

F

F

F

F

[:NAT,F

bool [:NAT,F

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

(F

F

Y is non empty Relation-like NAT -defined F

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 F

F

X . f is set

(F

F

[:[:{},{}:],{}:] 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

c

Class ((nabla the carrier of X),c

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 * c

the multF of X . (y,c

Class ((nabla the carrier of X),(y * c

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

c

Class (Y,c

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 * c

the multF of X . (y,c

Class (Y,(y * c

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 * c

the multF of X . (y,c

Class (Y,(y * c

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

c

Class (Y,c

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 * c

the multF of X . (y,c

Class (Y,(y * c

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

c

Class (Y,c

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

c

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):]

c

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 . (c

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

c

f . (x,c

y . (x,c

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

c

w9 is Element of the carrier of X

c

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 . (c

Class (Y,(c

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):]

c

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

c

Class (Y,c

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

c

Class (Y,c

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

{ b

for b

( not b

meet { b

for b

( not b

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

c

[x,c

{x,c

{x} is non empty trivial V41() V48(1) set

{{x,c

Class ((nabla the carrier of X),c

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

c

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:]

{ b

for b

( not b

meet { b

for b

( not b

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

{ b

for b

( not b

meet { b

for b

( not b

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

c

w1 is Element of the carrier of X

Class ((X,Y),w1) is Element of bool the carrier of X

y * c

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,c

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,c

{w1,c

{w1} is non empty trivial V41() V48(1) set

{{w1,c

[(x * w1),(y * c

{(x * w1),(y * c

{(x * w1)} is non empty trivial V41() V48(1) set

{{(x * w1),(y * c

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

c

f . c

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:]

c

w1 is set

[c

{c

{c

{{c

f . c

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

c

w1 is set

[c

{c

{c

{{c

f . c

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

c

Class (( the carrier of X, the carrier of Y,f),c

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

c

the multF of X . (c

Class (( the carrier of X, the carrier of Y,f),(c

[c

{c

{c

{{c

[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 . (c

f . c

(f . c

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 . c

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

[(c

{(c

{(c

{{(c

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

{ [b

id { [b

[: { [b

bool [: { [b

dom (id { [b

bool { [b

rng (id { [b

c

w1 is set

(id { [b

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

c

(Y,c

proj1 c

{ b

for b

( not b

meet { b

for b

( not b

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

c

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

c

w9 is Element of the carrier of Y

[c

{c

{c

{{c

f . c

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:]

c

w9 is Element of the carrier of Y

[c

{c

{c

{{c

c

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

c

x * c

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,c

[x,c

{x,c

{x} is non empty trivial V41() V48(1) set

{{x,c

the multF of Y . [x,c

the multF of X || the carrier of Y is Relation-like Function-like set

( the multF of X || the carrier of Y) . [x,c

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

c

Y . c

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

c

x * c

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,c

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

c

x * c

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,c

dom f is non empty Element of bool the carrier of Y

f . x is Element of the carrier of X

f . c

(f . x) * (f . c

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