:: GRCAT_1 semantic presentation

K171() is Element of bool K167()
K167() is set
bool K167() is non empty set
K47() is set
bool K47() is non empty set
bool K171() is non empty set
{} is empty set
1 is non empty set
{{},1} is non empty set
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
{{}} is non empty set
UN is non empty V15() V22() V23() universal set
a is Element of UN
aa is Element of UN
C is Element of UN
[a,aa,C] is V27() V28() set
[a,aa] is V27() set
[[a,aa],C] is V27() set
ii is Element of UN
[a,aa,C,ii] is V27() V28() V29() set
[[a,aa,C],ii] is V27() set
[a,aa] is V27() Element of UN
[[a,aa],C] is V27() Element of UN
op2 is Relation-like [:1,1:] -defined 1 -valued Function-like non empty total quasi_total Element of bool [:[:1,1:],1:]
op2 . ({},{}) is set
[{},{}] is V27() set
op2 . [{},{}] is set
op1 is Relation-like 1 -defined 1 -valued Function-like non empty total quasi_total Element of bool [:1,1:]
op1 . {} is set
op0 is empty Element of 1
[:{{}},{{}}:] is non empty set
[{{}},{{}}] is V27() set
[:{{}},{{}}:] is non empty set
UN is non empty V15() V22() V23() universal set
Funcs ([:{{}},{{}}:],{{}}) is functional non empty FUNCTION_DOMAIN of [:{{}},{{}}:],{{}}
Funcs ({{}},{{}}) is functional non empty FUNCTION_DOMAIN of {{}},{{}}
Trivial-addLoopStr is non empty trivial V49() V54(1) left_add-cancelable right_add-cancelable add-cancelable strict left_complementable right_complementable complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
addLoopStr(# 1,op2,op0 #) is non empty strict addLoopStr
the carrier of Trivial-addLoopStr is non empty trivial V34() set
the left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
aa is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
Double the left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
0. Trivial-addLoopStr is V50( Trivial-addLoopStr ) left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
the ZeroF of Trivial-addLoopStr is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
a is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
Double a is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
the carrier of Trivial-addLoopStr is non empty trivial V34() set
0. Trivial-addLoopStr is V50( Trivial-addLoopStr ) left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
the ZeroF of Trivial-addLoopStr is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
UN is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
a is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
aa is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
a + aa is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
the addF of Trivial-addLoopStr is Relation-like [: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:] -defined the carrier of Trivial-addLoopStr -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:], the carrier of Trivial-addLoopStr:]
[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:] is non empty set
[:[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:], the carrier of Trivial-addLoopStr:] is non empty set
bool [:[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:], the carrier of Trivial-addLoopStr:] is non empty set
the addF of Trivial-addLoopStr . (a,aa) is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
[a,aa] is V27() set
the addF of Trivial-addLoopStr . [a,aa] is set
C is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
- C is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
UN is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of UN is non empty set
bool the carrier of UN is non empty set
a is non empty Element of bool the carrier of UN
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
the carrier' of UN is non empty set
bool the carrier' of UN is non empty set
UN is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of UN is non empty set
bool the carrier of UN is non empty set
a is non empty Element of bool the carrier of UN
(UN,a) is Element of bool the carrier' of UN
the carrier' of UN is non empty set
bool the carrier' of UN is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
UN is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of UN is non empty set
bool the carrier of UN is non empty set
the carrier' of UN is non empty set
the Source of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
[: the carrier' of UN, the carrier of UN:] is non empty set
bool [: the carrier' of UN, the carrier of UN:] is non empty set
a is non empty Element of bool the carrier of UN
(UN,a) is non empty Element of bool the carrier' of UN
bool the carrier' of UN is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
the Source of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
[:(UN,a),a:] is non empty set
bool [:(UN,a),a:] is non empty set
the Target of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
the Target of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
the Comp of UN is Relation-like [: the carrier' of UN, the carrier' of UN:] -defined the carrier' of UN -valued Function-like Element of bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:]
[: the carrier' of UN, the carrier' of UN:] is non empty set
[:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
the Comp of UN || (UN,a) is Relation-like Function-like set
[:(UN,a),(UN,a):] is Relation-like the carrier' of UN -defined the carrier' of UN -valued non empty Element of bool [: the carrier' of UN, the carrier' of UN:]
bool [: the carrier' of UN, the carrier' of UN:] is non empty set
[:[:(UN,a),(UN,a):],(UN,a):] is non empty set
bool [:[:(UN,a),(UN,a):],(UN,a):] is non empty set
UN is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of UN is non empty set
bool the carrier of UN is non empty set
a is non empty Element of bool the carrier of UN
(UN,a) is non empty Element of bool the carrier' of UN
the carrier' of UN is non empty set
bool the carrier' of UN is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
(UN,a) is Relation-like (UN,a) -defined a -valued Function-like non empty total quasi_total Element of bool [:(UN,a),a:]
[:(UN,a),a:] is non empty set
bool [:(UN,a),a:] is non empty set
the Source of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
[: the carrier' of UN, the carrier of UN:] is non empty set
bool [: the carrier' of UN, the carrier of UN:] is non empty set
the Source of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
(UN,a) is Relation-like (UN,a) -defined a -valued Function-like non empty total quasi_total Element of bool [:(UN,a),a:]
the Target of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
the Target of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
(UN,a) is Relation-like [:(UN,a),(UN,a):] -defined (UN,a) -valued Function-like Element of bool [:[:(UN,a),(UN,a):],(UN,a):]
[:(UN,a),(UN,a):] is Relation-like the carrier' of UN -defined the carrier' of UN -valued non empty Element of bool [: the carrier' of UN, the carrier' of UN:]
[: the carrier' of UN, the carrier' of UN:] is non empty set
bool [: the carrier' of UN, the carrier' of UN:] is non empty set
[:[:(UN,a),(UN,a):],(UN,a):] is non empty set
bool [:[:(UN,a),(UN,a):],(UN,a):] is non empty set
the Comp of UN is Relation-like [: the carrier' of UN, the carrier' of UN:] -defined the carrier' of UN -valued Function-like Element of bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:]
[:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
the Comp of UN || (UN,a) is Relation-like Function-like set
CatStr(# a,(UN,a),(UN,a),(UN,a),(UN,a) #) is non empty non void V55() strict CatStr
UN is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of UN is non empty set
bool the carrier of UN is non empty set
a is non empty Element of bool the carrier of UN
(UN,a) is non empty non void V55() Category-like transitive associative reflexive with_identities Subcategory of UN
(UN,a) is non empty Element of bool the carrier' of UN
the carrier' of UN is non empty set
bool the carrier' of UN is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
(UN,a) is Relation-like (UN,a) -defined a -valued Function-like non empty total quasi_total Element of bool [:(UN,a),a:]
[:(UN,a),a:] is non empty set
bool [:(UN,a),a:] is non empty set
the Source of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
[: the carrier' of UN, the carrier of UN:] is non empty set
bool [: the carrier' of UN, the carrier of UN:] is non empty set
the Source of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
(UN,a) is Relation-like (UN,a) -defined a -valued Function-like non empty total quasi_total Element of bool [:(UN,a),a:]
the Target of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
the Target of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
(UN,a) is Relation-like [:(UN,a),(UN,a):] -defined (UN,a) -valued Function-like Element of bool [:[:(UN,a),(UN,a):],(UN,a):]
[:(UN,a),(UN,a):] is Relation-like the carrier' of UN -defined the carrier' of UN -valued non empty Element of bool [: the carrier' of UN, the carrier' of UN:]
[: the carrier' of UN, the carrier' of UN:] is non empty set
bool [: the carrier' of UN, the carrier' of UN:] is non empty set
[:[:(UN,a),(UN,a):],(UN,a):] is non empty set
bool [:[:(UN,a),(UN,a):],(UN,a):] is non empty set
the Comp of UN is Relation-like [: the carrier' of UN, the carrier' of UN:] -defined the carrier' of UN -valued Function-like Element of bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:]
[:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
the Comp of UN || (UN,a) is Relation-like Function-like set
CatStr(# a,(UN,a),(UN,a),(UN,a),(UN,a) #) is non empty non void V55() strict CatStr
UN is non empty non void V55() Category-like transitive associative reflexive with_identities CatStr
the carrier of UN is non empty set
bool the carrier of UN is non empty set
a is non empty Element of bool the carrier of UN
(UN,a) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of UN
(UN,a) is non empty Element of bool the carrier' of UN
the carrier' of UN is non empty set
bool the carrier' of UN is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of UN : ( b₁ in a & b₂ in a ) } is set
(UN,a) is Relation-like (UN,a) -defined a -valued Function-like non empty total quasi_total Element of bool [:(UN,a),a:]
[:(UN,a),a:] is non empty set
bool [:(UN,a),a:] is non empty set
the Source of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
[: the carrier' of UN, the carrier of UN:] is non empty set
bool [: the carrier' of UN, the carrier of UN:] is non empty set
the Source of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
(UN,a) is Relation-like (UN,a) -defined a -valued Function-like non empty total quasi_total Element of bool [:(UN,a),a:]
the Target of UN is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier' of UN, the carrier of UN:]
the Target of UN | (UN,a) is Relation-like the carrier' of UN -defined the carrier of UN -valued Function-like Element of bool [: the carrier' of UN, the carrier of UN:]
(UN,a) is Relation-like [:(UN,a),(UN,a):] -defined (UN,a) -valued Function-like Element of bool [:[:(UN,a),(UN,a):],(UN,a):]
[:(UN,a),(UN,a):] is Relation-like the carrier' of UN -defined the carrier' of UN -valued non empty Element of bool [: the carrier' of UN, the carrier' of UN:]
[: the carrier' of UN, the carrier' of UN:] is non empty set
bool [: the carrier' of UN, the carrier' of UN:] is non empty set
[:[:(UN,a),(UN,a):],(UN,a):] is non empty set
bool [:[:(UN,a),(UN,a):],(UN,a):] is non empty set
the Comp of UN is Relation-like [: the carrier' of UN, the carrier' of UN:] -defined the carrier' of UN -valued Function-like Element of bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:]
[:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
bool [:[: the carrier' of UN, the carrier' of UN:], the carrier' of UN:] is non empty set
the Comp of UN || (UN,a) is Relation-like Function-like set
CatStr(# a,(UN,a),(UN,a),(UN,a),(UN,a) #) is non empty non void V55() strict CatStr
the carrier of (UN,a) is non empty set
a is non empty ZeroStr
the carrier of a is non empty set
UN is non empty 1-sorted
the carrier of UN is non empty set
0. a is V50(a) Element of the carrier of a
the ZeroF of a is Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
comp Trivial-addLoopStr is Relation-like the carrier of Trivial-addLoopStr -defined the carrier of Trivial-addLoopStr -valued Function-like non empty total quasi_total Element of bool [: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:]
[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:] is non empty set
bool [: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:] is non empty set
bool [:{{}},{{}}:] is non empty set
UN is Relation-like {{}} -defined {{}} -valued Function-like non empty total quasi_total Element of bool [:{{}},{{}}:]
a is set
op1 . a is set
UN . a is set
aa is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
op1 . aa is set
- aa is left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Element of the carrier of Trivial-addLoopStr
UN . aa is set
UN is non empty addMagma
a is non empty right_zeroed addLoopStr
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) Element of the carrier of a
the ZeroF of a is Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
C is Element of the carrier of UN
ii is Element of the carrier of UN
C + ii is Element of the carrier of UN
the addF of UN is Relation-like [: the carrier of UN, the carrier of UN:] -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of UN, the carrier of UN:], the carrier of UN:]
[: the carrier of UN, the carrier of UN:] is non empty set
[:[: the carrier of UN, the carrier of UN:], the carrier of UN:] is non empty set
bool [:[: the carrier of UN, the carrier of UN:], the carrier of UN:] is non empty set
the addF of UN . (C,ii) is Element of the carrier of UN
[C,ii] is V27() set
the addF of UN . [C,ii] is set
(UN,a) . (C + ii) is Element of the carrier of a
(UN,a) . C is Element of the carrier of a
(UN,a) . ii is Element of the carrier of a
((UN,a) . C) + ((UN,a) . ii) is Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the addF of a . (((UN,a) . C),((UN,a) . ii)) is Element of the carrier of a
[((UN,a) . C),((UN,a) . ii)] is V27() set
the addF of a . [((UN,a) . C),((UN,a) . ii)] is set
UN is non empty addMagma
the carrier of UN is non empty set
a is non empty right_zeroed addLoopStr
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
0. a is V50(a) Element of the carrier of a
the ZeroF of a is Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
UN is non empty addMagma
the carrier of UN is non empty set
a is non empty addMagma
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
aa is non empty addMagma
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is non empty set
bool [: the carrier of a, the carrier of aa:] is non empty set
C is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
ii is Relation-like the carrier of a -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of aa:]
ii * C is Relation-like the carrier of UN -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of aa:]
[: the carrier of UN, the carrier of aa:] is non empty set
bool [: the carrier of UN, the carrier of aa:] is non empty set
ii is Element of the carrier of UN
C . ii is Element of the carrier of a
ii . (C . ii) is Element of the carrier of aa
(ii * C) . ii is Element of the carrier of aa
ii is Element of the carrier of UN
C . ii is Element of the carrier of a
ii . (C . ii) is Element of the carrier of aa
(ii * C) . ii is Element of the carrier of aa
ii + ii is Element of the carrier of UN
the addF of UN is Relation-like [: the carrier of UN, the carrier of UN:] -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of UN, the carrier of UN:], the carrier of UN:]
[: the carrier of UN, the carrier of UN:] is non empty set
[:[: the carrier of UN, the carrier of UN:], the carrier of UN:] is non empty set
bool [:[: the carrier of UN, the carrier of UN:], the carrier of UN:] is non empty set
the addF of UN . (ii,ii) is Element of the carrier of UN
[ii,ii] is V27() set
the addF of UN . [ii,ii] is set
(ii * C) . (ii + ii) is Element of the carrier of aa
C . (ii + ii) is Element of the carrier of a
ii . (C . (ii + ii)) is Element of the carrier of aa
(C . ii) + (C . ii) is Element of the carrier of a
the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set
the addF of a . ((C . ii),(C . ii)) is Element of the carrier of a
[(C . ii),(C . ii)] is V27() set
the addF of a . [(C . ii),(C . ii)] is set
ii . ((C . ii) + (C . ii)) is Element of the carrier of aa
((ii * C) . ii) + ((ii * C) . ii) is Element of the carrier of aa
the addF of aa is Relation-like [: the carrier of aa, the carrier of aa:] -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of aa, the carrier of aa:], the carrier of aa:]
[: the carrier of aa, the carrier of aa:] is non empty set
[:[: the carrier of aa, the carrier of aa:], the carrier of aa:] is non empty set
bool [:[: the carrier of aa, the carrier of aa:], the carrier of aa:] is non empty set
the addF of aa . (((ii * C) . ii),((ii * C) . ii)) is Element of the carrier of aa
[((ii * C) . ii),((ii * C) . ii)] is V27() set
the addF of aa . [((ii * C) . ii),((ii * C) . ii)] is set
UN is non empty addMagma
the carrier of UN is non empty set
a is non empty right_zeroed addLoopStr
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
aa is non empty right_zeroed addLoopStr
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is non empty set
bool [: the carrier of a, the carrier of aa:] is non empty set
[: the carrier of UN, the carrier of aa:] is non empty set
bool [: the carrier of UN, the carrier of aa:] is non empty set
C is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
ii is Relation-like the carrier of a -defined the carrier of aa -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of a, the carrier of aa:]
ii * C is Relation-like the carrier of UN -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of aa:]
ia is Relation-like the carrier of UN -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of aa:]
UN is ()
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is ()
the of UN is Relation-like the carrier of the of UN -defined the carrier of the of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of UN, the carrier of the of UN:]
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of the of UN is non empty set
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of the of UN is non empty set
[: the carrier of the of UN, the carrier of the of UN:] is non empty set
bool [: the carrier of the of UN, the carrier of the of UN:] is non empty set
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (UN) is non empty set
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (UN) is non empty set
[: the carrier of (UN), the carrier of (UN):] is non empty set
bool [: the carrier of (UN), the carrier of (UN):] is non empty set
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of a is non empty set
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is non empty set
bool [: the carrier of a, the carrier of aa:] is non empty set
UN is ()
C is Relation-like the carrier of a -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,C) is () ()
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (UN) is non empty set
the carrier of (UN) is non empty set
(UN) is Relation-like the carrier of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (UN), the carrier of (UN):]
[: the carrier of (UN), the carrier of (UN):] is non empty set
bool [: the carrier of (UN), the carrier of (UN):] is non empty set
the of UN is Relation-like the carrier of the of UN -defined the carrier of the of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of UN, the carrier of the of UN:]
the carrier of the of UN is non empty set
the carrier of the of UN is non empty set
[: the carrier of the of UN, the carrier of the of UN:] is non empty set
bool [: the carrier of the of UN, the carrier of the of UN:] is non empty set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,(UN,a)) is () ()
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,a) is ()
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,(UN,a)) is () ()
the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is () ()
( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is Relation-like the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -defined the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :]
the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is non empty set
[: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :] is non empty set
bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :] is non empty set
0. the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is V50( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the ZeroF of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr --> (0. the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is Relation-like the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -defined the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -valued Function-like non empty total quasi_total Element of bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :]
( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ,( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) is () ()
(( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) is Relation-like the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) -defined the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )), the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )):]
the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) is non empty set
the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) is non empty set
[: the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )), the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )):] is non empty set
bool [: the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )), the carrier of (( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )):] is non empty set
the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is Relation-like the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) -defined the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ), the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ):]
the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is non empty set
the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is non empty set
[: the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ), the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ):] is non empty set
bool [: the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ), the carrier of the of ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ):] is non empty set
UN is () ()
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is Relation-like the carrier of the of UN -defined the carrier of the of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of UN, the carrier of the of UN:]
the carrier of the of UN is non empty set
the carrier of the of UN is non empty set
[: the carrier of the of UN, the carrier of the of UN:] is non empty set
bool [: the carrier of the of UN, the carrier of the of UN:] is non empty set
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (UN) is non empty set
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (UN) is non empty set
(UN) is Relation-like the carrier of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (UN), the carrier of (UN):]
[: the carrier of (UN), the carrier of (UN):] is non empty set
bool [: the carrier of (UN), the carrier of (UN):] is non empty set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,a) is () ()
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,(UN,a)) is () ()
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN,a)) is Relation-like the carrier of ((UN,a)) -defined the carrier of ((UN,a)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((UN,a)), the carrier of ((UN,a)):]
the carrier of ((UN,a)) is non empty set
the carrier of ((UN,a)) is non empty set
[: the carrier of ((UN,a)), the carrier of ((UN,a)):] is non empty set
bool [: the carrier of ((UN,a)), the carrier of ((UN,a)):] is non empty set
the of (UN,a) is Relation-like the carrier of the of (UN,a) -defined the carrier of the of (UN,a) -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of (UN,a), the carrier of the of (UN,a):]
the carrier of the of (UN,a) is non empty set
the carrier of the of (UN,a) is non empty set
[: the carrier of the of (UN,a), the carrier of the of (UN,a):] is non empty set
bool [: the carrier of the of (UN,a), the carrier of the of (UN,a):] is non empty set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,a) is () () ()
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,(UN,a)) is () ()
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,a) is () () ()
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,(UN,a)) is () ()
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(aa) is Relation-like the carrier of (aa) -defined the carrier of (aa) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (aa), the carrier of (aa):]
the carrier of (aa) is non empty set
the carrier of (aa) is non empty set
[: the carrier of (aa), the carrier of (aa):] is non empty set
bool [: the carrier of (aa), the carrier of (aa):] is non empty set
the of aa is Relation-like the carrier of the of aa -defined the carrier of the of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of aa, the carrier of the of aa:]
the carrier of the of aa is non empty set
the carrier of the of aa is non empty set
[: the carrier of the of aa, the carrier of the of aa:] is non empty set
bool [: the carrier of the of aa, the carrier of the of aa:] is non empty set
C is () () ()
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of UN is non empty set
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
aa is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,aa) is () ()
((UN,a,aa)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a,aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ((UN,a,aa)) is non empty set
((UN,a,aa)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a,aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ((UN,a,aa)) is non empty set
((UN,a,aa)) is Relation-like the carrier of ((UN,a,aa)) -defined the carrier of ((UN,a,aa)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((UN,a,aa)), the carrier of ((UN,a,aa)):]
[: the carrier of ((UN,a,aa)), the carrier of ((UN,a,aa)):] is non empty set
bool [: the carrier of ((UN,a,aa)), the carrier of ((UN,a,aa)):] is non empty set
the of (UN,a,aa) is Relation-like the carrier of the of (UN,a,aa) -defined the carrier of the of (UN,a,aa) -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):]
the carrier of the of (UN,a,aa) is non empty set
the carrier of the of (UN,a,aa) is non empty set
[: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):] is non empty set
bool [: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):] is non empty set
UN is non empty addMagma
id UN is Relation-like the carrier of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
the carrier of UN is non empty set
[: the carrier of UN, the carrier of UN:] is non empty set
bool [: the carrier of UN, the carrier of UN:] is non empty set
id the carrier of UN is Relation-like the carrier of UN -defined the carrier of UN -valued non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
aa is Element of the carrier of UN
C is Element of the carrier of UN
aa + C is Element of the carrier of UN
the addF of UN is Relation-like [: the carrier of UN, the carrier of UN:] -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of UN, the carrier of UN:], the carrier of UN:]
[:[: the carrier of UN, the carrier of UN:], the carrier of UN:] is non empty set
bool [:[: the carrier of UN, the carrier of UN:], the carrier of UN:] is non empty set
the addF of UN . (aa,C) is Element of the carrier of UN
[aa,C] is V27() set
the addF of UN . [aa,C] is set
(id UN) . (aa + C) is Element of the carrier of UN
(id UN) . aa is Element of the carrier of UN
(id UN) . C is Element of the carrier of UN
((id UN) . aa) + ((id UN) . C) is Element of the carrier of UN
the addF of UN . (((id UN) . aa),((id UN) . C)) is Element of the carrier of UN
[((id UN) . aa),((id UN) . C)] is V27() set
the addF of UN . [((id UN) . aa),((id UN) . C)] is set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
id UN is Relation-like the carrier of UN -defined the carrier of UN -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of UN:]
the carrier of UN is non empty set
[: the carrier of UN, the carrier of UN:] is non empty set
bool [: the carrier of UN, the carrier of UN:] is non empty set
id the carrier of UN is Relation-like the carrier of UN -defined the carrier of UN -valued non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
(UN,UN,(id UN)) is () ()
((UN,UN,(id UN))) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,UN,(id UN)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ((UN,UN,(id UN))) is non empty set
((UN,UN,(id UN))) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,UN,(id UN)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ((UN,UN,(id UN))) is non empty set
((UN,UN,(id UN))) is Relation-like the carrier of ((UN,UN,(id UN))) -defined the carrier of ((UN,UN,(id UN))) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((UN,UN,(id UN))), the carrier of ((UN,UN,(id UN))):]
[: the carrier of ((UN,UN,(id UN))), the carrier of ((UN,UN,(id UN))):] is non empty set
bool [: the carrier of ((UN,UN,(id UN))), the carrier of ((UN,UN,(id UN))):] is non empty set
the of (UN,UN,(id UN)) is Relation-like the carrier of the of (UN,UN,(id UN)) -defined the carrier of the of (UN,UN,(id UN)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):]
the carrier of the of (UN,UN,(id UN)) is non empty set
the carrier of the of (UN,UN,(id UN)) is non empty set
[: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):] is non empty set
bool [: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):] is non empty set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN) is () (UN,UN)
id UN is Relation-like the carrier of UN -defined the carrier of UN -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of UN:]
the carrier of UN is non empty set
[: the carrier of UN, the carrier of UN:] is non empty set
bool [: the carrier of UN, the carrier of UN:] is non empty set
id the carrier of UN is Relation-like the carrier of UN -defined the carrier of UN -valued non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
(UN,UN,(id UN)) is () ()
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,a) is () () ()
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,(UN,a)) is () ()
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ((UN,a)) is non empty set
((UN,a)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN,a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ((UN,a)) is non empty set
((UN,a)) is Relation-like the carrier of ((UN,a)) -defined the carrier of ((UN,a)) -valued Function-like non empty total quasi_total Element of bool [: the carrier of ((UN,a)), the carrier of ((UN,a)):]
[: the carrier of ((UN,a)), the carrier of ((UN,a)):] is non empty set
bool [: the carrier of ((UN,a)), the carrier of ((UN,a)):] is non empty set
the of (UN,a) is Relation-like the carrier of the of (UN,a) -defined the carrier of the of (UN,a) -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of (UN,a), the carrier of the of (UN,a):]
the carrier of the of (UN,a) is non empty set
the carrier of the of (UN,a) is non empty set
[: the carrier of the of (UN,a), the carrier of the of (UN,a):] is non empty set
bool [: the carrier of the of (UN,a), the carrier of the of (UN,a):] is non empty set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of UN is non empty set
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
aa is () (UN,a)
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is Relation-like the carrier of the of aa -defined the carrier of the of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of aa, the carrier of the of aa:]
the carrier of the of aa is non empty set
the carrier of the of aa is non empty set
[: the carrier of the of aa, the carrier of the of aa:] is non empty set
bool [: the carrier of the of aa, the carrier of the of aa:] is non empty set
( the of aa, the of aa, the of aa) is () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,C) is () ()
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of UN is non empty set
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
aa is () () (UN,a)
C is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,C) is () ()
UN is () ()
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is () () ()
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of a is non empty set
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is non empty set
bool [: the carrier of a, the carrier of aa:] is non empty set
C is () (a,aa)
ii is Relation-like the carrier of a -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,ii) is () ()
UN is () ()
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is () ()
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is () ()
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is () ()
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is Relation-like the carrier of the of UN -defined the carrier of the of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of UN, the carrier of the of UN:]
the carrier of the of UN is non empty set
the carrier of the of UN is non empty set
[: the carrier of the of UN, the carrier of the of UN:] is non empty set
bool [: the carrier of the of UN, the carrier of the of UN:] is non empty set
( the of UN, the of UN, the of UN) is () ()
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is Relation-like the carrier of the of a -defined the carrier of the of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of a, the carrier of the of a:]
the carrier of the of a is non empty set
the carrier of the of a is non empty set
[: the carrier of the of a, the carrier of the of a:] is non empty set
bool [: the carrier of the of a, the carrier of the of a:] is non empty set
( the of a, the of a, the of a) is () ()
C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of aa is non empty set
the carrier of C is non empty set
[: the carrier of aa, the carrier of C:] is non empty set
bool [: the carrier of aa, the carrier of C:] is non empty set
ia is Relation-like the carrier of aa -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,ia) is () ()
the carrier of ii is non empty set
[: the carrier of C, the carrier of ii:] is non empty set
bool [: the carrier of C, the carrier of ii:] is non empty set
ii is Relation-like the carrier of C -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of C, the carrier of ii:]
(C,ii,ii) is () ()
ii * ia is Relation-like the carrier of aa -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of ii:]
[: the carrier of aa, the carrier of ii:] is non empty set
bool [: the carrier of aa, the carrier of ii:] is non empty set
(aa,ii,(ii * ia)) is () ()
ii is () () ()
gf is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of gf is non empty set
hg is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of hg is non empty set
[: the carrier of gf, the carrier of hg:] is non empty set
bool [: the carrier of gf, the carrier of hg:] is non empty set
c₉ is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of c₉ is non empty set
[: the carrier of c₉, the carrier of gf:] is non empty set
bool [: the carrier of c₉, the carrier of gf:] is non empty set
f is Relation-like the carrier of gf -defined the carrier of hg -valued Function-like non empty total quasi_total Element of bool [: the carrier of gf, the carrier of hg:]
(gf,hg,f) is () ()
ia is Relation-like the carrier of c₉ -defined the carrier of gf -valued Function-like non empty total quasi_total Element of bool [: the carrier of c₉, the carrier of gf:]
(c₉,gf,ia) is () ()
f * ia is Relation-like the carrier of c₉ -defined the carrier of hg -valued Function-like non empty total quasi_total Element of bool [: the carrier of c₉, the carrier of hg:]
[: the carrier of c₉, the carrier of hg:] is non empty set
bool [: the carrier of c₉, the carrier of hg:] is non empty set
(c₉,hg,(f * ia)) is () ()
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is () (aa,C)
the carrier of aa is non empty set
the carrier of ia is non empty set
[: the carrier of aa, the carrier of ia:] is non empty set
bool [: the carrier of aa, the carrier of ia:] is non empty set
ii is () (aa,ia)
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is Relation-like the carrier of the of ii -defined the carrier of the of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of ii, the carrier of the of ii:]
the carrier of the of ii is non empty set
the carrier of the of ii is non empty set
[: the carrier of the of ii, the carrier of the of ii:] is non empty set
bool [: the carrier of the of ii, the carrier of the of ii:] is non empty set
( the of ii, the of ii, the of ii) is () ()
c₉ is Relation-like the carrier of aa -defined the carrier of ia -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of ia:]
(aa,ia,c₉) is () ()
hg is () () ()
f is () () ()
the carrier of ii is non empty set
[: the carrier of ia, the carrier of ii:] is non empty set
bool [: the carrier of ia, the carrier of ii:] is non empty set
gf is () (ia,ii)
the of gf is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of gf is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of gf is Relation-like the carrier of the of gf -defined the carrier of the of gf -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of gf, the carrier of the of gf:]
the carrier of the of gf is non empty set
the carrier of the of gf is non empty set
[: the carrier of the of gf, the carrier of the of gf:] is non empty set
bool [: the carrier of the of gf, the carrier of the of gf:] is non empty set
( the of gf, the of gf, the of gf) is () ()
ia is Relation-like the carrier of ia -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of ia, the carrier of ii:]
(ia,ii,ia) is () ()
ia * c₉ is Relation-like the carrier of aa -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of ii:]
[: the carrier of aa, the carrier of ii:] is non empty set
bool [: the carrier of aa, the carrier of ii:] is non empty set
(aa,ii,(ia * c₉)) is () ()
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is () (a,aa)
ii is () (UN,a)
(C,ii) is () () ()
the carrier of a is non empty set
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is non empty set
bool [: the carrier of a, the carrier of aa:] is non empty set
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of C is Relation-like the carrier of the of C -defined the carrier of the of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of C, the carrier of the of C:]
the carrier of the of C is non empty set
the carrier of the of C is non empty set
[: the carrier of the of C, the carrier of the of C:] is non empty set
bool [: the carrier of the of C, the carrier of the of C:] is non empty set
( the of C, the of C, the of C) is () ()
ia is Relation-like the carrier of a -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,ia) is () ()
the carrier of UN is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is Relation-like the carrier of the of ii -defined the carrier of the of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of ii, the carrier of the of ii:]
the carrier of the of ii is non empty set
the carrier of the of ii is non empty set
[: the carrier of the of ii, the carrier of the of ii:] is non empty set
bool [: the carrier of the of ii, the carrier of the of ii:] is non empty set
( the of ii, the of ii, the of ii) is () ()
ii is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,ii) is () ()
(C) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia * ii is Relation-like the carrier of UN -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of aa:]
[: the carrier of UN, the carrier of aa:] is non empty set
bool [: the carrier of UN, the carrier of aa:] is non empty set
(UN,aa,(ia * ii)) is () ()
((C,ii)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (C,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((C,ii)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (C,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is () (a,aa)
ii is () (UN,a)
(C,ii) is () () ()
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of a is non empty set
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is non empty set
bool [: the carrier of a, the carrier of aa:] is non empty set
the carrier of UN is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
C is () (a,aa)
ii is () (UN,a)
(UN,a,aa,C,ii) is () () (UN,aa)
ia is Relation-like the carrier of a -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,ia) is () ()
ii is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,ii) is () ()
ia * ii is Relation-like the carrier of UN -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of aa:]
[: the carrier of UN, the carrier of aa:] is non empty set
bool [: the carrier of UN, the carrier of aa:] is non empty set
(UN,aa,(ia * ii)) is () ()
(C) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is () () ()
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is () () ()
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(a,UN) is () () ()
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (UN) is non empty set
the carrier of (UN) is non empty set
[: the carrier of (UN), the carrier of (UN):] is non empty set
bool [: the carrier of (UN), the carrier of (UN):] is non empty set
ia is () () ((UN),(UN))
ii is Relation-like the carrier of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (UN), the carrier of (UN):]
((UN),(UN),ii) is () ()
the carrier of (a) is non empty set
[: the carrier of (UN), the carrier of (a):] is non empty set
bool [: the carrier of (UN), the carrier of (a):] is non empty set
ii is () () ((UN),(a))
c₉ is Relation-like the carrier of (UN) -defined the carrier of (a) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (UN), the carrier of (a):]
((UN),(a),c₉) is () ()
c₉ * ii is Relation-like the carrier of (UN) -defined the carrier of (a) -valued Function-like non empty total quasi_total Element of bool [: the carrier of (UN), the carrier of (a):]
[: the carrier of (UN), the carrier of (a):] is non empty set
bool [: the carrier of (UN), the carrier of (a):] is non empty set
((UN),(a),(c₉ * ii)) is () ()
a is () () ()
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is () () ()
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(a,UN) is () () ()
((a,UN)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (a,UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((a,UN)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (a,UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of aa is non empty set
C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of C is non empty set
[: the carrier of aa, the carrier of C:] is non empty set
bool [: the carrier of aa, the carrier of C:] is non empty set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ii is non empty set
[: the carrier of C, the carrier of ii:] is non empty set
bool [: the carrier of C, the carrier of ii:] is non empty set
ia is Relation-like the carrier of aa -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,ia) is () ()
ii is Relation-like the carrier of C -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of C, the carrier of ii:]
(C,ii,ii) is () ()
ii * ia is Relation-like the carrier of aa -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of ii:]
[: the carrier of aa, the carrier of ii:] is non empty set
bool [: the carrier of aa, the carrier of ii:] is non empty set
(aa,ii,(ii * ia)) is () ()
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of aa is non empty set
C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of C is non empty set
[: the carrier of aa, the carrier of C:] is non empty set
bool [: the carrier of aa, the carrier of C:] is non empty set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ii is non empty set
[: the carrier of C, the carrier of ii:] is non empty set
bool [: the carrier of C, the carrier of ii:] is non empty set
ia is Relation-like the carrier of aa -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,ia) is () ()
ii is Relation-like the carrier of C -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of C, the carrier of ii:]
(C,ii,ii) is () ()
ii * ia is Relation-like the carrier of aa -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of ii:]
[: the carrier of aa, the carrier of ii:] is non empty set
bool [: the carrier of aa, the carrier of ii:] is non empty set
(aa,ii,(ii * ia)) is () ()
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is () () (UN,a)
ia is () () (a,aa)
(UN,a,aa,ia,ii) is () () (UN,aa)
ii is () () (aa,C)
(UN,aa,C,ii,(UN,a,aa,ia,ii)) is () () (UN,C)
(a,aa,C,ii,ia) is () () (a,C)
(UN,a,C,(a,aa,C,ii,ia),ii) is () () (UN,C)
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
ii is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,ii) is () ()
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is non empty set
bool [: the carrier of a, the carrier of aa:] is non empty set
c₉ is Relation-like the carrier of a -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,c₉) is () ()
the carrier of C is non empty set
[: the carrier of aa, the carrier of C:] is non empty set
bool [: the carrier of aa, the carrier of C:] is non empty set
gf is Relation-like the carrier of aa -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,gf) is () ()
gf * c₉ is Relation-like the carrier of a -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of C:]
[: the carrier of a, the carrier of C:] is non empty set
bool [: the carrier of a, the carrier of C:] is non empty set
(a,C,(gf * c₉)) is () ()
c₉ * ii is Relation-like the carrier of UN -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of aa:]
[: the carrier of UN, the carrier of aa:] is non empty set
bool [: the carrier of UN, the carrier of aa:] is non empty set
(UN,aa,(c₉ * ii)) is () ()
gf * (c₉ * ii) is Relation-like the carrier of UN -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of C:]
[: the carrier of UN, the carrier of C:] is non empty set
bool [: the carrier of UN, the carrier of C:] is non empty set
(UN,C,(gf * (c₉ * ii))) is () ()
(gf * c₉) * ii is Relation-like the carrier of UN -defined the carrier of C -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of C:]
(UN,C,((gf * c₉) * ii)) is () ()
aa is () () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is () () ()
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is () () ()
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(a,UN) is () () ()
(aa,(a,UN)) is () () ()
(aa,a) is () () ()
((aa,a),UN) is () () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia is () ((a),(aa))
ii is () ((UN),(a))
ii is () ((UN),(UN))
((UN),(UN),(a),ii,ii) is () () ((UN),(a))
((UN),(a),(aa),ia,((UN),(UN),(a),ii,ii)) is () () ((UN),(aa))
((UN),(a),(aa),ia,ii) is () () ((UN),(aa))
((UN),(UN),(aa),((UN),(a),(aa),ia,ii),ii) is () () ((UN),(aa))
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN) is () () (UN,UN)
id UN is Relation-like the carrier of UN -defined the carrier of UN -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of UN:]
the carrier of UN is non empty set
[: the carrier of UN, the carrier of UN:] is non empty set
bool [: the carrier of UN, the carrier of UN:] is non empty set
id the carrier of UN is Relation-like the carrier of UN -defined the carrier of UN -valued non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
(UN,UN,(id UN)) is () ()
((UN)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is () () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),aa) is () () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (aa) is non empty set
[: the carrier of (aa), the carrier of UN:] is non empty set
bool [: the carrier of (aa), the carrier of UN:] is non empty set
ii is () ((aa),UN)
ia is Relation-like the carrier of (aa) -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of (aa), the carrier of UN:]
((aa),UN,ia) is () ()
(id UN) * ia is Relation-like the carrier of (aa) -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of (aa), the carrier of UN:]
aa is () () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(aa,(UN)) is () () ()
(aa) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of (aa) is non empty set
[: the carrier of UN, the carrier of (aa):] is non empty set
bool [: the carrier of UN, the carrier of (aa):] is non empty set
ii is () (UN,(aa))
ia is Relation-like the carrier of UN -defined the carrier of (aa) -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of (aa):]
(UN,(aa),ia) is () ()
ia * (id UN) is Relation-like the carrier of UN -defined the carrier of (aa) -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of (aa):]
{Trivial-addLoopStr} is non empty set
a is set
UN is non empty () set
a is Element of UN
UN is non empty () set
the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ) is () () ( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )
id the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is Relation-like the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -defined the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :]
the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is non empty set
[: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :] is non empty set
bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :] is non empty set
id the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr is Relation-like the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -defined the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr -valued non empty total quasi_total Element of bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr :]
( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr , the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr ,(id the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )) is () ()
{( the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr )} is non empty set
a is set
UN is non empty () set
a is Element of UN
UN is non empty () set
the () (UN) is () (UN)
UN is () () ()
{UN} is non empty set
a is set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,a) is () () (UN,a)
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
the carrier of UN is non empty set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,(UN,a)) is () ()
{(UN,a)} is non empty set
aa is non empty () set
C is () (aa)
UN is non empty set
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is Element of UN
C is set
C is non empty () set
ii is () (C)
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is () () (UN,a)
{aa} is non empty set
C is Element of {aa}
UN is 1-sorted
the carrier of UN is set
a is 1-sorted
the carrier of a is set
[: the carrier of UN, the carrier of a:] is set
bool [: the carrier of UN, the carrier of a:] is non empty set
aa is set
UN is 1-sorted
the carrier of UN is set
a is 1-sorted
the carrier of a is set
Funcs ( the carrier of UN, the carrier of a) is functional set
aa is set
[: the carrier of UN, the carrier of a:] is set
bool [: the carrier of UN, the carrier of a:] is non empty set
UN is 1-sorted
a is non empty 1-sorted
(UN,a) is (UN,a)
the carrier of UN is set
the carrier of a is non empty set
Funcs ( the carrier of UN, the carrier of a) is functional non empty set
UN is 1-sorted
a is non empty 1-sorted
(UN,a) is non empty (UN,a)
the carrier of UN is set
the carrier of a is non empty set
Funcs ( the carrier of UN, the carrier of a) is functional non empty set
UN is 1-sorted
a is non empty 1-sorted
aa is non empty (UN,a)
the carrier of UN is set
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is set
bool [: the carrier of UN, the carrier of a:] is non empty set
C is Element of aa
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of UN is non empty set
the carrier of a is non empty set
(UN,a) is non empty (UN,a)
Funcs ( the carrier of UN, the carrier of a) is functional non empty set
(UN,a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of UN, the carrier of a:]
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
0. a is V50(a) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the ZeroF of a is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of a
the carrier of UN --> (0. a) is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
{ (UN,a,b₁) where b₁ is Relation-like the carrier of UN -defined the carrier of a -valued Function-like total quasi_total (UN,a,(UN,a)) : b₁ is additive } is set
aa is Relation-like the carrier of UN -defined the carrier of a -valued Function-like total quasi_total (UN,a,(UN,a))
(UN,a,aa) is () ()
ii is non empty set
ia is set
ii is Relation-like the carrier of UN -defined the carrier of a -valued Function-like total quasi_total (UN,a,(UN,a))
(UN,a,ii) is () ()
ia is Element of ii
ia is set
ii is () () (UN,a)
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is Relation-like the carrier of the of ii -defined the carrier of the of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of ii, the carrier of the of ii:]
the carrier of the of ii is non empty set
the carrier of the of ii is non empty set
[: the carrier of the of ii, the carrier of the of ii:] is non empty set
bool [: the carrier of the of ii, the carrier of the of ii:] is non empty set
ii is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
c₉ is Relation-like the carrier of UN -defined the carrier of a -valued Function-like total quasi_total (UN,a,(UN,a))
(UN,a,c₉) is () ()
ia is non empty () (UN,a)
ii is set
ii is set
aa is non empty () (UN,a)
C is non empty () (UN,a)
ii is set
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty () (UN,a)
C is Element of aa
UN is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty () (UN,a)
the () (UN,a,aa) is () (UN,a,aa)
UN is set
a is set
aa is set
C is set
ii is set
ia is set
ii is set
[C,ii,ia,ii] is V27() V28() V29() set
[C,ii,ia] is V27() V28() set
[C,ii] is V27() set
[[C,ii],ia] is V27() set
[[C,ii,ia],ii] is V27() set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ii is non empty set
the addF of ii is Relation-like [: the carrier of ii, the carrier of ii:] -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]
[: the carrier of ii, the carrier of ii:] is non empty set
[:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is non empty set
bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is non empty set
comp ii is Relation-like the carrier of ii -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of ii, the carrier of ii:]
bool [: the carrier of ii, the carrier of ii:] is non empty set
0. ii is V50(ii) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ii
the ZeroF of ii is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ii
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ii is non empty set
the addF of ii is Relation-like [: the carrier of ii, the carrier of ii:] -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]
[: the carrier of ii, the carrier of ii:] is non empty set
[:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is non empty set
bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is non empty set
comp ii is Relation-like the carrier of ii -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of ii, the carrier of ii:]
bool [: the carrier of ii, the carrier of ii:] is non empty set
0. ii is V50(ii) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ii
the ZeroF of ii is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ii
c₉ is set
gf is set
hg is set
f is set
[c₉,gf,hg,f] is V27() V28() V29() set
[c₉,gf,hg] is V27() V28() set
[c₉,gf] is V27() set
[[c₉,gf],hg] is V27() set
[[c₉,gf,hg],f] is V27() set
ia is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ia is non empty set
the addF of ia is Relation-like [: the carrier of ia, the carrier of ia:] -defined the carrier of ia -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ia, the carrier of ia:], the carrier of ia:]
[: the carrier of ia, the carrier of ia:] is non empty set
[:[: the carrier of ia, the carrier of ia:], the carrier of ia:] is non empty set
bool [:[: the carrier of ia, the carrier of ia:], the carrier of ia:] is non empty set
comp ia is Relation-like the carrier of ia -defined the carrier of ia -valued Function-like non empty total quasi_total Element of bool [: the carrier of ia, the carrier of ia:]
bool [: the carrier of ia, the carrier of ia:] is non empty set
0. ia is V50(ia) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ia
the ZeroF of ia is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ia
ia is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ia is non empty set
the addF of ia is Relation-like [: the carrier of ia, the carrier of ia:] -defined the carrier of ia -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ia, the carrier of ia:], the carrier of ia:]
[: the carrier of ia, the carrier of ia:] is non empty set
[:[: the carrier of ia, the carrier of ia:], the carrier of ia:] is non empty set
bool [:[: the carrier of ia, the carrier of ia:], the carrier of ia:] is non empty set
comp ia is Relation-like the carrier of ia -defined the carrier of ia -valued Function-like non empty total quasi_total Element of bool [: the carrier of ia, the carrier of ia:]
bool [: the carrier of ia, the carrier of ia:] is non empty set
0. ia is V50(ia) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ia
the ZeroF of ia is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ia
UN is non empty V15() V22() V23() universal set
C is Element of UN
{C} is non empty Element of UN
Extract {} is Element of {{}}
a is Element of UN
aa is Element of UN
ia is Element of UN
[{C},a,aa,ia] is V27() V28() V29() set
[{C},a,aa] is V27() V28() set
[{C},a] is V27() set
[[{C},a],aa] is V27() set
[[{C},a,aa],ia] is V27() set
ii is V27() V28() V29() set
the addF of Trivial-addLoopStr is Relation-like [: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:] -defined the carrier of Trivial-addLoopStr -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:], the carrier of Trivial-addLoopStr:]
[:[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:], the carrier of Trivial-addLoopStr:] is non empty set
bool [:[: the carrier of Trivial-addLoopStr, the carrier of Trivial-addLoopStr:], the carrier of Trivial-addLoopStr:] is non empty set
UN is non empty V15() V22() V23() universal set
a is set
aa is set
C is set
a is set
aa is set
ii is set
C is set
a is set
aa is set
UN is non empty V15() V22() V23() universal set
(UN) is set
a is set
UN is non empty V15() V22() V23() universal set
(UN) is set
UN is non empty V15() V22() V23() universal set
(UN) is non empty set
a is Element of (UN)
aa is set
C is set
ii is set
ia is set
ii is set
[C,ii,ia,ii] is V27() V28() V29() set
[C,ii,ia] is V27() V28() set
[C,ii] is V27() set
[[C,ii],ia] is V27() set
[[C,ii,ia],ii] is V27() set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of ii is non empty set
the addF of ii is Relation-like [: the carrier of ii, the carrier of ii:] -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]
[: the carrier of ii, the carrier of ii:] is non empty set
[:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is non empty set
bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is non empty set
comp ii is Relation-like the carrier of ii -defined the carrier of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of ii, the carrier of ii:]
bool [: the carrier of ii, the carrier of ii:] is non empty set
0. ii is V50(ii) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ii
the ZeroF of ii is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ii
UN is non empty V15() V22() V23() universal set
(UN) is non empty set
a is set
UN is non empty () set
the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)) is non empty () ( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN))
{ (b₁,b₂) where b₁, b₂ is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) : verum } is set
( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)) is () () ( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN))
( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)) is Relation-like the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) -defined the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN):]
the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) is non empty set
[: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN):] is non empty set
bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN):] is non empty set
0. the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) is V50( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the ZeroF of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) --> (0. the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)) is Relation-like the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) -defined the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the carrier of the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN):]
( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN),( the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN), the non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN))) is () ()
union { (b₁,b₂) where b₁, b₂ is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN) : verum } is set
ii is non empty set
ia is set
ii is set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
c₉ is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
(ii,c₉) is non empty () (ii,c₉)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
(ii,ii) is non empty () (ii,ii)
ia is set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ia is non empty () set
ii is set
ii is set
c₉ is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
gf is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
a is non empty () set
aa is non empty () set
C is set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ia is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ia is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
UN is non empty () set
(UN) is non empty () set
a is () ((UN))
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
C is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is () (aa,C)
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(a) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
C is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is () (aa,C)
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty () set
a is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
(a) is () () (a,a)
id a is Relation-like the carrier of a -defined the carrier of a -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of a, the carrier of a:]
the carrier of a is non empty set
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
id the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued non empty total quasi_total Element of bool [: the carrier of a, the carrier of a:]
(a,a,(id a)) is () ()
(UN) is non empty () set
aa is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
(aa) is () () (aa,aa)
id aa is Relation-like the carrier of aa -defined the carrier of aa -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of aa, the carrier of aa:]
the carrier of aa is non empty set
[: the carrier of aa, the carrier of aa:] is non empty set
bool [: the carrier of aa, the carrier of aa:] is non empty set
id the carrier of aa is Relation-like the carrier of aa -defined the carrier of aa -valued non empty total quasi_total Element of bool [: the carrier of aa, the carrier of aa:]
(aa,aa,(id aa)) is () ()
UN is non empty () set
(UN) is non empty () set
[:(UN),UN:] is non empty set
bool [:(UN),UN:] is non empty set
a is Relation-like (UN) -defined UN -valued Function-like non empty total quasi_total Element of bool [:(UN),UN:]
aa is () ((UN))
a . aa is Element of UN
(UN,aa) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is Relation-like (UN) -defined UN -valued Function-like non empty total quasi_total Element of bool [:(UN),UN:]
aa is Relation-like (UN) -defined UN -valued Function-like non empty total quasi_total Element of bool [:(UN),UN:]
C is () ((UN))
a . C is Element of UN
(UN,C) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa . C is Element of UN
a is Relation-like (UN) -defined UN -valued Function-like non empty total quasi_total Element of bool [:(UN),UN:]
aa is () ((UN))
a . aa is Element of UN
(UN,aa) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
a is Relation-like (UN) -defined UN -valued Function-like non empty total quasi_total Element of bool [:(UN),UN:]
aa is Relation-like (UN) -defined UN -valued Function-like non empty total quasi_total Element of bool [:(UN),UN:]
C is () ((UN))
a . C is Element of UN
(UN,C) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
aa . C is Element of UN
UN is non empty () set
(UN) is non empty () set
aa is () ((UN))
(UN,aa) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is () ((UN))
(UN,C) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ia is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
UN is non empty () set
(UN) is non empty () set
aa is () ((UN))
(UN,aa) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is () ((UN))
(UN,C) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(aa,C) is () () ()
ia is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
c₉ is () (ia,ii)
ii is () (ii,ia)
(ii,ia,ii,c₉,ii) is () () (ii,ii)
UN is non empty () set
(UN) is non empty () set
[:(UN),(UN):] is non empty set
[:[:(UN),(UN):],(UN):] is non empty set
bool [:[:(UN),(UN):],(UN):] is non empty set
aa is () ((UN))
(UN,aa) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
C is () ((UN))
(UN,C) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(aa,C) is () () ()
aa is Relation-like [:(UN),(UN):] -defined (UN) -valued Function-like Element of bool [:[:(UN),(UN):],(UN):]
proj1 aa is Relation-like set
C is () ((UN))
ii is () ((UN))
[C,ii] is V27() set
(UN,C) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia is () ((UN))
(UN,ia) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is () ((UN))
(UN,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
[ia,ii] is V27() set
ii is () ((UN))
c₉ is () ((UN))
[ii,c₉] is V27() set
aa . (ii,c₉) is set
aa . [ii,c₉] is set
(ii,c₉) is () () ()
aa is Relation-like [:(UN),(UN):] -defined (UN) -valued Function-like Element of bool [:[:(UN),(UN):],(UN):]
proj1 aa is Relation-like set
C is Relation-like [:(UN),(UN):] -defined (UN) -valued Function-like Element of bool [:[:(UN),(UN):],(UN):]
proj1 C is Relation-like set
ia is set
ii is () ((UN))
ii is () ((UN))
[ii,ii] is V27() set
(UN,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia is set
ii is set
[ia,ii] is V27() set
aa . (ia,ii) is set
aa . [ia,ii] is set
C . (ia,ii) is set
C . [ia,ii] is set
ii is () ((UN))
c₉ is () ((UN))
aa . (ii,c₉) is set
[ii,c₉] is V27() set
aa . [ii,c₉] is set
(ii,c₉) is () () ()
ia is set
ii is () ((UN))
ii is () ((UN))
[ii,ii] is V27() set
(UN,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(UN,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like (UN)
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier' of (UN) is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
proj1 the Comp of (UN) is Relation-like set
ii is Element of the carrier' of (UN)
C is Element of the carrier' of (UN)
[ii,C] is V27() set
dom ii is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . ii is Element of the carrier of (UN)
cod C is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . C is Element of the carrier of (UN)
ii is () (((UN)))
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia is () (((UN)))
((UN),ia) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier' of (UN) is non empty set
the carrier of (UN) is non empty set
ii is Element of the carrier' of (UN)
ia is () (((UN)))
ii is Element of the carrier of (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
c₉ is set
gf is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
hg is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
gf is set
hg is set
f is set
ia is set
[gf,hg,f,ia] is V27() V28() V29() set
[gf,hg,f] is V27() V28() set
[gf,hg] is V27() set
[[gf,hg],f] is V27() set
[[gf,hg,f],ia] is V27() set
c₁₄ is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of c₁₄ is non empty set
the addF of c₁₄ is Relation-like [: the carrier of c₁₄, the carrier of c₁₄:] -defined the carrier of c₁₄ -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of c₁₄, the carrier of c₁₄:], the carrier of c₁₄:]
[: the carrier of c₁₄, the carrier of c₁₄:] is non empty set
[:[: the carrier of c₁₄, the carrier of c₁₄:], the carrier of c₁₄:] is non empty set
bool [:[: the carrier of c₁₄, the carrier of c₁₄:], the carrier of c₁₄:] is non empty set
comp c₁₄ is Relation-like the carrier of c₁₄ -defined the carrier of c₁₄ -valued Function-like non empty total quasi_total Element of bool [: the carrier of c₁₄, the carrier of c₁₄:]
bool [: the carrier of c₁₄, the carrier of c₁₄:] is non empty set
0. c₁₄ is V50(c₁₄) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of c₁₄
the ZeroF of c₁₄ is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of c₁₄
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier' of (UN) is non empty set
proj1 ((UN)) is Relation-like set
ii is Element of the carrier' of (UN)
ia is Element of the carrier' of (UN)
dom ia is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . ia is Element of the carrier of (UN)
cod ii is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . ii is Element of the carrier of (UN)
ia (*) ii is Element of the carrier' of (UN)
dom ii is Element of the carrier of (UN)
the Source of (UN) . ii is Element of the carrier of (UN)
cod ia is Element of the carrier of (UN)
the Target of (UN) . ia is Element of the carrier of (UN)
ii is () (((UN)))
ii is () (((UN)))
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
[ii,ii] is V27() set
(ii,ii) is () () ()
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
[ia,ii] is V27() set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
proj1 the Comp of (UN) is Relation-like set
((UN)) . (ii,ii) is set
((UN)) . [ii,ii] is set
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier' of (UN) is non empty set
C is Element of the carrier' of (UN)
dom C is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . C is Element of the carrier of (UN)
aa is Element of the carrier' of (UN)
cod aa is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . aa is Element of the carrier of (UN)
C (*) aa is Element of the carrier' of (UN)
dom (C (*) aa) is Element of the carrier of (UN)
the Source of (UN) . (C (*) aa) is Element of the carrier of (UN)
dom aa is Element of the carrier of (UN)
the Source of (UN) . aa is Element of the carrier of (UN)
cod (C (*) aa) is Element of the carrier of (UN)
the Target of (UN) . (C (*) aa) is Element of the carrier of (UN)
cod C is Element of the carrier of (UN)
the Target of (UN) . C is Element of the carrier of (UN)
ii is () () (((UN)))
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ia is () () (((UN)))
((UN),ia) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(ii,ia) is () () ()
ii is () (((UN)))
((ii,ia)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (ii,ia) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ia) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((ii,ia)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (ii,ia) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
aa is Element of the carrier of (UN)
Hom (aa,aa) is Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = aa & cod b₁ = aa ) } is set
C is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
ii is set
((UN),C) is () () (((UN)))
(C) is () () (C,C)
id C is Relation-like the carrier of C -defined the carrier of C -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of C, the carrier of C:]
the carrier of C is non empty set
[: the carrier of C, the carrier of C:] is non empty set
bool [: the carrier of C, the carrier of C:] is non empty set
id the carrier of C is Relation-like the carrier of C -defined the carrier of C -valued non empty total quasi_total Element of bool [: the carrier of C, the carrier of C:]
(C,C,(id C)) is () ()
ii is set
ii is set
c₉ is set
gf is set
[ii,ii,c₉,gf] is V27() V28() V29() set
[ii,ii,c₉] is V27() V28() set
[ii,ii] is V27() set
[[ii,ii],c₉] is V27() set
[[ii,ii,c₉],gf] is V27() set
f is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier of f is non empty set
the addF of f is Relation-like [: the carrier of f, the carrier of f:] -defined the carrier of f -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of f, the carrier of f:], the carrier of f:]
[: the carrier of f, the carrier of f:] is non empty set
[:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
bool [:[: the carrier of f, the carrier of f:], the carrier of f:] is non empty set
comp f is Relation-like the carrier of f -defined the carrier of f -valued Function-like non empty total quasi_total Element of bool [: the carrier of f, the carrier of f:]
bool [: the carrier of f, the carrier of f:] is non empty set
0. f is V50(f) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
the ZeroF of f is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of f
f is Element of the carrier' of (UN)
dom f is Element of the carrier of (UN)
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . f is Element of the carrier of (UN)
ia is ()
(ia) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
cod f is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . f is Element of the carrier of (UN)
(ia) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier' of (UN) is non empty set
C is Element of the carrier' of (UN)
aa is Element of the carrier' of (UN)
[C,aa] is V27() set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
proj1 the Comp of (UN) is Relation-like set
dom C is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . C is Element of the carrier of (UN)
cod aa is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . aa is Element of the carrier of (UN)
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like reflexive CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
a is Element of the carrier of (UN)
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
((UN),aa) is () () (((UN)))
(aa) is () () (aa,aa)
id aa is Relation-like the carrier of aa -defined the carrier of aa -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of aa, the carrier of aa:]
the carrier of aa is non empty set
[: the carrier of aa, the carrier of aa:] is non empty set
bool [: the carrier of aa, the carrier of aa:] is non empty set
id the carrier of aa is Relation-like the carrier of aa -defined the carrier of aa -valued non empty total quasi_total Element of bool [: the carrier of aa, the carrier of aa:]
(aa,aa,(id aa)) is () ()
C is Morphism of a,a
ii is Element of the carrier of (UN)
Hom (a,ii) is Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = a & cod b₁ = ii ) } is set
Hom (ii,a) is Element of bool the carrier' of (UN)
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = ii & cod b₁ = a ) } is set
ia is Morphism of a,ii
ia (*) C is Element of the carrier' of (UN)
ii is () (((UN)))
c₉ is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
gf is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the carrier of c₉ is non empty set
the carrier of gf is non empty set
[: the carrier of c₉, the carrier of gf:] is non empty set
bool [: the carrier of c₉, the carrier of gf:] is non empty set
hg is Relation-like the carrier of c₉ -defined the carrier of gf -valued Function-like non empty total quasi_total Element of bool [: the carrier of c₉, the carrier of gf:]
(c₉,gf,hg) is () ()
ii is () (((UN)))
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
Hom (a,a) is non empty Element of bool the carrier' of (UN)
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = a & cod b₁ = a ) } is set
dom ia is Element of the carrier of (UN)
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . ia is Element of the carrier of (UN)
cod C is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . C is Element of the carrier of (UN)
[: the carrier of aa, the carrier of gf:] is non empty set
bool [: the carrier of aa, the carrier of gf:] is non empty set
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is Relation-like the carrier of the of ii -defined the carrier of the of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of ii, the carrier of the of ii:]
the carrier of the of ii is non empty set
the carrier of the of ii is non empty set
[: the carrier of the of ii, the carrier of the of ii:] is non empty set
bool [: the carrier of the of ii, the carrier of the of ii:] is non empty set
( the of ii, the of ii, the of ii) is () ()
f is Relation-like the carrier of aa -defined the carrier of gf -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of gf:]
(aa,gf,f) is () ()
[ii,ii] is V27() set
proj1 ((UN)) is Relation-like set
[ia,C] is V27() set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
proj1 the Comp of (UN) is Relation-like set
the Comp of (UN) . (ia,C) is set
the Comp of (UN) . [ia,C] is set
((UN)) . (ia,C) is set
((UN)) . [ia,C] is set
(ii,ii) is () () ()
f * (id aa) is Relation-like the carrier of aa -defined the carrier of gf -valued Function-like non empty total quasi_total Element of bool [: the carrier of aa, the carrier of gf:]
(aa,gf,(f * (id aa))) is () ()
ia is Morphism of ii,a
C (*) ia is Element of the carrier' of (UN)
ii is () (((UN)))
c₉ is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
gf is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the carrier of c₉ is non empty set
the carrier of gf is non empty set
[: the carrier of c₉, the carrier of gf:] is non empty set
bool [: the carrier of c₉, the carrier of gf:] is non empty set
hg is Relation-like the carrier of c₉ -defined the carrier of gf -valued Function-like non empty total quasi_total Element of bool [: the carrier of c₉, the carrier of gf:]
(c₉,gf,hg) is () ()
ii is () (((UN)))
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
Hom (a,a) is non empty Element of bool the carrier' of (UN)
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = a & cod b₁ = a ) } is set
cod ia is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Target of (UN) . ia is Element of the carrier of (UN)
dom C is Element of the carrier of (UN)
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Source of (UN) . C is Element of the carrier of (UN)
[: the carrier of c₉, the carrier of aa:] is non empty set
bool [: the carrier of c₉, the carrier of aa:] is non empty set
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is Relation-like the carrier of the of ii -defined the carrier of the of ii -valued Function-like non empty total quasi_total Element of bool [: the carrier of the of ii, the carrier of the of ii:]
the carrier of the of ii is non empty set
the carrier of the of ii is non empty set
[: the carrier of the of ii, the carrier of the of ii:] is non empty set
bool [: the carrier of the of ii, the carrier of the of ii:] is non empty set
( the of ii, the of ii, the of ii) is () ()
f is Relation-like the carrier of c₉ -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of c₉, the carrier of aa:]
(c₉,aa,f) is () ()
[ii,ii] is V27() set
proj1 ((UN)) is Relation-like set
[C,ia] is V27() set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
proj1 the Comp of (UN) is Relation-like set
the Comp of (UN) . (C,ia) is set
the Comp of (UN) . [C,ia] is set
((UN)) . (C,ia) is set
((UN)) . [C,ia] is set
(ii,ii) is () () ()
(id aa) * f is Relation-like the carrier of c₉ -defined the carrier of aa -valued Function-like non empty total quasi_total Element of bool [: the carrier of c₉, the carrier of aa:]
(c₉,aa,((id aa) * f)) is () ()
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like reflexive CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier' of (UN) is non empty set
ii is Element of the carrier' of (UN)
dom ii is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . ii is Element of the carrier of (UN)
C is Element of the carrier' of (UN)
cod C is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . C is Element of the carrier of (UN)
ii (*) C is Element of the carrier' of (UN)
dom (ii (*) C) is Element of the carrier of (UN)
the Source of (UN) . (ii (*) C) is Element of the carrier of (UN)
dom C is Element of the carrier of (UN)
the Source of (UN) . C is Element of the carrier of (UN)
cod (ii (*) C) is Element of the carrier of (UN)
the Target of (UN) . (ii (*) C) is Element of the carrier of (UN)
cod ii is Element of the carrier of (UN)
the Target of (UN) . ii is Element of the carrier of (UN)
ia is () () (((UN)))
((UN),ia) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is () () (((UN)))
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(ia,ii) is () () ()
ii is () (((UN)))
((ia,ii)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (ia,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((ia,ii)) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of (ia,ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ia) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the carrier' of (UN) is non empty set
ia is Element of the carrier' of (UN)
dom ia is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . ia is Element of the carrier of (UN)
ii is Element of the carrier' of (UN)
cod ii is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . ii is Element of the carrier of (UN)
dom ii is Element of the carrier of (UN)
the Source of (UN) . ii is Element of the carrier of (UN)
C is Element of the carrier' of (UN)
cod C is Element of the carrier of (UN)
the Target of (UN) . C is Element of the carrier of (UN)
ii (*) C is Element of the carrier' of (UN)
ia (*) (ii (*) C) is Element of the carrier' of (UN)
ia (*) ii is Element of the carrier' of (UN)
(ia (*) ii) (*) C is Element of the carrier' of (UN)
c₉ is () () (((UN)))
ii is () () (((UN)))
(c₉,ii) is () () ()
dom (ia (*) ii) is Element of the carrier of (UN)
the Source of (UN) . (ia (*) ii) is Element of the carrier of (UN)
((UN),c₉) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of c₉ is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is () () (((UN)))
((UN),ii) is non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
(ii,ii) is () () ()
cod (ii (*) C) is Element of the carrier of (UN)
the Target of (UN) . (ii (*) C) is Element of the carrier of (UN)
gf is () (((UN)))
(c₉,gf) is () () ()
hg is () (((UN)))
(hg,ii) is () () ()
the carrier of (UN) is non empty set
C is Element of the carrier of (UN)
the carrier' of (UN) is non empty set
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
((UN),ii) is () () (((UN)))
(ii) is () () (ii,ii)
id ii is Relation-like the carrier of ii -defined the carrier of ii -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of ii, the carrier of ii:]
the carrier of ii is non empty set
[: the carrier of ii, the carrier of ii:] is non empty set
bool [: the carrier of ii, the carrier of ii:] is non empty set
id the carrier of ii is Relation-like the carrier of ii -defined the carrier of ii -valued non empty total quasi_total Element of bool [: the carrier of ii, the carrier of ii:]
(ii,ii,(id ii)) is () ()
ia is Element of the carrier' of (UN)
dom ia is Element of the carrier of (UN)
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . ia is Element of the carrier of (UN)
ii is ()
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
cod ia is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . ia is Element of the carrier of (UN)
(ii) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is Morphism of C,C
c₉ is Element of the carrier of (UN)
hg is Element of the carrier of (UN)
Hom (C,c₉) is Element of bool the carrier' of (UN)
bool the carrier' of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = C & cod b₁ = c₉ ) } is set
gf is Morphism of C,c₉
gf (*) ii is Element of the carrier' of (UN)
Hom (hg,C) is Element of bool the carrier' of (UN)
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = hg & cod b₁ = C ) } is set
f is Morphism of hg,C
ii (*) f is Element of the carrier' of (UN)
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
bool the carrier of (UN) is non empty set
aa is set
C is Element of the carrier of (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
UN is non empty V15() V22() V23() universal set
(UN) is Element of bool the carrier of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
UN is non empty V15() V22() V23() universal set
(UN) is Element of bool the carrier of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr st b₁ = b₂ } is set
bool the carrier of (UN) is non empty set
aa is set
C is Element of the carrier of (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr
UN is non empty V15() V22() V23() universal set
(UN) is Element of bool the carrier of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr st b₁ = b₂ } is set
ia is set
ii is non empty set
ii is Element of the carrier of (UN)
ii is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
UN is non empty V15() V22() V23() universal set
(UN) is non empty Element of bool the carrier of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
(UN) is non empty Element of bool the carrier of (UN)
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr st b₁ = b₂ } is set
((UN),(UN)) is non empty non void V55() strict Category-like transitive associative reflexive with_identities Subcategory of (UN)
((UN),(UN)) is non empty Element of bool the carrier' of (UN)
the carrier' of (UN) is non empty set
bool the carrier' of (UN) is non empty set
{ (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
union { (Hom (b₁,b₂)) where b₁, b₂ is Element of the carrier of (UN) : ( b₁ in (UN) & b₂ in (UN) ) } is set
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
[:((UN),(UN)),(UN):] is non empty set
bool [:((UN),(UN)),(UN):] is non empty set
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like ((UN),(UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN),(UN)),(UN):]
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) | ((UN),(UN)) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like Element of bool [: the carrier' of (UN), the carrier of (UN):]
((UN),(UN)) is Relation-like [:((UN),(UN)),((UN),(UN)):] -defined ((UN),(UN)) -valued Function-like Element of bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):]
[:((UN),(UN)),((UN),(UN)):] is Relation-like the carrier' of (UN) -defined the carrier' of (UN) -valued non empty Element of bool [: the carrier' of (UN), the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier' of (UN):] is non empty set
[:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
bool [:[:((UN),(UN)),((UN),(UN)):],((UN),(UN)):] is non empty set
the Comp of (UN) is Relation-like [: the carrier' of (UN), the carrier' of (UN):] -defined the carrier' of (UN) -valued Function-like Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is non empty set
the Comp of (UN) || ((UN),(UN)) is Relation-like Function-like set
CatStr(# (UN),((UN),(UN)),((UN),(UN)),((UN),(UN)),((UN),(UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
bool the carrier of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier of (UN) : ex b₂ being non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Fanoian Abelian add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like midpoint_operator addLoopStr st b₁ = b₂ } is set
UN is non empty 1-sorted
the carrier of UN is non empty set
a is non empty 1-sorted
the carrier of a is non empty set
[: the carrier of UN, the carrier of a:] is non empty set
bool [: the carrier of UN, the carrier of a:] is non empty set
id a is Relation-like the carrier of a -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of a:]
[: the carrier of a, the carrier of a:] is non empty set
bool [: the carrier of a, the carrier of a:] is non empty set
id the carrier of a is Relation-like the carrier of a -defined the carrier of a -valued non empty total quasi_total Element of bool [: the carrier of a, the carrier of a:]
id UN is Relation-like the carrier of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
[: the carrier of UN, the carrier of UN:] is non empty set
bool [: the carrier of UN, the carrier of UN:] is non empty set
id the carrier of UN is Relation-like the carrier of UN -defined the carrier of UN -valued non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
aa is Relation-like the carrier of UN -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of a:]
aa " is Relation-like the carrier of a -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of UN:]
[: the carrier of a, the carrier of UN:] is non empty set
bool [: the carrier of a, the carrier of UN:] is non empty set
aa * (aa ") is Relation-like the carrier of a -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of a:]
(aa ") * aa is Relation-like the carrier of UN -defined the carrier of UN -valued Function-like non empty total quasi_total Element of bool [: the carrier of UN, the carrier of UN:]
[#] a is non empty non proper Element of bool the carrier of a
bool the carrier of a is non empty set
proj2 aa is set
proj1 aa is set
proj2 (aa ") is set
[#] UN is non empty non proper Element of bool the carrier of UN
bool the carrier of UN is non empty set
UN is non empty V15() V22() V23() universal set
(UN) is non empty non void V55() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is non empty set
bool [:((UN)),(UN):] is non empty set
((UN)) is Relation-like ((UN)) -defined (UN) -valued Function-like non empty total quasi_total Element of bool [:((UN)),(UN):]
((UN)) is Relation-like [:((UN)),((UN)):] -defined ((UN)) -valued Function-like Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is non empty set
[:[:((UN)),((UN)):],((UN)):] is non empty set
bool [:[:((UN)),((UN)):],((UN)):] is non empty set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is non empty non void V55() strict CatStr
the carrier of (UN) is non empty set
a is Element of the carrier of (UN)
id a is Morphism of a,a
aa is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like ((UN))
((UN),aa) is () () (((UN)))
(aa) is () () (aa,aa)
id aa is Relation-like the carrier of aa -defined the carrier of aa -valued Function-like non empty total quasi_total additive Element of bool [: the carrier of aa, the carrier of aa:]
the carrier of aa is non empty set
[: the carrier of aa, the carrier of aa:] is non empty set
bool [: the carrier of aa, the carrier of aa:] is non empty set
id the carrier of aa is Relation-like the carrier of aa -defined the carrier of aa -valued non empty total quasi_total Element of bool [: the carrier of aa, the carrier of aa:]
(aa,aa,(id aa)) is () ()
the carrier' of (UN) is non empty set
ii is Element of the carrier' of (UN)
dom ii is Element of the carrier of (UN)
the Source of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is non empty set
bool [: the carrier' of (UN), the carrier of (UN):] is non empty set
the Source of (UN) . ii is Element of the carrier of (UN)
ia is ()
(ia) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
cod ii is Element of the carrier of (UN)
the Target of (UN) is Relation-like the carrier' of (UN) -defined the carrier of (UN) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Target of (UN) . ii is Element of the carrier of (UN)
(ia) is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
the of ia is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr
ii is Morphism of a,a
ii is Element of the carrier of (UN)
gf is Element of the carrier of (UN)
Hom (a,ii) is Element of bool the carrier' of (UN)
bool the carrier' of (UN) is non empty set
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = a & cod b₁ = ii ) } is set
c₉ is Morphism of a,ii
c₉ (*) ii is Element of the carrier' of (UN)
Hom (gf,a) is Element of bool the carrier' of (UN)
{ b₁ where b₁ is Element of the carrier' of (UN) : ( dom b₁ = gf & cod b₁ = a ) } is set
hg is Morphism of gf,a
ii (*) hg is Element of the carrier' of (UN)