:: YELLOW18 semantic presentation

NAT is non empty V15() V16() V17() Element of bool REAL

REAL is set

bool REAL is non empty set

NAT is non empty V15() V16() V17() set

bool NAT is non empty set

bool NAT is non empty set

K145() is Element of bool NAT

[:NAT,K145():] is Relation-like set

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

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() Function-yielding V63() set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() Function-yielding V63() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V15() V16() V17() V19() V20() V21() Function-yielding V63() set

1 is non empty set

{{},1} is non empty set

F

[:F

A is Relation-like [:F

{|A,A|} is Relation-like [:F

[:F

{|A|} is Relation-like [:F

c

FF is set

a is set

b is set

[FF,a,b] is V22() V23() set

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

[[FF,a],b] is V22() set

{[FF,a],b} is non empty set

{[FF,a]} is Relation-like Function-like non empty set

{{[FF,a],b},{[FF,a]}} is non empty set

c is Element of F

d is Element of F

f is Element of F

F

F

[:F

F

fa is set

fb is set

g is set

[fb,g] is V22() set

{fb,g} is non empty set

{fb} is non empty set

{{fb,g},{fb}} is non empty set

F

g is set

fa is Relation-like Function-like set

proj1 fa is set

proj2 fa is set

A . (c,d) is set

[c,d] is V22() set

{c,d} is non empty set

{c} is non empty set

{{c,d},{c}} is non empty set

A . [c,d] is set

A . (d,f) is set

[d,f] is V22() set

{d,f} is non empty set

{d} is non empty set

{{d,f},{d}} is non empty set

A . [d,f] is set

A . (c,f) is set

[c,f] is V22() set

{c,f} is non empty set

{{c,f},{c}} is non empty set

A . [c,f] is set

{|A,A|} . (c,d,f) is set

{|A|} . (c,d,f) is set

[:({|A,A|} . (c,d,f)),({|A|} . (c,d,f)):] is Relation-like set

bool [:({|A,A|} . (c,d,f)),({|A|} . (c,d,f)):] is non empty set

fb is Relation-like {|A,A|} . (c,d,f) -defined {|A|} . (c,d,f) -valued Function-like quasi_total Element of bool [:({|A,A|} . (c,d,f)),({|A|} . (c,d,f)):]

g is Relation-like {|A,A|} . (c,d,f) -defined {|A|} . (c,d,f) -valued Function-like quasi_total Element of bool [:({|A,A|} . (c,d,f)),({|A|} . (c,d,f)):]

[c,d,f] is V22() V23() set

[[c,d],f] is V22() set

{[c,d],f} is non empty set

{[c,d]} is Relation-like Function-like non empty set

{{[c,d],f},{[c,d]}} is non empty set

g is set

c

[c

{c

{c

{{c

fb . [c

F

a1 is set

g9 is set

[a1,g9] is V22() set

{a1,g9} is non empty set

{a1} is non empty set

{{a1,g9},{a1}} is non empty set

F

c

proj1 c

a is set

FF is Relation-like [:F

FF . a is set

b is Element of F

c is Element of F

d is Element of F

{|A,A|} . (b,c,d) is set

{|A|} . (b,c,d) is set

[:({|A,A|} . (b,c,d)),({|A|} . (b,c,d)):] is Relation-like set

bool [:({|A,A|} . (b,c,d)),({|A|} . (b,c,d)):] is non empty set

[b,c,d] is V22() V23() set

[b,c] is V22() set

{b,c} is non empty set

{b} is non empty set

{{b,c},{b}} is non empty set

[[b,c],d] is V22() set

{[b,c],d} is non empty set

{[b,c]} is Relation-like Function-like non empty set

{{[b,c],d},{[b,c]}} is non empty set

f is Relation-like {|A,A|} . (b,c,d) -defined {|A|} . (b,c,d) -valued Function-like quasi_total Element of bool [:({|A,A|} . (b,c,d)),({|A|} . (b,c,d)):]

F

F

{|A|} . a is set

{|A,A|} . a is set

[:({|A,A|} . a),({|A|} . a):] is Relation-like set

bool [:({|A,A|} . a),({|A|} . a):] is non empty set

a is Relation-like [:F

AltCatStr(# F

the carrier of AltCatStr(# F

c is Element of the carrier of AltCatStr(# F

d is Element of the carrier of AltCatStr(# F

<^c,d^> is set

the Arrows of AltCatStr(# F

[: the carrier of AltCatStr(# F

the Arrows of AltCatStr(# F

[c,d] is V22() set

{c,d} is non empty set

{c} is non empty set

{{c,d},{c}} is non empty set

the Arrows of AltCatStr(# F

f is Element of the carrier of AltCatStr(# F

<^d,f^> is set

the Arrows of AltCatStr(# F

[d,f] is V22() set

{d,f} is non empty set

{d} is non empty set

{{d,f},{d}} is non empty set

the Arrows of AltCatStr(# F

<^c,f^> is set

the Arrows of AltCatStr(# F

[c,f] is V22() set

{c,f} is non empty set

{{c,f},{c}} is non empty set

the Arrows of AltCatStr(# F

the Element of <^c,d^> is Element of <^c,d^>

the Element of <^d,f^> is Element of <^d,f^>

fa is Element of F

fb is Element of F

F

g is Element of F

F

F

F

c is non empty transitive strict AltCatStr

the carrier of c is non empty set

d is Element of the carrier of c

f is Element of the carrier of c

<^d,f^> is set

the Arrows of c is Relation-like [: the carrier of c, the carrier of c:] -defined Function-like non empty V14([: the carrier of c, the carrier of c:]) set

[: the carrier of c, the carrier of c:] is Relation-like non empty set

the Arrows of c . (d,f) is set

[d,f] is V22() set

{d,f} is non empty set

{d} is non empty set

{{d,f},{d}} is non empty set

the Arrows of c . [d,f] is set

F

d is Element of the carrier of c

f is Element of the carrier of c

<^d,f^> is set

the Arrows of c is Relation-like [: the carrier of c, the carrier of c:] -defined Function-like non empty V14([: the carrier of c, the carrier of c:]) set

[: the carrier of c, the carrier of c:] is Relation-like non empty set

the Arrows of c . (d,f) is set

[d,f] is V22() set

{d,f} is non empty set

{d} is non empty set

{{d,f},{d}} is non empty set

the Arrows of c . [d,f] is set

fa is Element of the carrier of c

<^f,fa^> is set

the Arrows of c . (f,fa) is set

[f,fa] is V22() set

{f,fa} is non empty set

{f} is non empty set

{{f,fa},{f}} is non empty set

the Arrows of c . [f,fa] is set

[d,f,fa] is V22() V23() set

[[d,f],fa] is V22() set

{[d,f],fa} is non empty set

{[d,f]} is Relation-like Function-like non empty set

{{[d,f],fa},{[d,f]}} is non empty set

a . [d,f,fa] is Relation-like Function-like set

fb is Element of F

g is Element of F

g is Element of F

{|A,A|} . (fb,g,g) is set

{|A|} . (fb,g,g) is set

[:({|A,A|} . (fb,g,g)),({|A|} . (fb,g,g)):] is Relation-like set

bool [:({|A,A|} . (fb,g,g)),({|A|} . (fb,g,g)):] is non empty set

[fb,g,g] is V22() V23() set

[fb,g] is V22() set

{fb,g} is non empty set

{fb} is non empty set

{{fb,g},{fb}} is non empty set

[[fb,g],g] is V22() set

{[fb,g],g} is non empty set

{[fb,g]} is Relation-like Function-like non empty set

{{[fb,g],g},{[fb,g]}} is non empty set

c

F

F

g9 is Element of <^d,f^>

a1 is Element of <^f,fa^>

a1 * g9 is Element of <^d,fa^>

<^d,fa^> is set

the Arrows of c . (d,fa) is set

[d,fa] is V22() set

{d,fa} is non empty set

{{d,fa},{d}} is non empty set

the Arrows of c . [d,fa] is set

F

F

F

[a1,g9] is V22() set

{a1,g9} is non empty set

{a1} is non empty set

{{a1,g9},{a1}} is non empty set

c

the Comp of c is Relation-like [: the carrier of c, the carrier of c, the carrier of c:] -defined Function-like non empty V14([: the carrier of c, the carrier of c, the carrier of c:]) Function-yielding V63() ManySortedFunction of {| the Arrows of c, the Arrows of c|},{| the Arrows of c|}

[: the carrier of c, the carrier of c, the carrier of c:] is non empty set

{| the Arrows of c, the Arrows of c|} is Relation-like [: the carrier of c, the carrier of c, the carrier of c:] -defined Function-like non empty V14([: the carrier of c, the carrier of c, the carrier of c:]) set

{| the Arrows of c|} is Relation-like [: the carrier of c, the carrier of c, the carrier of c:] -defined Function-like non empty V14([: the carrier of c, the carrier of c, the carrier of c:]) set

the Comp of c . (d,f,fa) is Relation-like [:( the Arrows of c . (f,fa)),( the Arrows of c . (d,f)):] -defined the Arrows of c . (d,fa) -valued Function-like quasi_total Element of bool [:[:( the Arrows of c . (f,fa)),( the Arrows of c . (d,f)):],( the Arrows of c . (d,fa)):]

[:( the Arrows of c . (f,fa)),( the Arrows of c . (d,f)):] is Relation-like set

[:[:( the Arrows of c . (f,fa)),( the Arrows of c . (d,f)):],( the Arrows of c . (d,fa)):] is Relation-like set

bool [:[:( the Arrows of c . (f,fa)),( the Arrows of c . (d,f)):],( the Arrows of c . (d,fa)):] is non empty set

( the Comp of c . (d,f,fa)) . (a1,g9) is set

( the Comp of c . (d,f,fa)) . [a1,g9] is set

F

the carrier of F

the Arrows of F

[: the carrier of F

A is Element of the carrier of F

c

the Arrows of F

[A,c

{A,c

{A} is non empty set

{{A,c

the Arrows of F

FF is Element of the carrier of F

the Arrows of F

[c

{c

{c

{{c

the Arrows of F

a is Element of the carrier of F

the Arrows of F

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

the Arrows of F

the Comp of F

[: the carrier of F

{| the Arrows of F

{| the Arrows of F

the Comp of F

the Arrows of F

[A,FF] is V22() set

{A,FF} is non empty set

{{A,FF},{A}} is non empty set

the Arrows of F

[:( the Arrows of F

the Arrows of F

[A,a] is V22() set

{A,a} is non empty set

{{A,a},{A}} is non empty set

the Arrows of F

[:[:( the Arrows of F

bool [:[:( the Arrows of F

the Comp of F

[:( the Arrows of F

[:[:( the Arrows of F

bool [:[:( the Arrows of F

the Comp of F

the Arrows of F

[c

{c

{{c

the Arrows of F

[:( the Arrows of F

[:[:( the Arrows of F

bool [:[:( the Arrows of F

the Comp of F

[:( the Arrows of F

[:[:( the Arrows of F

bool [:[:( the Arrows of F

g is set

c

g9 is set

( the Comp of F

[c

{c

{c

{{c

( the Comp of F

( the Comp of F

[g9,(( the Comp of F

{g9,(( the Comp of F

{g9} is non empty set

{{g9,(( the Comp of F

( the Comp of F

( the Comp of F

[g9,c

{g9,c

{{g9,c

( the Comp of F

( the Comp of F

[(( the Comp of F

{(( the Comp of F

{(( the Comp of F

{{(( the Comp of F

( the Comp of F

f is Element of the carrier of F

fa is Element of the carrier of F

<^f,fa^> is set

the Arrows of F

[f,fa] is V22() set

{f,fa} is non empty set

{f} is non empty set

{{f,fa},{f}} is non empty set

the Arrows of F

fb is Element of the carrier of F

<^fa,fb^> is set

the Arrows of F

[fa,fb] is V22() set

{fa,fb} is non empty set

{fa} is non empty set

{{fa,fb},{fa}} is non empty set

the Arrows of F

g is Element of the carrier of F

<^fb,g^> is set

the Arrows of F

[fb,g] is V22() set

{fb,g} is non empty set

{fb} is non empty set

{{fb,g},{fb}} is non empty set

the Arrows of F

<^f,fb^> is set

the Arrows of F

[f,fb] is V22() set

{f,fb} is non empty set

{{f,fb},{f}} is non empty set

the Arrows of F

<^fa,g^> is set

the Arrows of F

[fa,g] is V22() set

{fa,g} is non empty set

{{fa,g},{fa}} is non empty set

the Arrows of F

a1 is Element of <^f,fa^>

b1 is Element of <^fa,fb^>

b1 * a1 is Element of <^f,fb^>

( the Comp of F

[g9,(b1 * a1)] is V22() set

{g9,(b1 * a1)} is non empty set

{{g9,(b1 * a1)},{g9}} is non empty set

( the Comp of F

f1 is Element of <^fb,g^>

f1 * (b1 * a1) is Element of <^f,g^>

<^f,g^> is set

the Arrows of F

[f,g] is V22() set

{f,g} is non empty set

{{f,g},{f}} is non empty set

the Arrows of F

F

F

F

F

F

f1 * b1 is Element of <^fa,g^>

F

(f1 * b1) * a1 is Element of <^f,g^>

( the Comp of F

[(f1 * b1),g] is V22() set

{(f1 * b1),g} is non empty set

{(f1 * b1)} is non empty set

{{(f1 * b1),g},{(f1 * b1)}} is non empty set

( the Comp of F

F

the carrier of F

the Comp of F

[: the carrier of F

the Arrows of F

[: the carrier of F

{| the Arrows of F

{| the Arrows of F

b is Element of the carrier of F

c is Element of the carrier of F

<^c,c^> is set

the Arrows of F

[c,c] is V22() set

{c,c} is non empty set

{c} is non empty set

{{c,c},{c}} is non empty set

the Arrows of F

d is set

f is set

the Arrows of F

[b,b] is V22() set

{b,b} is non empty set

{b} is non empty set

{{b,b},{b}} is non empty set

the Arrows of F

fb is set

fa is Element of the carrier of F

the Arrows of F

[fa,b] is V22() set

{fa,b} is non empty set

{fa} is non empty set

{{fa,b},{fa}} is non empty set

the Arrows of F

g is Element of the carrier of F

<^g,c^> is set

the Arrows of F

[g,c] is V22() set

{g,c} is non empty set

{g} is non empty set

{{g,c},{g}} is non empty set

the Arrows of F

F

the Comp of F

[:( the Arrows of F

[:[:( the Arrows of F

bool [:[:( the Arrows of F

( the Comp of F

[f,fb] is V22() set

{f,fb} is non empty set

{f} is non empty set

{{f,fb},{f}} is non empty set

( the Comp of F

c

g is Element of <^c,c^>

g * c

b is Element of the carrier of F

the Arrows of F

[b,b] is V22() set

{b,b} is non empty set

{b} is non empty set

{{b,b},{b}} is non empty set

the Arrows of F

c is Element of the carrier of F

<^c,c^> is set

the Arrows of F

[c,c] is V22() set

{c,c} is non empty set

{c} is non empty set

{{c,c},{c}} is non empty set

the Arrows of F

d is set

fa is Element of the carrier of F

the Arrows of F

[b,fa] is V22() set

{b,fa} is non empty set

{{b,fa},{b}} is non empty set

the Arrows of F

the Comp of F

[:( the Arrows of F

[:[:( the Arrows of F

bool [:[:( the Arrows of F

fb is set

( the Comp of F

[fb,d] is V22() set

{fb,d} is non empty set

{fb} is non empty set

{{fb,d},{fb}} is non empty set

( the Comp of F

g is Element of the carrier of F

<^c,g^> is set

the Arrows of F

[c,g] is V22() set

{c,g} is non empty set

{{c,g},{c}} is non empty set

the Arrows of F

F

f is Element of <^c,c^>

g is Element of <^c,g^>

g * f is Element of <^c,g^>

F

a is set

A is Element of F

c

F

b is set

FF is Element of F

F

F

F

A is non empty transitive strict AltCatStr

the carrier of A is non empty set

c

FF is Element of the carrier of A

<^c

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the Arrows of A . (c

[c

{c

{c

{{c

the Arrows of A . [c

a is Element of the carrier of A

<^FF,a^> is set

the Arrows of A . (FF,a) is set

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

the Arrows of A . [FF,a] is set

b is Element of the carrier of A

<^a,b^> is set

the Arrows of A . (a,b) is set

[a,b] is V22() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

the Arrows of A . [a,b] is set

c is set

d is set

f is set

F

F

F

F

F

F

F

c

<^c

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the Arrows of A . (c

[c

{c

{c

{{c

the Arrows of A . [c

F

FF is set

a is Element of the carrier of A

<^c

the Arrows of A . (c

[c

{c

{{c

the Arrows of A . [c

F

b is set

F

c

<^c

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the Arrows of A . (c

[c

{c

{c

{{c

the Arrows of A . [c

F

FF is set

a is Element of the carrier of A

<^a,c

the Arrows of A . (a,c

[a,c

{a,c

{a} is non empty set

{{a,c

the Arrows of A . [a,c

F

b is set

F

F

A is non empty transitive AltCatStr

the carrier of A is non empty set

c

the carrier of c

the Arrows of A is Relation-like [: the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A:]) set

[: the carrier of A, the carrier of A:] is Relation-like non empty set

the Comp of A is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A, the carrier of A:]) Function-yielding V63() ManySortedFunction of {| the Arrows of A, the Arrows of A|},{| the Arrows of A|}

[: the carrier of A, the carrier of A, the carrier of A:] is non empty set

{| the Arrows of A, the Arrows of A|} is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A, the carrier of A:]) set

{| the Arrows of A|} is Relation-like [: the carrier of A, the carrier of A, the carrier of A:] -defined Function-like non empty V14([: the carrier of A, the carrier of A, the carrier of A:]) set

AltCatStr(# the carrier of A, the Arrows of A, the Comp of A #) is non empty strict AltCatStr

the Arrows of c

[: the carrier of c

the Comp of c

[: the carrier of c

{| the Arrows of c

{| the Arrows of c

AltCatStr(# the carrier of c

FF is set

[:F

a is set

b is set

[a,b] is V22() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

the Arrows of A . FF is set

c is Element of the carrier of A

d is Element of the carrier of A

<^c,d^> is set

the Arrows of A . (c,d) is set

[c,d] is V22() set

{c,d} is non empty set

{c} is non empty set

{{c,d},{c}} is non empty set

the Arrows of A . [c,d] is set

F

f is Element of the carrier of c

fa is Element of the carrier of c

<^f,fa^> is set

the Arrows of c

[f,fa] is V22() set

{f,fa} is non empty set

{f} is non empty set

{{f,fa},{f}} is non empty set

the Arrows of c

the Arrows of c

FF is set

[:F

a is set

b is set

c is set

[a,b,c] is V22() V23() set

[a,b] is V22() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

[[a,b],c] is V22() set

{[a,b],c} is non empty set

{[a,b]} is Relation-like Function-like non empty set

{{[a,b],c},{[a,b]}} is non empty set

the Comp of A . FF is Relation-like Function-like set

d is Element of the carrier of A

f is Element of the carrier of A

fa is Element of the carrier of A

the Comp of A . (d,f,fa) is Relation-like [:( the Arrows of A . (f,fa)),( the Arrows of A . (d,f)):] -defined the Arrows of A . (d,fa) -valued Function-like quasi_total Element of bool [:[:( the Arrows of A . (f,fa)),( the Arrows of A . (d,f)):],( the Arrows of A . (d,fa)):]

the Arrows of A . (f,fa) is set

[f,fa] is V22() set

{f,fa} is non empty set

{f} is non empty set

{{f,fa},{f}} is non empty set

the Arrows of A . [f,fa] is set

the Arrows of A . (d,f) is set

[d,f] is V22() set

{d,f} is non empty set

{d} is non empty set

{{d,f},{d}} is non empty set

the Arrows of A . [d,f] is set

[:( the Arrows of A . (f,fa)),( the Arrows of A . (d,f)):] is Relation-like set

the Arrows of A . (d,fa) is set

[d,fa] is V22() set

{d,fa} is non empty set

{{d,fa},{d}} is non empty set

the Arrows of A . [d,fa] is set

[:[:( the Arrows of A . (f,fa)),( the Arrows of A . (d,f)):],( the Arrows of A . (d,fa)):] is Relation-like set

bool [:[:( the Arrows of A . (f,fa)),( the Arrows of A . (d,f)):],( the Arrows of A . (d,fa)):] is non empty set

the Comp of c

fb is Element of the carrier of c

g is Element of the carrier of c

g is Element of the carrier of c

the Comp of c

the Arrows of c

[g,g] is V22() set

{g,g} is non empty set

{g} is non empty set

{{g,g},{g}} is non empty set

the Arrows of c

the Arrows of c

[fb,g] is V22() set

{fb,g} is non empty set

{fb} is non empty set

{{fb,g},{fb}} is non empty set

the Arrows of c

[:( the Arrows of c

the Arrows of c

[fb,g] is V22() set

{fb,g} is non empty set

{{fb,g},{fb}} is non empty set

the Arrows of c

[:[:( the Arrows of c

bool [:[:( the Arrows of c

<^f,fa^> is set

<^d,f^> is set

[:<^f,fa^>,<^d,f^>:] is Relation-like set

<^d,fa^> is set

dom ( the Comp of A . (d,f,fa)) is Relation-like the Arrows of A . (f,fa) -defined the Arrows of A . (d,f) -valued Element of bool [:( the Arrows of A . (f,fa)),( the Arrows of A . (d,f)):]

bool [:( the Arrows of A . (f,fa)),( the Arrows of A . (d,f)):] is non empty set

dom ( the Comp of c

bool [:( the Arrows of c

c

g9 is set

a1 is set

[g9,a1] is V22() set

{g9,a1} is non empty set

{g9} is non empty set

{{g9,a1},{g9}} is non empty set

<^g,g^> is set

b1 is Element of <^f,fa^>

<^fb,g^> is set

f1 is Element of <^d,f^>

( the Comp of A . (d,f,fa)) . c

( the Comp of A . (d,f,fa)) . (b1,f1) is set

[b1,f1] is V22() set

{b1,f1} is non empty set

{b1} is non empty set

{{b1,f1},{b1}} is non empty set

( the Comp of A . (d,f,fa)) . [b1,f1] is set

b1 * f1 is Element of <^d,fa^>

F

b2 is Element of <^fb,g^>

G1 is Element of <^g,g^>

G1 * b2 is Element of <^fb,g^>

<^fb,g^> is set

( the Comp of c

[G1,b2] is V22() set

{G1,b2} is non empty set

{G1} is non empty set

{{G1,b2},{G1}} is non empty set

( the Comp of c

( the Comp of c

F

[:F

A is Relation-like Function-like set

proj1 A is set

c

FF is Element of F

[c

{c

{c

{{c

[c

[c

a is set

A . (c

A . [c

F

b is set

c

FF is Element of F

A . (c

[c

{c

{c

{{c

A . [c

c is set

a is Element of F

A . (FF,a) is set

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

A . [FF,a] is set

F

F

F

F

A . (c

[c

{c

{{c

A . [c

c is set

c

FF is Element of F

A . (c

[c

{c

{c

{{c

A . [c

d is set

a is Element of F

A . (FF,a) is set

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

A . [FF,a] is set

f is set

b is Element of F

A . (a,b) is set

[a,b] is V22() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

A . [a,b] is set

F

F

F

F

F

F

F

c

F

FF is set

a is set

A . (c

[c

{c

{c

{{c

A . [c

c is set

b is Element of F

A . (c

[c

{c

{{c

A . [c

F

F

c

F

FF is set

a is set

A . (c

[c

{c

{c

{{c

A . [c

c is set

b is Element of F

A . (b,c

[b,c

{b,c

{b} is non empty set

{{b,c

A . [b,c

F

F

c

the carrier of c

FF is Element of the carrier of c

a is Element of the carrier of c

<^FF,a^> is set

the Arrows of c

[: the carrier of c

the Arrows of c

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

the Arrows of c

A . (FF,a) is set

A . [FF,a] is set

b is set

F

FF is Element of the carrier of c

a is Element of the carrier of c

<^FF,a^> is set

the Arrows of c

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

the Arrows of c

b is Element of the carrier of c

<^a,b^> is set

the Arrows of c

[a,b] is V22() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

the Arrows of c

c is Element of <^FF,a^>

d is Element of <^a,b^>

d * c is Element of <^FF,b^>

<^FF,b^> is set

the Arrows of c

[FF,b] is V22() set

{FF,b} is non empty set

{{FF,b},{FF}} is non empty set

the Arrows of c

F

A is Relation-like Function-like Function-yielding V63() set

c

FF is set

a is set

A . (c

[c

[c

{c

{c

{{c

[[c

{[c

{[c

{{[c

A . [c

F

the carrier of F

A is set

FF is Element of the carrier of F

c

FF is set

the Arrows of F

[: the carrier of F

the Comp of F

[: the carrier of F

{| the Arrows of F

{| the Arrows of F

c is set

FF is Element of c

a is Element of c

the Arrows of F

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

the Arrows of F

d is set

b is Element of c

the Arrows of F

[a,b] is V22() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

the Arrows of F

f is Element of the carrier of F

fa is Element of the carrier of F

<^f,fa^> is set

the Arrows of F

[f,fa] is V22() set

{f,fa} is non empty set

{f} is non empty set

{{f,fa},{f}} is non empty set

the Arrows of F

fb is Element of the carrier of F

<^fa,fb^> is set

the Arrows of F

[fa,fb] is V22() set

{fa,fb} is non empty set

{fa} is non empty set

{{fa,fb},{fa}} is non empty set

the Arrows of F

the Comp of F

( the Comp of F

[d,c] is V22() set

{d,c} is non empty set

{d} is non empty set

{{d,c},{d}} is non empty set

( the Comp of F

g is Element of <^f,fa^>

g is Element of <^fa,fb^>

g * g is Element of <^f,fb^>

<^f,fb^> is set

the Arrows of F

[f,fb] is V22() set

{f,fb} is non empty set

{{f,fb},{f}} is non empty set

the Arrows of F

the Arrows of F

[FF,b] is V22() set

{FF,b} is non empty set

{{FF,b},{FF}} is non empty set

the Arrows of F

d is set

FF is Element of c

a is Element of c

the Arrows of F

[FF,a] is V22() set

{FF,a} is non empty set

{FF} is non empty set

{{FF,a},{FF}} is non empty set

the Arrows of F

f is set

b is Element of c

the Arrows of F

[a,b] is V22() set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

the Arrows of F

fa is set

c is Element of c

the Arrows of F

[b,c] is V22() set

{b,c} is non empty set

{b} is non empty set

{{b,c},{b}} is non empty set

the Arrows of F

fb is Element of the carrier of F

g is Element of the carrier of F

<^fb,g^> is set

the Arrows of F

[fb,g] is V22() set

{fb,g} is non empty set

{fb} is non empty set

{{fb,g},{fb}} is non empty set

the Arrows of F

g is Element of the carrier of F

<^g,g^> is set

the Arrows of F

[g,g] is V22() set

{g,g} is non empty set

{g} is non empty set

{{g,g},{g}} is non empty set

the Arrows of F

c

<^g,c

the Arrows of F

[g,c

{g,c

{g} is non empty set

{{g,c

the Arrows of F

<^fb,g^> is set

the Arrows of F

[fb,g] is V22() set

{fb,g} is non empty set

{{fb,g},{fb}} is non empty set

the Arrows of F

<^g,c

the Arrows of F

[g,c

{g,c

{{g,c

the Arrows of F

the Comp of F

( the Comp of F

[f,d] is V22() set

{f,d} is non empty set

{f} is non empty set

{{f,d},{f}} is non empty set

( the Comp of F

the Comp of F

( the Comp of F

[fa,(( the Comp of F

{fa,(( the Comp of F

{fa} is non empty set

{{fa,(( the Comp of F

( the Comp of F

g9 is Element of <^fb,g^>

a1 is Element of <^g,g^>

a1 * g9 is Element of <^fb,g^>

the Comp of F

( the Comp of F

[fa,(a1 * g9)] is V22() set

{fa,(a1 * g9)} is non empty set

{{fa,(a1 * g9)},{fa}} is non empty set

( the Comp of F

b1 is Element of <^g,c

b1 * (a1 * g9) is Element of <^fb,c

<^fb,c

the Arrows of F

[fb,c

{fb,c

{{fb,c

the Arrows of F

b1 * a1 is Element of <^g,c

(b1 * a1) * g9 is Element of <^fb,c

the Comp of F

( the Comp of F

[(b1 * a1),d] is V22() set

{(b1 * a1),d} is non empty set

{(b1 * a1)} is non empty set

{{(b1 * a1),d},{(b1 * a1)}} is non empty set

( the Comp of F

the Comp of F

( the Comp of F

[fa,f] is V22() set

{fa,f} is non empty set

{{fa,f},{fa}} is non empty set

( the Comp of F

( the Comp of F

[(( the Comp of F

{(( the Comp of F

{(( the Comp of F

{{(( the Comp of F

( the Comp of F

FF is Element of c

a is Element of the carrier of F

idm a is retraction coretraction iso mono epi Element of <^a,a^>

<^a,a^> is non empty set

the Arrows of F

[a,a] is V22() set

{a,a} is non empty set

{a} is non empty set

{{a,a},{a}} is non empty set

the Arrows of F

b is set

c is set

the Arrows of F

[FF,FF] is V22() set

{FF,FF} is non empty set

{FF} is non empty set

{{FF,FF},{FF}} is non empty set

the Arrows of F

f is set

d is Element of c

the Arrows of F

[FF,d] is V22() set

{FF,d} is non empty set

{{FF,d},{FF}} is non empty set

the Arrows of F

fa is Element of the carrier of F

<^a,fa^> is set

the Arrows of F

[a,fa] is V22() set

{a,fa} is non empty set

{{a,fa},{a}} is non empty set

the Arrows of F

the Comp of F

( the Comp of F

[f,c] is V22() set

{f,c} is non empty set

{f} is non empty set

{{f,c},{f}} is non empty set

( the Comp of F

fb is Element of <^a,fa^>

fb * (idm a) is Element of <^a,fa^>

FF is Element of c

a is Element of the carrier of F

idm a is retraction coretraction iso mono epi Element of <^a,a^>

<^a,a^> is non empty set

the Arrows of F

[a,a] is V22() set

{a,a} is non empty set

{a} is non empty set

{{a,a},{a}} is non empty set

the Arrows of F

b is set

c is set

the Arrows of F

[FF,FF] is V22() set

{FF,FF} is non empty set

{FF} is non empty set

{{FF,FF},{FF}} is non empty set

the Arrows of F

f is set

d is Element of c

the Arrows of F

[d,FF] is V22() set

{d,FF} is non empty set

{d} is non empty set

{{d,FF},{d}} is non empty set

the Arrows of F

fa is Element of the carrier of F

<^fa,a^> is set

the Arrows of F

[fa,a] is V22() set

{fa,a} is non empty set

{fa} is non empty set

{{fa,a},{fa}} is non empty set

the Arrows of F

the Comp of F

( the Comp of F

[c,f] is V22() set

{c,f} is non empty set

{c} is non empty set

{{c,f},{c}} is non empty set

( the Comp of F

fb is Element of <^fa,a^>

(idm a) * fb is Element of <^fa,a^>

FF is non empty transitive strict associative with_units reflexive AltCatStr

the carrier of FF is non empty set

[: the carrier of FF, the carrier of FF:] is Relation-like non empty set

the Arrows of FF is Relation-like [: the carrier of FF, the carrier of FF:] -defined Function-like non empty V14([: the carrier of FF, the carrier of FF:]) set

[: the carrier of FF, the carrier of FF, the carrier of FF:] is non empty set

the Comp of FF is Relation-like [: the carrier of FF, the carrier of FF, the carrier of FF:] -defined Function-like non empty V14([: the carrier of FF, the carrier of FF, the carrier of FF:]) Function-yielding V63() ManySortedFunction of {| the Arrows of FF, the Arrows of FF|},{| the Arrows of FF|}

{| the Arrows of FF, the Arrows of FF|} is Relation-like [: the carrier of FF, the carrier of FF, the carrier of FF:] -defined Function-like non empty V14([: the carrier of FF, the carrier of FF, the carrier of FF:]) set

{| the Arrows of FF|} is Relation-like [: the carrier of FF, the carrier of FF, the carrier of FF:] -defined Function-like non empty V14([: the carrier of FF, the carrier of FF, the carrier of FF:]) set

a is set

b is set

c is set

[b,c] is V22() set

{b,c} is non empty set

{b} is non empty set

{{b,c},{b}} is non empty set

the Arrows of FF . a is set

d is Element of the carrier of FF

f is Element of the carrier of FF

<^d,f^> is set

the Arrows of FF . (d,f) is set

[d,f] is V22() set

{d,f} is non empty set

{d} is non empty set

{{d,f},{d}} is non empty set

the Arrows of FF . [d,f] is set

the Arrows of F

the Arrows of F

the Arrows of F

fa is set

a is set

the Comp of FF . a is Relation-like Function-like set

the Comp of F

b is set

c is set

d is set

[b,c,d] is V22() V23() set

[b,c] is V22() set

{b,c} is non empty set

{b} is non empty set

{{b,c},{b}} is non empty set

[[b,c],d] is V22() set

{[b,c],d} is non empty set

{[b,c]} is Relation-like Function-like non empty set

{{[b,c],d},{[b,c]}} is non empty set

f is Element of the carrier of FF

fa is Element of the carrier of FF

fb is Element of the carrier of FF

g9 is set

the Comp of FF . (f,fa,fb) is Relation-like [:( the Arrows of FF . (fa,fb)),( the Arrows of FF . (f,fa)):] -defined the Arrows of FF . (f,fb) -valued Function-like quasi_total Element of bool [:[:( the Arrows of FF . (fa,fb)),( the Arrows of FF . (f,fa)):],( the Arrows of FF . (f,fb)):]

the Arrows of FF . (fa,fb) is set

[fa,fb] is V22() set

{fa,fb} is non empty set

{fa} is non empty set

{{fa,fb},{fa}} is non empty set

the Arrows of FF . [fa,fb] is set

the Arrows of FF . (f,fa) is set

[f,fa] is V22() set

{f,fa} is non empty set

{f} is non empty