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
F1() is non empty set
[:F1(),F1():] is Relation-like non empty set
A is Relation-like [:F1(),F1():] -defined Function-like non empty V14([:F1(),F1():]) set
{|A,A|} is Relation-like [:F1(),F1(),F1():] -defined Function-like non empty V14([:F1(),F1(),F1():]) set
[:F1(),F1(),F1():] is non empty set
{|A|} is Relation-like [:F1(),F1(),F1():] -defined Function-like non empty V14([:F1(),F1(),F1():]) set
c2 is set
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 F1()
d is Element of F1()
f is Element of F1()
F2(d,f) is set
F2(c,d) is set
[:F2(d,f),F2(c,d):] is Relation-like set
F2(c,f) is set
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
F3(c,d,f,g,fb) is set
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
c13 is set
[c13,g] is V22() set
{c13,g} is non empty set
{c13} is non empty set
{{c13,g},{c13}} is non empty set
fb . [c13,g] is set
F3(c,d,f,g,c13) is set
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
F3(c,d,f,g9,a1) is set
c2 is Relation-like Function-like set
proj1 c2 is set
a is set
FF is Relation-like [:F1(),F1(),F1():] -defined Function-like non empty V14([:F1(),F1(),F1():]) set
FF . a is set
b is Element of F1()
c is Element of F1()
d is Element of F1()
{|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)):]
F2(b,c) is set
F2(c,d) is set
{|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 [:F1(),F1(),F1():] -defined Function-like non empty V14([:F1(),F1(),F1():]) Function-yielding V63() ManySortedFunction of {|A,A|},{|A|}
AltCatStr(# F1(),A,a #) is non empty strict AltCatStr
the carrier of AltCatStr(# F1(),A,a #) is non empty set
c is Element of the carrier of AltCatStr(# F1(),A,a #)
d is Element of the carrier of AltCatStr(# F1(),A,a #)
<^c,d^> is set
the Arrows of AltCatStr(# F1(),A,a #) is Relation-like [: the carrier of AltCatStr(# F1(),A,a #), the carrier of AltCatStr(# F1(),A,a #):] -defined Function-like non empty V14([: the carrier of AltCatStr(# F1(),A,a #), the carrier of AltCatStr(# F1(),A,a #):]) set
[: the carrier of AltCatStr(# F1(),A,a #), the carrier of AltCatStr(# F1(),A,a #):] is Relation-like non empty set
the Arrows of AltCatStr(# F1(),A,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 AltCatStr(# F1(),A,a #) . [c,d] is set
f is Element of the carrier of AltCatStr(# F1(),A,a #)
<^d,f^> is set
the Arrows of AltCatStr(# F1(),A,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 AltCatStr(# F1(),A,a #) . [d,f] is set
<^c,f^> is set
the Arrows of AltCatStr(# F1(),A,a #) . (c,f) is set
[c,f] is V22() set
{c,f} is non empty set
{{c,f},{c}} is non empty set
the Arrows of AltCatStr(# F1(),A,a #) . [c,f] is set
the Element of <^c,d^> is Element of <^c,d^>
the Element of <^d,f^> is Element of <^d,f^>
fa is Element of F1()
fb is Element of F1()
F2(fa,fb) is set
g is Element of F1()
F2(fb,g) is set
F3(fa,fb,g, the Element of <^c,d^>, the Element of <^d,f^>) is set
F2(fa,g) is set
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
F2(d,f) is 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
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 F1()
g is Element of F1()
g is Element of F1()
{|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
c13 is Relation-like {|A,A|} . (fb,g,g) -defined {|A|} . (fb,g,g) -valued Function-like quasi_total Element of bool [:({|A,A|} . (fb,g,g)),({|A|} . (fb,g,g)):]
F2(fb,g) is set
F2(g,g) is set
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
F3(d,f,fa,g9,a1) is set
F2(d,f) is set
F2(f,fa) 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
c13 . [a1,g9] is set
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
F1() is non empty transitive AltCatStr
the carrier of F1() is non empty set
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1():]) set
[: the carrier of F1(), the carrier of F1():] is Relation-like non empty set
A is Element of the carrier of F1()
c2 is Element of the carrier of F1()
the Arrows of F1() . (A,c2) is set
[A,c2] is V22() set
{A,c2} is non empty set
{A} is non empty set
{{A,c2},{A}} is non empty set
the Arrows of F1() . [A,c2] is set
FF is Element of the carrier of F1()
the Arrows of F1() . (c2,FF) is set
[c2,FF] is V22() set
{c2,FF} is non empty set
{c2} is non empty set
{{c2,FF},{c2}} is non empty set
the Arrows of F1() . [c2,FF] is set
a is Element of the carrier of F1()
the Arrows of F1() . (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 F1() . [FF,a] is set
the Comp of F1() is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) Function-yielding V63() ManySortedFunction of {| the Arrows of F1(), the Arrows of F1()|},{| the Arrows of F1()|}
[: the carrier of F1(), the carrier of F1(), the carrier of F1():] is non empty set
{| the Arrows of F1(), the Arrows of F1()|} is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) set
{| the Arrows of F1()|} is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) set
the Comp of F1() . (A,FF,a) is Relation-like [:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (A,FF)):] -defined the Arrows of F1() . (A,a) -valued Function-like quasi_total Element of bool [:[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (A,FF)):],( the Arrows of F1() . (A,a)):]
the Arrows of F1() . (A,FF) is set
[A,FF] is V22() set
{A,FF} is non empty set
{{A,FF},{A}} is non empty set
the Arrows of F1() . [A,FF] is set
[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (A,FF)):] is Relation-like set
the Arrows of F1() . (A,a) is set
[A,a] is V22() set
{A,a} is non empty set
{{A,a},{A}} is non empty set
the Arrows of F1() . [A,a] is set
[:[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (A,FF)):],( the Arrows of F1() . (A,a)):] is Relation-like set
bool [:[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (A,FF)):],( the Arrows of F1() . (A,a)):] is non empty set
the Comp of F1() . (A,c2,FF) is Relation-like [:( the Arrows of F1() . (c2,FF)),( the Arrows of F1() . (A,c2)):] -defined the Arrows of F1() . (A,FF) -valued Function-like quasi_total Element of bool [:[:( the Arrows of F1() . (c2,FF)),( the Arrows of F1() . (A,c2)):],( the Arrows of F1() . (A,FF)):]
[:( the Arrows of F1() . (c2,FF)),( the Arrows of F1() . (A,c2)):] is Relation-like set
[:[:( the Arrows of F1() . (c2,FF)),( the Arrows of F1() . (A,c2)):],( the Arrows of F1() . (A,FF)):] is Relation-like set
bool [:[:( the Arrows of F1() . (c2,FF)),( the Arrows of F1() . (A,c2)):],( the Arrows of F1() . (A,FF)):] is non empty set
the Comp of F1() . (A,c2,a) is Relation-like [:( the Arrows of F1() . (c2,a)),( the Arrows of F1() . (A,c2)):] -defined the Arrows of F1() . (A,a) -valued Function-like quasi_total Element of bool [:[:( the Arrows of F1() . (c2,a)),( the Arrows of F1() . (A,c2)):],( the Arrows of F1() . (A,a)):]
the Arrows of F1() . (c2,a) is set
[c2,a] is V22() set
{c2,a} is non empty set
{{c2,a},{c2}} is non empty set
the Arrows of F1() . [c2,a] is set
[:( the Arrows of F1() . (c2,a)),( the Arrows of F1() . (A,c2)):] is Relation-like set
[:[:( the Arrows of F1() . (c2,a)),( the Arrows of F1() . (A,c2)):],( the Arrows of F1() . (A,a)):] is Relation-like set
bool [:[:( the Arrows of F1() . (c2,a)),( the Arrows of F1() . (A,c2)):],( the Arrows of F1() . (A,a)):] is non empty set
the Comp of F1() . (c2,FF,a) is Relation-like [:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (c2,FF)):] -defined the Arrows of F1() . (c2,a) -valued Function-like quasi_total Element of bool [:[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (c2,FF)):],( the Arrows of F1() . (c2,a)):]
[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (c2,FF)):] is Relation-like set
[:[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (c2,FF)):],( the Arrows of F1() . (c2,a)):] is Relation-like set
bool [:[:( the Arrows of F1() . (FF,a)),( the Arrows of F1() . (c2,FF)):],( the Arrows of F1() . (c2,a)):] is non empty set
g is set
c13 is set
g9 is set
( the Comp of F1() . (A,c2,FF)) . (c13,g) is set
[c13,g] is V22() set
{c13,g} is non empty set
{c13} is non empty set
{{c13,g},{c13}} is non empty set
( the Comp of F1() . (A,c2,FF)) . [c13,g] is set
( the Comp of F1() . (A,FF,a)) . (g9,(( the Comp of F1() . (A,c2,FF)) . (c13,g))) is set
[g9,(( the Comp of F1() . (A,c2,FF)) . (c13,g))] is V22() set
{g9,(( the Comp of F1() . (A,c2,FF)) . (c13,g))} is non empty set
{g9} is non empty set
{{g9,(( the Comp of F1() . (A,c2,FF)) . (c13,g))},{g9}} is non empty set
( the Comp of F1() . (A,FF,a)) . [g9,(( the Comp of F1() . (A,c2,FF)) . (c13,g))] is set
( the Comp of F1() . (c2,FF,a)) . (g9,c13) is set
[g9,c13] is V22() set
{g9,c13} is non empty set
{{g9,c13},{g9}} is non empty set
( the Comp of F1() . (c2,FF,a)) . [g9,c13] is set
( the Comp of F1() . (A,c2,a)) . ((( the Comp of F1() . (c2,FF,a)) . (g9,c13)),g) is set
[(( the Comp of F1() . (c2,FF,a)) . (g9,c13)),g] is V22() set
{(( the Comp of F1() . (c2,FF,a)) . (g9,c13)),g} is non empty set
{(( the Comp of F1() . (c2,FF,a)) . (g9,c13))} is non empty set
{{(( the Comp of F1() . (c2,FF,a)) . (g9,c13)),g},{(( the Comp of F1() . (c2,FF,a)) . (g9,c13))}} is non empty set
( the Comp of F1() . (A,c2,a)) . [(( the Comp of F1() . (c2,FF,a)) . (g9,c13)),g] is set
f is Element of the carrier of F1()
fa is Element of the carrier of F1()
<^f,fa^> is set
the Arrows of F1() . (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 F1() . [f,fa] is set
fb is Element of the carrier of F1()
<^fa,fb^> is set
the Arrows of F1() . (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 F1() . [fa,fb] is set
g is Element of the carrier of F1()
<^fb,g^> is set
the Arrows of F1() . (fb,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
the Arrows of F1() . [fb,g] is set
<^f,fb^> is set
the Arrows of F1() . (f,fb) is set
[f,fb] is V22() set
{f,fb} is non empty set
{{f,fb},{f}} is non empty set
the Arrows of F1() . [f,fb] is set
<^fa,g^> is set
the Arrows of F1() . (fa,g) is set
[fa,g] is V22() set
{fa,g} is non empty set
{{fa,g},{fa}} is non empty set
the Arrows of F1() . [fa,g] is set
a1 is Element of <^f,fa^>
b1 is Element of <^fa,fb^>
b1 * a1 is Element of <^f,fb^>
( the Comp of F1() . (A,FF,a)) . (g9,(b1 * a1)) is set
[g9,(b1 * a1)] is V22() set
{g9,(b1 * a1)} is non empty set
{{g9,(b1 * a1)},{g9}} is non empty set
( the Comp of F1() . (A,FF,a)) . [g9,(b1 * a1)] is set
f1 is Element of <^fb,g^>
f1 * (b1 * a1) is Element of <^f,g^>
<^f,g^> is set
the Arrows of F1() . (f,g) is set
[f,g] is V22() set
{f,g} is non empty set
{{f,g},{f}} is non empty set
the Arrows of F1() . [f,g] is set
F2(A,FF,a,(b1 * a1),f1) is set
F2(A,c2,FF,g,c13) is set
F2(A,FF,a,F2(A,c2,FF,g,c13),g9) is set
F2(fa,fb,g,c13,g9) is set
F2(f,fa,g,g,F2(fa,fb,g,c13,g9)) is set
f1 * b1 is Element of <^fa,g^>
F2(f,fa,g,g,(f1 * b1)) is set
(f1 * b1) * a1 is Element of <^f,g^>
( the Comp of F1() . (A,c2,a)) . ((f1 * b1),g) is set
[(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 F1() . (A,c2,a)) . [(f1 * b1),g] is set
F1() is non empty transitive AltCatStr
the carrier of F1() is non empty set
the Comp of F1() is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) Function-yielding V63() ManySortedFunction of {| the Arrows of F1(), the Arrows of F1()|},{| the Arrows of F1()|}
[: the carrier of F1(), the carrier of F1(), the carrier of F1():] is non empty set
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1():]) set
[: the carrier of F1(), the carrier of F1():] is Relation-like non empty set
{| the Arrows of F1(), the Arrows of F1()|} is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) set
{| the Arrows of F1()|} is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) set
b is Element of the carrier of F1()
c is Element of the carrier of F1()
<^c,c^> is set
the Arrows of F1() . (c,c) is set
[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 F1() . [c,c] is set
d is set
f is set
the Arrows of F1() . (b,b) is set
[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 F1() . [b,b] is set
fb is set
fa is Element of the carrier of F1()
the Arrows of F1() . (fa,b) is set
[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 F1() . [fa,b] is set
g is Element of the carrier of F1()
<^g,c^> is set
the Arrows of F1() . (g,c) is set
[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 F1() . [g,c] is set
F2(fa,b,b,fb,f) is set
the Comp of F1() . (fa,b,b) is Relation-like [:( the Arrows of F1() . (b,b)),( the Arrows of F1() . (fa,b)):] -defined the Arrows of F1() . (fa,b) -valued Function-like quasi_total Element of bool [:[:( the Arrows of F1() . (b,b)),( the Arrows of F1() . (fa,b)):],( the Arrows of F1() . (fa,b)):]
[:( the Arrows of F1() . (b,b)),( the Arrows of F1() . (fa,b)):] is Relation-like set
[:[:( the Arrows of F1() . (b,b)),( the Arrows of F1() . (fa,b)):],( the Arrows of F1() . (fa,b)):] is Relation-like set
bool [:[:( the Arrows of F1() . (b,b)),( the Arrows of F1() . (fa,b)):],( the Arrows of F1() . (fa,b)):] is non empty set
( the Comp of F1() . (fa,b,b)) . (f,fb) is set
[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 F1() . (fa,b,b)) . [f,fb] is set
c13 is Element of <^g,c^>
g is Element of <^c,c^>
g * c13 is Element of <^g,c^>
b is Element of the carrier of F1()
the Arrows of F1() . (b,b) is set
[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 F1() . [b,b] is set
c is Element of the carrier of F1()
<^c,c^> is set
the Arrows of F1() . (c,c) is set
[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 F1() . [c,c] is set
d is set
fa is Element of the carrier of F1()
the Arrows of F1() . (b,fa) is set
[b,fa] is V22() set
{b,fa} is non empty set
{{b,fa},{b}} is non empty set
the Arrows of F1() . [b,fa] is set
the Comp of F1() . (b,b,fa) is Relation-like [:( the Arrows of F1() . (b,fa)),( the Arrows of F1() . (b,b)):] -defined the Arrows of F1() . (b,fa) -valued Function-like quasi_total Element of bool [:[:( the Arrows of F1() . (b,fa)),( the Arrows of F1() . (b,b)):],( the Arrows of F1() . (b,fa)):]
[:( the Arrows of F1() . (b,fa)),( the Arrows of F1() . (b,b)):] is Relation-like set
[:[:( the Arrows of F1() . (b,fa)),( the Arrows of F1() . (b,b)):],( the Arrows of F1() . (b,fa)):] is Relation-like set
bool [:[:( the Arrows of F1() . (b,fa)),( the Arrows of F1() . (b,b)):],( the Arrows of F1() . (b,fa)):] is non empty set
fb is set
( the Comp of F1() . (b,b,fa)) . (fb,d) is set
[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 F1() . (b,b,fa)) . [fb,d] is set
g is Element of the carrier of F1()
<^c,g^> is set
the Arrows of F1() . (c,g) is set
[c,g] is V22() set
{c,g} is non empty set
{{c,g},{c}} is non empty set
the Arrows of F1() . [c,g] is set
F2(b,b,fa,d,fb) is set
f is Element of <^c,c^>
g is Element of <^c,g^>
g * f is Element of <^c,g^>
F1() is non empty set
a is set
A is Element of F1()
c2 is Element of F1()
F2(A,c2) is set
b is set
FF is Element of F1()
F2(c2,FF) is set
F3(A,c2,FF,a,b) is set
F2(A,FF) is set
A is non empty transitive strict AltCatStr
the carrier of A is non empty set
c2 is Element of the carrier of A
FF is Element of the carrier of A
<^c2,FF^> is set
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 . (c2,FF) is set
[c2,FF] is V22() set
{c2,FF} is non empty set
{c2} is non empty set
{{c2,FF},{c2}} is non empty set
the Arrows of A . [c2,FF] is set
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
F3(c2,FF,a,c,d) is set
F3(c2,a,b,H1(c2,FF,a,c,d),f) is set
F3(FF,a,b,d,f) is set
F3(c2,FF,b,c,H1(FF,a,b,d,f)) is set
F2(c2,FF) is set
F2(FF,a) is set
F2(a,b) is set
c2 is Element of the carrier of A
<^c2,c2^> is set
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 . (c2,c2) is set
[c2,c2] is V22() set
{c2,c2} is non empty set
{c2} is non empty set
{{c2,c2},{c2}} is non empty set
the Arrows of A . [c2,c2] is set
F2(c2,c2) is set
FF is set
a is Element of the carrier of A
<^c2,a^> is set
the Arrows of A . (c2,a) is set
[c2,a] is V22() set
{c2,a} is non empty set
{{c2,a},{c2}} is non empty set
the Arrows of A . [c2,a] is set
F2(c2,a) is set
b is set
F3(c2,c2,a,FF,b) is set
c2 is Element of the carrier of A
<^c2,c2^> is set
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 . (c2,c2) is set
[c2,c2] is V22() set
{c2,c2} is non empty set
{c2} is non empty set
{{c2,c2},{c2}} is non empty set
the Arrows of A . [c2,c2] is set
F2(c2,c2) is set
FF is set
a is Element of the carrier of A
<^a,c2^> is set
the Arrows of A . (a,c2) is set
[a,c2] is V22() set
{a,c2} is non empty set
{a} is non empty set
{{a,c2},{a}} is non empty set
the Arrows of A . [a,c2] is set
F2(a,c2) is set
b is set
F3(a,c2,c2,b,FF) is set
F1() is non empty set
A is non empty transitive AltCatStr
the carrier of A is non empty set
c2 is non empty transitive AltCatStr
the carrier of c2 is non empty set
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 c2 is Relation-like [: the carrier of c2, the carrier of c2:] -defined Function-like non empty V14([: the carrier of c2, the carrier of c2:]) set
[: the carrier of c2, the carrier of c2:] is Relation-like non empty set
the Comp of c2 is Relation-like [: the carrier of c2, the carrier of c2, the carrier of c2:] -defined Function-like non empty V14([: the carrier of c2, the carrier of c2, the carrier of c2:]) Function-yielding V63() ManySortedFunction of {| the Arrows of c2, the Arrows of c2|},{| the Arrows of c2|}
[: the carrier of c2, the carrier of c2, the carrier of c2:] is non empty set
{| the Arrows of c2, the Arrows of c2|} is Relation-like [: the carrier of c2, the carrier of c2, the carrier of c2:] -defined Function-like non empty V14([: the carrier of c2, the carrier of c2, the carrier of c2:]) set
{| the Arrows of c2|} is Relation-like [: the carrier of c2, the carrier of c2, the carrier of c2:] -defined Function-like non empty V14([: the carrier of c2, the carrier of c2, the carrier of c2:]) set
AltCatStr(# the carrier of c2, the Arrows of c2, the Comp of c2 #) is non empty strict AltCatStr
FF is set
[:F1(),F1():] is Relation-like non empty set
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
F2(c,d) is set
f is Element of the carrier of c2
fa is Element of the carrier of c2
<^f,fa^> is set
the Arrows of c2 . (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 c2 . [f,fa] is set
the Arrows of c2 . FF is set
FF is set
[:F1(),F1(),F1():] is non empty set
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 c2 . FF is Relation-like Function-like set
fb is Element of the carrier of c2
g is Element of the carrier of c2
g is Element of the carrier of c2
the Comp of c2 . (fb,g,g) is Relation-like [:( the Arrows of c2 . (g,g)),( the Arrows of c2 . (fb,g)):] -defined the Arrows of c2 . (fb,g) -valued Function-like quasi_total Element of bool [:[:( the Arrows of c2 . (g,g)),( the Arrows of c2 . (fb,g)):],( the Arrows of c2 . (fb,g)):]
the Arrows of c2 . (g,g) is set
[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 c2 . [g,g] is set
the Arrows of c2 . (fb,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
the Arrows of c2 . [fb,g] is set
[:( the Arrows of c2 . (g,g)),( the Arrows of c2 . (fb,g)):] is Relation-like set
the Arrows of c2 . (fb,g) is set
[fb,g] is V22() set
{fb,g} is non empty set
{{fb,g},{fb}} is non empty set
the Arrows of c2 . [fb,g] is set
[:[:( the Arrows of c2 . (g,g)),( the Arrows of c2 . (fb,g)):],( the Arrows of c2 . (fb,g)):] is Relation-like set
bool [:[:( the Arrows of c2 . (g,g)),( the Arrows of c2 . (fb,g)):],( the Arrows of c2 . (fb,g)):] is non empty set
<^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 c2 . (fb,g,g)) is Relation-like the Arrows of c2 . (g,g) -defined the Arrows of c2 . (fb,g) -valued Element of bool [:( the Arrows of c2 . (g,g)),( the Arrows of c2 . (fb,g)):]
bool [:( the Arrows of c2 . (g,g)),( the Arrows of c2 . (fb,g)):] is non empty set
c13 is set
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)) . c13 is set
( 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^>
F3(d,f,fa,f1,b1) is set
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 c2 . (fb,g,g)) . (G1,b2) is set
[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 c2 . (fb,g,g)) . [G1,b2] is set
( the Comp of c2 . (fb,g,g)) . c13 is set
F1() is non empty set
[:F1(),F1():] is Relation-like non empty set
A is Relation-like Function-like set
proj1 A is set
c2 is Element of F1()
FF is Element of F1()
[c2,FF] is V22() set
{c2,FF} is non empty set
{c2} is non empty set
{{c2,FF},{c2}} is non empty set
[c2,FF] `1 is set
[c2,FF] `2 is set
a is set
A . (c2,FF) is set
A . [c2,FF] is set
F2(c2,FF) is set
b is set
c2 is Element of F1()
FF is Element of F1()
A . (c2,FF) is set
[c2,FF] is V22() set
{c2,FF} is non empty set
{c2} is non empty set
{{c2,FF},{c2}} is non empty set
A . [c2,FF] is set
c is set
a is Element of F1()
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
F2(c2,FF) is set
F2(FF,a) is set
F3(c2,FF,a,b,c) is set
F2(c2,a) is set
A . (c2,a) is set
[c2,a] is V22() set
{c2,a} is non empty set
{{c2,a},{c2}} is non empty set
A . [c2,a] is set
c is set
c2 is Element of F1()
FF is Element of F1()
A . (c2,FF) is set
[c2,FF] is V22() set
{c2,FF} is non empty set
{c2} is non empty set
{{c2,FF},{c2}} is non empty set
A . [c2,FF] is set
d is set
a is Element of F1()
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 F1()
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
F2(c2,FF) is set
F2(FF,a) is set
F2(a,b) is set
F3(c2,FF,a,c,d) is set
F3(c2,a,b,H2(c2,FF,a,c,d),f) is set
F3(FF,a,b,d,f) is set
F3(c2,FF,b,c,H2(FF,a,b,d,f)) is set
c2 is Element of F1()
F2(c2,c2) is set
FF is set
a is set
A . (c2,c2) is set
[c2,c2] is V22() set
{c2,c2} is non empty set
{c2} is non empty set
{{c2,c2},{c2}} is non empty set
A . [c2,c2] is set
c is set
b is Element of F1()
A . (c2,b) is set
[c2,b] is V22() set
{c2,b} is non empty set
{{c2,b},{c2}} is non empty set
A . [c2,b] is set
F2(c2,b) is set
F3(c2,c2,b,a,c) is set
c2 is Element of F1()
F2(c2,c2) is set
FF is set
a is set
A . (c2,c2) is set
[c2,c2] is V22() set
{c2,c2} is non empty set
{c2} is non empty set
{{c2,c2},{c2}} is non empty set
A . [c2,c2] is set
c is set
b is Element of F1()
A . (b,c2) is set
[b,c2] is V22() set
{b,c2} is non empty set
{b} is non empty set
{{b,c2},{b}} is non empty set
A . [b,c2] is set
F2(b,c2) is set
F3(b,c2,c2,c,a) is set
c2 is non empty transitive strict associative with_units reflexive AltCatStr
the carrier of c2 is non empty set
FF is Element of the carrier of c2
a is Element of the carrier of c2
<^FF,a^> is set
the Arrows of c2 is Relation-like [: the carrier of c2, the carrier of c2:] -defined Function-like non empty V14([: the carrier of c2, the carrier of c2:]) set
[: the carrier of c2, the carrier of c2:] is Relation-like non empty set
the Arrows of c2 . (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 c2 . [FF,a] is set
A . (FF,a) is set
A . [FF,a] is set
b is set
F2(FF,a) is set
FF is Element of the carrier of c2
a is Element of the carrier of c2
<^FF,a^> is set
the Arrows of c2 . (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 c2 . [FF,a] is set
b is Element of the carrier of c2
<^a,b^> is set
the Arrows of c2 . (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 c2 . [a,b] is set
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 c2 . (FF,b) is set
[FF,b] is V22() set
{FF,b} is non empty set
{{FF,b},{FF}} is non empty set
the Arrows of c2 . [FF,b] is set
F3(FF,a,b,c,d) is set
A is Relation-like Function-like Function-yielding V63() set
c2 is set
FF is set
a is set
A . (c2,FF,a) is set
[c2,FF,a] is V22() V23() set
[c2,FF] is V22() set
{c2,FF} is non empty set
{c2} is non empty set
{{c2,FF},{c2}} is non empty set
[[c2,FF],a] is V22() set
{[c2,FF],a} is non empty set
{[c2,FF]} is Relation-like Function-like non empty set
{{[c2,FF],a},{[c2,FF]}} is non empty set
A . [c2,FF,a] is Relation-like Function-like set
F1() is non empty transitive associative with_units reflexive AltCatStr
the carrier of F1() is non empty set
A is set
FF is Element of the carrier of F1()
c2 is non empty set
FF is set
the Arrows of F1() is Relation-like [: the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1():]) set
[: the carrier of F1(), the carrier of F1():] is Relation-like non empty set
the Comp of F1() is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) Function-yielding V63() ManySortedFunction of {| the Arrows of F1(), the Arrows of F1()|},{| the Arrows of F1()|}
[: the carrier of F1(), the carrier of F1(), the carrier of F1():] is non empty set
{| the Arrows of F1(), the Arrows of F1()|} is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) set
{| the Arrows of F1()|} is Relation-like [: the carrier of F1(), the carrier of F1(), the carrier of F1():] -defined Function-like non empty V14([: the carrier of F1(), the carrier of F1(), the carrier of F1():]) set
c is set
FF is Element of c2
a is Element of c2
the Arrows of F1() . (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 F1() . [FF,a] is set
d is set
b is Element of c2
the Arrows of F1() . (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 F1() . [a,b] is set
f is Element of the carrier of F1()
fa is Element of the carrier of F1()
<^f,fa^> is set
the Arrows of F1() . (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 F1() . [f,fa] is set
fb is Element of the carrier of F1()
<^fa,fb^> is set
the Arrows of F1() . (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 F1() . [fa,fb] is set
the Comp of F1() . (FF,a,b) is Relation-like Function-like set
( the Comp of F1() . (FF,a,b)) . (d,c) is set
[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 F1() . (FF,a,b)) . [d,c] is set
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 F1() . (f,fb) is set
[f,fb] is V22() set
{f,fb} is non empty set
{{f,fb},{f}} is non empty set
the Arrows of F1() . [f,fb] is set
the Arrows of F1() . (FF,b) is set
[FF,b] is V22() set
{FF,b} is non empty set
{{FF,b},{FF}} is non empty set
the Arrows of F1() . [FF,b] is set
d is set
FF is Element of c2
a is Element of c2
the Arrows of F1() . (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 F1() . [FF,a] is set
f is set
b is Element of c2
the Arrows of F1() . (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 F1() . [a,b] is set
fa is set
c is Element of c2
the Arrows of F1() . (b,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 F1() . [b,c] is set
fb is Element of the carrier of F1()
g is Element of the carrier of F1()
<^fb,g^> is set
the Arrows of F1() . (fb,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
the Arrows of F1() . [fb,g] is set
g is Element of the carrier of F1()
<^g,g^> is set
the Arrows of F1() . (g,g) is set
[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 F1() . [g,g] is set
c13 is Element of the carrier of F1()
<^g,c13^> is set
the Arrows of F1() . (g,c13) is set
[g,c13] is V22() set
{g,c13} is non empty set
{g} is non empty set
{{g,c13},{g}} is non empty set
the Arrows of F1() . [g,c13] is set
<^fb,g^> is set
the Arrows of F1() . (fb,g) is set
[fb,g] is V22() set
{fb,g} is non empty set
{{fb,g},{fb}} is non empty set
the Arrows of F1() . [fb,g] is set
<^g,c13^> is set
the Arrows of F1() . (g,c13) is set
[g,c13] is V22() set
{g,c13} is non empty set
{{g,c13},{g}} is non empty set
the Arrows of F1() . [g,c13] is set
the Comp of F1() . (FF,a,b) is Relation-like Function-like set
( the Comp of F1() . (FF,a,b)) . (f,d) is set
[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 F1() . (FF,a,b)) . [f,d] is set
the Comp of F1() . (FF,b,c) is Relation-like Function-like set
( the Comp of F1() . (FF,b,c)) . (fa,H2(FF,a,b,d,f)) is set
[fa,(( the Comp of F1() . (FF,a,b)) . (f,d))] is V22() set
{fa,(( the Comp of F1() . (FF,a,b)) . (f,d))} is non empty set
{fa} is non empty set
{{fa,(( the Comp of F1() . (FF,a,b)) . (f,d))},{fa}} is non empty set
( the Comp of F1() . (FF,b,c)) . [fa,(( the Comp of F1() . (FF,a,b)) . (f,d))] is set
g9 is Element of <^fb,g^>
a1 is Element of <^g,g^>
a1 * g9 is Element of <^fb,g^>
the Comp of F1() . (fb,g,c13) is Relation-like Function-like set
( the Comp of F1() . (fb,g,c13)) . (fa,(a1 * g9)) is set
[fa,(a1 * g9)] is V22() set
{fa,(a1 * g9)} is non empty set
{{fa,(a1 * g9)},{fa}} is non empty set
( the Comp of F1() . (fb,g,c13)) . [fa,(a1 * g9)] is set
b1 is Element of <^g,c13^>
b1 * (a1 * g9) is Element of <^fb,c13^>
<^fb,c13^> is set
the Arrows of F1() . (fb,c13) is set
[fb,c13] is V22() set
{fb,c13} is non empty set
{{fb,c13},{fb}} is non empty set
the Arrows of F1() . [fb,c13] is set
b1 * a1 is Element of <^g,c13^>
(b1 * a1) * g9 is Element of <^fb,c13^>
the Comp of F1() . (FF,a,c) is Relation-like Function-like set
( the Comp of F1() . (FF,a,c)) . ((b1 * a1),d) is set
[(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 F1() . (FF,a,c)) . [(b1 * a1),d] is set
the Comp of F1() . (a,b,c) is Relation-like Function-like set
( the Comp of F1() . (a,b,c)) . (fa,f) is set
[fa,f] is V22() set
{fa,f} is non empty set
{{fa,f},{fa}} is non empty set
( the Comp of F1() . (a,b,c)) . [fa,f] is set
( the Comp of F1() . (FF,a,c)) . (H2(a,b,c,f,fa),d) is set
[(( the Comp of F1() . (a,b,c)) . (fa,f)),d] is V22() set
{(( the Comp of F1() . (a,b,c)) . (fa,f)),d} is non empty set
{(( the Comp of F1() . (a,b,c)) . (fa,f))} is non empty set
{{(( the Comp of F1() . (a,b,c)) . (fa,f)),d},{(( the Comp of F1() . (a,b,c)) . (fa,f))}} is non empty set
( the Comp of F1() . (FF,a,c)) . [(( the Comp of F1() . (a,b,c)) . (fa,f)),d] is set
FF is Element of c2
a is Element of the carrier of F1()
idm a is retraction coretraction iso mono epi Element of <^a,a^>
<^a,a^> is non empty set
the Arrows of F1() . (a,a) is set
[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 F1() . [a,a] is set
b is set
c is set
the Arrows of F1() . (FF,FF) is set
[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 F1() . [FF,FF] is set
f is set
d is Element of c2
the Arrows of F1() . (FF,d) is set
[FF,d] is V22() set
{FF,d} is non empty set
{{FF,d},{FF}} is non empty set
the Arrows of F1() . [FF,d] is set
fa is Element of the carrier of F1()
<^a,fa^> is set
the Arrows of F1() . (a,fa) is set
[a,fa] is V22() set
{a,fa} is non empty set
{{a,fa},{a}} is non empty set
the Arrows of F1() . [a,fa] is set
the Comp of F1() . (FF,FF,d) is Relation-like Function-like set
( the Comp of F1() . (FF,FF,d)) . (f,c) is set
[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 F1() . (FF,FF,d)) . [f,c] is set
fb is Element of <^a,fa^>
fb * (idm a) is Element of <^a,fa^>
FF is Element of c2
a is Element of the carrier of F1()
idm a is retraction coretraction iso mono epi Element of <^a,a^>
<^a,a^> is non empty set
the Arrows of F1() . (a,a) is set
[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 F1() . [a,a] is set
b is set
c is set
the Arrows of F1() . (FF,FF) is set
[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 F1() . [FF,FF] is set
f is set
d is Element of c2
the Arrows of F1() . (d,FF) is set
[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 F1() . [d,FF] is set
fa is Element of the carrier of F1()
<^fa,a^> is set
the Arrows of F1() . (fa,a) is set
[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 F1() . [fa,a] is set
the Comp of F1() . (d,FF,FF) is Relation-like Function-like set
( the Comp of F1() . (d,FF,FF)) . (c,f) is set
[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 F1() . (d,FF,FF)) . [c,f] is set
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 F1() . a is set
the Arrows of F1() . (d,f) is set
the Arrows of F1() . [d,f] is set
fa is set
a is set
the Comp of FF . a is Relation-like Function-like set
the Comp of F1() . a is Relation-like Function-like set
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