K132() is set
bool K132() is set
{} is empty trivial Function-like functional set
dom {} is set
rng {} is set
C is non empty with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
C is non empty with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
C is non empty with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
C is non empty with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
C is non empty with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
idm o1 is Element of <^o1,o1^>
<^o1,o1^> is set
(idm o1) * (idm o1) is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
M1 is Element of <^o2,o1^>
M2 is Element of <^o2,o1^>
idm o1 is Element of <^o1,o1^>
<^o1,o1^> is set
(idm o1) * M1 is Element of <^o2,o1^>
M2 * o3 is Element of <^o1,o1^>
(M2 * o3) * M1 is Element of <^o2,o1^>
o3 * M1 is Element of <^o2,o2^>
<^o2,o2^> is set
M2 * (o3 * M1) is Element of <^o2,o1^>
idm o2 is Element of <^o2,o2^>
M2 * (idm o2) is Element of <^o2,o1^>
M1 is Element of <^o2,o1^>
M2 is Element of <^o2,o1^>
idm o2 is Element of <^o2,o2^>
<^o2,o2^> is set
M1 * (idm o2) is Element of <^o2,o1^>
o3 * M2 is Element of <^o2,o2^>
M1 * (o3 * M2) is Element of <^o2,o1^>
M1 * o3 is Element of <^o1,o1^>
<^o1,o1^> is set
(M1 * o3) * M2 is Element of <^o2,o1^>
idm o1 is Element of <^o1,o1^>
(idm o1) * M2 is Element of <^o2,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
idm o1 is Element of <^o1,o1^>
<^o1,o1^> is set
idm o2 is Element of <^o2,o2^>
<^o2,o2^> is set
o3 is Element of <^o1,o2^>
(C,o1,o2,o3) is Element of <^o2,o1^>
(C,o1,o2,o3) * o3 is Element of <^o1,o1^>
o3 * (C,o1,o2,o3) is Element of <^o2,o2^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
(C,o1,o2,o3) is Element of <^o2,o1^>
(C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o2^>
idm o2 is Element of <^o2,o2^>
<^o2,o2^> is set
(idm o2) * (C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o2^>
o3 * (C,o1,o2,o3) is Element of <^o2,o2^>
(o3 * (C,o1,o2,o3)) * (C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o2^>
(C,o1,o2,o3) * (C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o1^>
<^o1,o1^> is set
o3 * ((C,o1,o2,o3) * (C,o2,o1,(C,o1,o2,o3))) is Element of <^o1,o2^>
idm o1 is Element of <^o1,o1^>
o3 * (idm o1) is Element of <^o1,o2^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
idm o1 is Element of <^o1,o1^>
<^o1,o1^> is set
(C,o1,o1,(idm o1)) is Element of <^o1,o1^>
(C,o1,o1,(idm o1)) * (idm o1) is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of <^o1,o2^>
(C,o1,o2,o3) is Element of <^o2,o1^>
<^o2,o1^> is set
o3 * (C,o1,o2,o3) is Element of <^o2,o2^>
<^o2,o2^> is set
idm o2 is Element of <^o2,o2^>
(C,o1,o2,o3) * o3 is Element of <^o1,o1^>
<^o1,o1^> is set
idm o1 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
(C,o1,o2,o3) is Element of <^o2,o1^>
o3 * (C,o1,o2,o3) is Element of <^o2,o2^>
<^o2,o2^> is set
idm o2 is Element of <^o2,o2^>
(C,o1,o2,o3) * o3 is Element of <^o1,o1^>
<^o1,o1^> is set
idm o1 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
<^o3,o1^> is set
M1 is Element of <^o1,o2^>
(C,o1,o2,M1) is Element of <^o2,o1^>
<^o2,o1^> is set
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
(C,o1,o3,(M2 * M1)) is Element of <^o3,o1^>
(C,o2,o3,M2) is Element of <^o3,o2^>
<^o3,o2^> is set
(C,o1,o2,M1) * (C,o2,o3,M2) is Element of <^o3,o1^>
o is Element of <^o2,o1^>
B1 is Element of <^o3,o2^>
o * B1 is Element of <^o3,o1^>
(M2 * M1) * (o * B1) is Element of <^o3,o3^>
<^o3,o3^> is set
M1 * (o * B1) is Element of <^o3,o2^>
M2 * (M1 * (o * B1)) is Element of <^o3,o3^>
M1 * o is Element of <^o2,o2^>
<^o2,o2^> is set
(M1 * o) * B1 is Element of <^o3,o2^>
M2 * ((M1 * o) * B1) is Element of <^o3,o3^>
idm o2 is Element of <^o2,o2^>
(idm o2) * B1 is Element of <^o3,o2^>
M2 * ((idm o2) * B1) is Element of <^o3,o3^>
M2 * B1 is Element of <^o3,o3^>
idm o3 is Element of <^o3,o3^>
(o * B1) * (M2 * M1) is Element of <^o1,o1^>
<^o1,o1^> is set
B1 * (M2 * M1) is Element of <^o1,o2^>
o * (B1 * (M2 * M1)) is Element of <^o1,o1^>
B1 * M2 is Element of <^o2,o2^>
(B1 * M2) * M1 is Element of <^o1,o2^>
o * ((B1 * M2) * M1) is Element of <^o1,o1^>
(idm o2) * M1 is Element of <^o1,o2^>
o * ((idm o2) * M1) is Element of <^o1,o1^>
o * M1 is Element of <^o1,o1^>
idm o1 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o3 is Element of the U1 of C
<^o3,o3^> is set
idm o3 is Element of <^o3,o3^>
(C,o3,o3,(idm o3)) is Element of <^o3,o3^>
(C,o3,o3,(idm o3)) * (idm o3) is Element of <^o3,o3^>
(idm o3) * (idm o3) is Element of <^o3,o3^>
(idm o3) * (C,o3,o3,(idm o3)) is Element of <^o3,o3^>
o3 is Element of the U1 of C
M1 is Element of the U1 of C
<^o3,M1^> is set
<^M1,o3^> is set
M2 is Element of <^o3,M1^>
M2 is Element of <^o3,M1^>
(C,o3,M1,M2) is Element of <^M1,o3^>
o is Element of <^M1,o3^>
(C,M1,o3,o) is Element of <^o3,M1^>
(C,M1,o3,o) * o is Element of <^M1,M1^>
<^M1,M1^> is set
M2 * (C,o3,M1,M2) is Element of <^M1,M1^>
idm M1 is Element of <^M1,M1^>
o * (C,M1,o3,o) is Element of <^o3,o3^>
<^o3,o3^> is set
(C,o3,M1,M2) * M2 is Element of <^o3,o3^>
idm o3 is Element of <^o3,o3^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
o3 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o3^> is set
M1 is Element of <^o2,o3^>
M2 is Element of <^o1,o2^>
<^o2,o1^> is set
<^o3,o2^> is set
<^o1,o3^> is set
<^o3,o1^> is set
M1 * M2 is Element of <^o1,o3^>
C is non empty AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
C is non empty AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
C is non empty transitive associative AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of the U1 of C
<^o,o1^> is set
<^o,o2^> is set
B1 is Element of <^o,o1^>
(M2 * M1) * B1 is Element of <^o,o3^>
<^o,o3^> is set
A is Element of <^o,o1^>
(M2 * M1) * A is Element of <^o,o3^>
M1 * B1 is Element of <^o,o2^>
M2 * (M1 * B1) is Element of <^o,o3^>
M1 * A is Element of <^o,o2^>
M2 * (M1 * A) is Element of <^o,o3^>
C is non empty transitive associative AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of the U1 of C
<^o3,o^> is set
<^o2,o^> is set
B1 is Element of <^o3,o^>
B1 * (M2 * M1) is Element of <^o1,o^>
<^o1,o^> is set
A is Element of <^o3,o^>
A * (M2 * M1) is Element of <^o1,o^>
B1 * M2 is Element of <^o2,o^>
(B1 * M2) * M1 is Element of <^o1,o^>
A * M2 is Element of <^o2,o^>
(A * M2) * M1 is Element of <^o1,o^>
C is non empty transitive associative AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of the U1 of C
<^o,o1^> is set
B1 is Element of <^o,o1^>
M1 * B1 is Element of <^o,o2^>
<^o,o2^> is set
A is Element of <^o,o1^>
M1 * A is Element of <^o,o2^>
(M2 * M1) * B1 is Element of <^o,o3^>
<^o,o3^> is set
M2 * (M1 * B1) is Element of <^o,o3^>
(M2 * M1) * A is Element of <^o,o3^>
M2 * (M1 * A) is Element of <^o,o3^>
C is non empty transitive associative AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of the U1 of C
<^o3,o^> is set
B1 is Element of <^o3,o^>
B1 * M2 is Element of <^o2,o^>
<^o2,o^> is set
A is Element of <^o3,o^>
A * M2 is Element of <^o2,o^>
(B1 * M2) * M1 is Element of <^o1,o^>
<^o1,o^> is set
B1 * (M2 * M1) is Element of <^o1,o^>
(A * M2) * M1 is Element of <^o1,o^>
A * (M2 * M1) is Element of <^o1,o^>
C is non empty with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
idm o1 is Element of <^o1,o1^>
<^o1,o1^> is set
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of <^o1,o2^>
o3 * (idm o1) is Element of <^o1,o2^>
M1 is Element of <^o1,o2^>
M1 * (idm o1) is Element of <^o1,o2^>
o2 is Element of the U1 of C
<^o2,o1^> is set
o3 is Element of <^o2,o1^>
(idm o1) * o3 is Element of <^o2,o1^>
M1 is Element of <^o2,o1^>
(idm o1) * M1 is Element of <^o2,o1^>
C is non empty set
EnsCat C is non empty transitive strict quasi-functional semi-functional pseudo-functional associative with_units AltCatStr
the U1 of (EnsCat C) is set
o1 is Element of the U1 of (EnsCat C)
o2 is Element of the U1 of (EnsCat C)
<^o1,o2^> is set
[:o1,o2:] is set
bool [:o1,o2:] is set
o3 is Element of <^o1,o2^>
M1 is Relation-like o1 -defined o2 -valued Function-like quasi_total Element of bool [:o1,o2:]
dom M1 is set
o is set
B1 is set
M1 . o is set
M1 . B1 is set
o1 --> B1 is Relation-like o1 -defined {B1} -valued Function-like quasi_total Element of bool [:o1,{B1}:]
{B1} is non empty trivial set
[:o1,{B1}:] is set
bool [:o1,{B1}:] is set
o1 --> o is Relation-like o1 -defined {o} -valued Function-like quasi_total Element of bool [:o1,{o}:]
{o} is non empty trivial set
[:o1,{o}:] is set
bool [:o1,{o}:] is set
dom (o1 --> B1) is set
rng (o1 --> B1) is set
B2 is set
y is set
(o1 --> B1) . y is set
(o1 --> B1) * M1 is Relation-like Function-like set
dom ((o1 --> B1) * M1) is set
Funcs (o1,o1) is set
<^o1,o1^> is set
the Element of o1 is Element of o1
(o1 --> o) . the Element of o1 is set
(o1 --> B1) . the Element of o1 is set
dom (o1 --> o) is set
rng (o1 --> o) is set
A1 is set
x is set
(o1 --> o) . x is set
(o1 --> o) * M1 is Relation-like Function-like set
dom ((o1 --> o) * M1) is set
x is set
((o1 --> o) * M1) . x is set
(o1 --> o) . x is set
M1 . ((o1 --> o) . x) is set
(o1 --> B1) . x is set
M1 . ((o1 --> B1) . x) is set
((o1 --> B1) * M1) . x is set
A1 is Element of <^o1,o1^>
o3 * A1 is Element of <^o1,o2^>
B2 is Element of <^o1,o1^>
o3 * B2 is Element of <^o1,o2^>
M2 is Element of the U1 of (EnsCat C)
<^M2,o1^> is set
<^M2,o2^> is set
o is Element of <^M2,o1^>
o3 * o is Element of <^M2,o2^>
B1 is Element of <^M2,o1^>
o3 * B1 is Element of <^M2,o2^>
Funcs (M2,o1) is set
A is Relation-like Function-like set
dom A is set
rng A is set
B is Relation-like Function-like set
dom B is set
rng B is set
A * M1 is Relation-like Function-like set
B * M1 is Relation-like Function-like set
B2 is set
A . B2 is set
M1 . (A . B2) is set
(A * M1) . B2 is set
B . B2 is set
M1 . (B . B2) is set
Funcs (o1,o2) is set
the Element of Funcs (o1,o2) is Element of Funcs (o1,o2)
o is Element of the U1 of (EnsCat C)
<^o,o1^> is set
B1 is Relation-like Function-like set
dom B1 is set
rng B1 is set
A is Element of <^o,o1^>
o3 * A is Element of <^o,o2^>
<^o,o2^> is set
B is Element of <^o,o1^>
o3 * B is Element of <^o,o2^>
Funcs (o,o1) is set
B2 is Relation-like Function-like set
dom B2 is set
rng B2 is set
y is Relation-like Function-like set
dom y is set
rng y is set
C is non empty with_non-empty_elements non empty-membered set
EnsCat C is non empty transitive strict quasi-functional semi-functional pseudo-functional associative with_units AltCatStr
the U1 of (EnsCat C) is set
o1 is Element of the U1 of (EnsCat C)
o2 is Element of the U1 of (EnsCat C)
<^o1,o2^> is set
[:o1,o2:] is set
bool [:o1,o2:] is set
o3 is Element of <^o1,o2^>
M1 is Relation-like o1 -defined o2 -valued Function-like quasi_total Element of bool [:o1,o2:]
M2 is set
{M2} is non empty trivial set
dom M1 is set
rng M1 is set
o is set
{o} is non empty trivial set
M2 is Element of the U1 of (EnsCat C)
<^o2,M2^> is set
<^o1,M2^> is set
o is Element of <^o2,M2^>
o * o3 is Element of <^o1,M2^>
B1 is Element of <^o2,M2^>
B1 * o3 is Element of <^o1,M2^>
Funcs (o2,M2) is set
A is Relation-like Function-like set
dom A is set
rng A is set
B is Relation-like Function-like set
dom B is set
rng B is set
M1 * A is Relation-like Function-like set
M1 * B is Relation-like Function-like set
B2 is set
A . B2 is set
B . B2 is set
rng M1 is set
dom M1 is set
y is set
M1 . y is set
A . (M1 . y) is set
(M1 * A) . y is set
M2 is set
M2 is set
dom M1 is set
o is Element of the U1 of (EnsCat C)
the Element of o is Element of o
rng M1 is set
{ the Element of o} is non empty trivial set
o \ { the Element of o} is Element of bool o
bool o is set
B is set
o2 --> the Element of o is Relation-like o2 -defined { the Element of o} -valued Function-like quasi_total Element of bool [:o2,{ the Element of o}:]
[:o2,{ the Element of o}:] is set
bool [:o2,{ the Element of o}:] is set
dom (o2 --> the Element of o) is set
rng (o2 --> the Element of o) is set
y is set
A1 is set
(o2 --> the Element of o) . A1 is set
Funcs (o2,o) is set
<^o2,o^> is set
A is non empty set
the Element of A is Element of A
x is Element of o
z is Relation-like Function-like set
dom z is set
M1 * z is Relation-like Function-like set
dom (M1 * z) is set
rng z is set
A2 is set
z is set
z . z is set
IFEQ (z,B,x, the Element of o) is Element of o
IFEQ (z,B,x, the Element of o) is Element of o
rng (M1 * z) is set
z is set
Funcs (o1,o) is set
<^o1,o^> is set
z . B is set
IFEQ (B,B,x, the Element of o) is Element of o
M1 * (o2 --> the Element of o) is Relation-like Function-like set
dom (M1 * (o2 --> the Element of o)) is set
z is set
M1 . z is set
z . (M1 . z) is set
IFEQ ((M1 . z),B,x, the Element of o) is Element of o
(M1 * z) . z is set
(o2 --> the Element of o) . (M1 . z) is set
(M1 * (o2 --> the Element of o)) . z is set
A2 is Element of <^o2,o^>
A2 * o3 is Element of <^o1,o^>
y is Element of <^o2,o^>
y * o3 is Element of <^o1,o^>
B1 is Element of the U1 of (EnsCat C)
<^o2,B1^> is set
<^o1,B1^> is set
A is Element of <^o2,B1^>
A * o3 is Element of <^o1,B1^>
B is Element of <^o2,B1^>
B * o3 is Element of <^o1,B1^>
Funcs (o2,B1) is set
B2 is Relation-like Function-like set
dom B2 is set
rng B2 is set
y is Relation-like Function-like set
dom y is set
rng y is set
M1 * B2 is Relation-like Function-like set
M1 * y is Relation-like Function-like set
A1 is set
B2 . A1 is set
y . A1 is set
rng M1 is set
x is set
M1 . x is set
B2 . (M1 . x) is set
(M1 * B2) . x is set
M2 is Element of the U1 of (EnsCat C)
<^o2,M2^> is set
o is Element of <^o2,M2^>
o * o3 is Element of <^o1,M2^>
<^o1,M2^> is set
B1 is Element of <^o2,M2^>
B1 * o3 is Element of <^o1,M2^>
Funcs (o2,M2) is set
A is Relation-like Function-like set
dom A is set
rng A is set
B is Relation-like Function-like set
dom B is set
rng B is set
M2 is set
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
M1 is Element of <^o2,o1^>
M2 is Element of the U1 of C
<^o2,M2^> is set
o is Element of <^o2,M2^>
o * o3 is Element of <^o1,M2^>
<^o1,M2^> is set
B1 is Element of <^o2,M2^>
B1 * o3 is Element of <^o1,M2^>
idm o2 is Element of <^o2,o2^>
<^o2,o2^> is set
o * (idm o2) is Element of <^o2,M2^>
o3 * M1 is Element of <^o2,o2^>
o * (o3 * M1) is Element of <^o2,M2^>
(B1 * o3) * M1 is Element of <^o2,M2^>
B1 * (o3 * M1) is Element of <^o2,M2^>
B1 * (idm o2) is Element of <^o2,M2^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
M1 is Element of <^o2,o1^>
M2 is Element of the U1 of C
<^M2,o1^> is set
o is Element of <^M2,o1^>
o3 * o is Element of <^M2,o2^>
<^M2,o2^> is set
B1 is Element of <^M2,o1^>
o3 * B1 is Element of <^M2,o2^>
idm o1 is Element of <^o1,o1^>
<^o1,o1^> is set
(idm o1) * o is Element of <^M2,o1^>
M1 * o3 is Element of <^o1,o1^>
(M1 * o3) * o is Element of <^M2,o1^>
M1 * (o3 * B1) is Element of <^M2,o1^>
(M1 * o3) * B1 is Element of <^M2,o1^>
(idm o1) * B1 is Element of <^M2,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
M1 is Element of the U1 of C
<^o2,M1^> is set
M2 is Element of <^o2,M1^>
M2 * o3 is Element of <^o1,M1^>
<^o1,M1^> is set
o is Element of <^o2,M1^>
o * o3 is Element of <^o1,M1^>
(C,o1,o2,o3) is Element of <^o2,o1^>
o3 * (C,o1,o2,o3) is Element of <^o2,o2^>
<^o2,o2^> is set
M2 * (o3 * (C,o1,o2,o3)) is Element of <^o2,M1^>
(o * o3) * (C,o1,o2,o3) is Element of <^o2,M1^>
idm o2 is Element of <^o2,o2^>
M2 * (idm o2) is Element of <^o2,M1^>
o * (o3 * (C,o1,o2,o3)) is Element of <^o2,M1^>
o * (idm o2) is Element of <^o2,M1^>
M1 is Element of the U1 of C
<^M1,o1^> is set
M2 is Element of <^M1,o1^>
o3 * M2 is Element of <^M1,o2^>
<^M1,o2^> is set
o is Element of <^M1,o1^>
o3 * o is Element of <^M1,o2^>
(C,o1,o2,o3) is Element of <^o2,o1^>
(C,o1,o2,o3) * o3 is Element of <^o1,o1^>
<^o1,o1^> is set
((C,o1,o2,o3) * o3) * M2 is Element of <^M1,o1^>
(C,o1,o2,o3) * (o3 * o) is Element of <^M1,o1^>
idm o1 is Element of <^o1,o1^>
(idm o1) * M2 is Element of <^M1,o1^>
((C,o1,o2,o3) * o3) * o is Element of <^M1,o1^>
(idm o1) * o is Element of <^M1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
<^o3,o1^> is set
<^o2,o1^> is set
<^o3,o2^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of <^o2,o1^>
B1 is Element of <^o3,o2^>
o * B1 is Element of <^o3,o1^>
A is Element of <^o3,o1^>
(M2 * M1) * A is Element of <^o3,o3^>
<^o3,o3^> is set
M1 * (o * B1) is Element of <^o3,o2^>
M2 * (M1 * (o * B1)) is Element of <^o3,o3^>
M1 * o is Element of <^o2,o2^>
<^o2,o2^> is set
(M1 * o) * B1 is Element of <^o3,o2^>
M2 * ((M1 * o) * B1) is Element of <^o3,o3^>
idm o2 is Element of <^o2,o2^>
(idm o2) * B1 is Element of <^o3,o2^>
M2 * ((idm o2) * B1) is Element of <^o3,o3^>
M2 * B1 is Element of <^o3,o3^>
idm o3 is Element of <^o3,o3^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
<^o3,o1^> is set
<^o2,o1^> is set
<^o3,o2^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of <^o2,o1^>
B1 is Element of <^o3,o2^>
o * B1 is Element of <^o3,o1^>
A is Element of <^o3,o1^>
<^o2,o2^> is set
A * (M2 * M1) is Element of <^o1,o1^>
<^o1,o1^> is set
(o * B1) * M2 is Element of <^o2,o1^>
((o * B1) * M2) * M1 is Element of <^o1,o1^>
B1 * M2 is Element of <^o2,o2^>
o * (B1 * M2) is Element of <^o2,o1^>
(o * (B1 * M2)) * M1 is Element of <^o1,o1^>
idm o2 is Element of <^o2,o2^>
o * (idm o2) is Element of <^o2,o1^>
(o * (idm o2)) * M1 is Element of <^o1,o1^>
(idm o2) * M1 is Element of <^o1,o2^>
o * ((idm o2) * M1) is Element of <^o1,o1^>
o * M1 is Element of <^o1,o1^>
idm o1 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
M1 is Element of <^o2,o1^>
o3 * M1 is Element of <^o2,o2^>
<^o2,o2^> is set
(o3 * M1) * o3 is Element of <^o1,o2^>
idm o2 is Element of <^o2,o2^>
(idm o2) * o3 is Element of <^o1,o2^>
M1 * o3 is Element of <^o1,o1^>
<^o1,o1^> is set
o3 * (M1 * o3) is Element of <^o1,o2^>
idm o1 is Element of <^o1,o1^>
o3 * (idm o1) is Element of <^o1,o2^>
(C,o1,o2,o3) is Element of <^o2,o1^>
o3 * (C,o1,o2,o3) is Element of <^o2,o2^>
(C,o1,o2,o3) * o3 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
M1 is Element of <^o2,o1^>
M1 * o3 is Element of <^o1,o1^>
<^o1,o1^> is set
o3 * (M1 * o3) is Element of <^o1,o2^>
idm o1 is Element of <^o1,o1^>
o3 * (idm o1) is Element of <^o1,o2^>
idm o2 is Element of <^o2,o2^>
<^o2,o2^> is set
(idm o2) * o3 is Element of <^o1,o2^>
o3 * M1 is Element of <^o2,o2^>
(o3 * M1) * o3 is Element of <^o1,o2^>
(C,o1,o2,o3) is Element of <^o2,o1^>
(C,o1,o2,o3) * o3 is Element of <^o1,o1^>
o3 * (C,o1,o2,o3) is Element of <^o2,o2^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
<^o3,o1^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of <^o3,o1^>
(M2 * M1) * o is Element of <^o3,o3^>
<^o3,o3^> is set
idm o3 is Element of <^o3,o3^>
M1 * o is Element of <^o3,o2^>
<^o3,o2^> is set
M2 * (M1 * o) is Element of <^o3,o3^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
<^o3,o1^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of <^o3,o1^>
o * M2 is Element of <^o2,o1^>
<^o2,o1^> is set
(o * M2) * M1 is Element of <^o1,o1^>
<^o1,o1^> is set
o * (M2 * M1) is Element of <^o1,o1^>
idm o1 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
<^o2,o1^> is set
o3 is Element of <^o1,o2^>
M1 is Element of <^o2,o1^>
o3 * M1 is Element of <^o2,o2^>
<^o2,o2^> is set
M1 * (o3 * M1) is Element of <^o2,o1^>
idm o2 is Element of <^o2,o2^>
M1 * (idm o2) is Element of <^o2,o1^>
M1 * o3 is Element of <^o1,o1^>
<^o1,o1^> is set
(M1 * o3) * M1 is Element of <^o2,o1^>
idm o1 is Element of <^o1,o1^>
(idm o1) * M1 is Element of <^o2,o1^>
C is non empty with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
<^o1,o1^> is set
idm o1 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
<^o1,o1^> is set
idm o1 is Element of <^o1,o1^>
o2 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
<^o1,o1^> is set
o3 is (C,o1,o1) Element of <^o1,o1^>
o2 is (C,o1,o1) Element of <^o1,o1^>
o2 * o3 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
<^o1,o1^> is set
o3 is (C,o1,o1) Element of <^o1,o1^>
o2 is (C,o1,o1) Element of <^o1,o1^>
o2 * o3 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
<^o1,o1^> is set
o3 is (C,o1,o1) Element of <^o1,o1^>
o2 is (C,o1,o1) Element of <^o1,o1^>
o2 * o3 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
<^o1,o1^> is set
o3 is (C,o1,o1) Element of <^o1,o1^>
o2 is (C,o1,o1) Element of <^o1,o1^>
o2 * o3 is Element of <^o1,o1^>
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
<^o1,o1^> is set
o3 is (C,o1,o1) Element of <^o1,o1^>
o2 is (C,o1,o1) Element of <^o1,o1^>
o2 * o3 is Element of <^o1,o1^>
C is AltGraph
the U1 of C is set
C is AltGraph
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of <^o1,o2^>
{o3} is non empty trivial set
M1 is set
{M1} is non empty trivial set
M1 is Element of <^o1,o2^>
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of <^o1,o2^>
{o3} is non empty trivial set
M1 is set
M2 is Element of <^o1,o2^>
M1 is set
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o2,o2^> is set
o3 is Element of <^o2,o2^>
o3 is set
{o3} is non empty trivial set
<^o2,o1^> is set
M1 is Element of <^o2,o1^>
<^o1,o2^> is set
M2 is Element of <^o1,o2^>
M2 * M1 is Element of <^o2,o2^>
idm o2 is Element of <^o2,o2^>
<^o1,o1^> is set
o is Element of <^o1,o1^>
o is set
{o} is non empty trivial set
M1 * M2 is Element of <^o1,o1^>
idm o1 is Element of <^o1,o1^>
C is AltGraph
the U1 of C is set
C is AltGraph
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o2,o1^> is set
o3 is Element of <^o2,o1^>
{o3} is non empty trivial set
M1 is set
{M1} is non empty trivial set
M1 is Element of <^o2,o1^>
o2 is Element of the U1 of C
<^o2,o1^> is set
o3 is Element of <^o2,o1^>
{o3} is non empty trivial set
M1 is set
M2 is Element of <^o2,o1^>
M1 is set
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o1^> is set
o3 is Element of <^o1,o1^>
o3 is set
{o3} is non empty trivial set
<^o2,o1^> is set
M1 is Element of <^o2,o1^>
<^o1,o2^> is set
M2 is Element of <^o1,o2^>
M1 * M2 is Element of <^o1,o1^>
idm o1 is Element of <^o1,o1^>
<^o2,o2^> is set
o is Element of <^o2,o2^>
o is set
{o} is non empty trivial set
M2 * M1 is Element of <^o2,o2^>
idm o2 is Element of <^o2,o2^>
C is AltGraph
the U1 of C is set
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
C is non empty AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
C is non empty transitive associative with_units AltCatStr
the U1 of C is set
o1 is Element of the U1 of C
o2 is Element of the U1 of C
<^o1,o2^> is set
o3 is Element of the U1 of C
<^o2,o3^> is set
M1 is Element of <^o1,o2^>
M2 is Element of <^o2,o3^>
M2 * M1 is Element of <^o1,o3^>
<^o1,o3^> is set
o is Element of the U1 of C
<^o1,o^> is set
<^o,o3^> is set
<^o,o2^> is set
B1 is Element of <^o,o2^>
A is Element of <^o1,o^>
B is Element of <^o,o3^>
B * A is Element of <^o1,o3^>
B2 is Element of <^o,o3^>
y is set
{y} is non empty trivial set
A1 is Element of <^o1,o^>
x is set
{x} is non empty trivial set
<^o,o^> is set
z is Element of <^o,o^>
z is set
{z} is non empty trivial set
<^o2,o^> is set
A2 is Element of <^o2,o^>
idm o is Element of <^o,o^>
A2 * B1 is Element of <^o,o^>
B2 * A2 is Element of <^o2,o3^>
B1 * A1 is Element of <^o1,o2^>
(B2 * A2) * (B1 * A1) is Element of <^o1,o3^>
(B2 * A2) * B1 is Element of <^o,o3^>
((B2 * A2) * B1) * A1 is Element of <^o1,o3^>
B * (idm o) is Element of <^o,o3^>
(B * (idm o)) * A is Element of <^o1,o3^>