:: RINGCAT1 semantic presentation

K132() is Element of bool K128()
K128() is set
bool K128() is set
K47() is set
bool K47() is set
bool K132() is set

1 is non empty set
{{},1} is non empty set
K133() is empty Element of K132()
2 is non empty set
K319(K133(),1,2) is set
[:K319(K133(),1,2),K319(K133(),1,2):] is set
[:[:K319(K133(),1,2),K319(K133(),1,2):],K319(K133(),1,2):] is set
bool [:[:K319(K133(),1,2),K319(K133(),1,2):],K319(K133(),1,2):] is set
bool [:K319(K133(),1,2),K319(K133(),1,2):] is set

the carrier of Z_3 is non empty set
the addF of Z_3 is V1() V4([: the carrier of Z_3, the carrier of Z_3:]) V5( the carrier of Z_3) V6() total V28([: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3) Element of bool [:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:]
[: the carrier of Z_3, the carrier of Z_3:] is set
[:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:] is set
bool [:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:] is set
comp Z_3 is V1() V4( the carrier of Z_3) V5( the carrier of Z_3) V6() non empty total V28( the carrier of Z_3, the carrier of Z_3) Element of bool [: the carrier of Z_3, the carrier of Z_3:]
bool [: the carrier of Z_3, the carrier of Z_3:] is set
0. Z_3 is V48( Z_3 ) Element of the carrier of Z_3
the ZeroF of Z_3 is Element of the carrier of Z_3
the multF of Z_3 is V1() V4([: the carrier of Z_3, the carrier of Z_3:]) V5( the carrier of Z_3) V6() total V28([: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3) Element of bool [:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:]
1. Z_3 is Element of the carrier of Z_3
the OneF of Z_3 is Element of the carrier of Z_3
UN is non empty doubleLoopStr
the carrier of UN is non empty set
a is non empty doubleLoopStr
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 set
UN is non empty doubleLoopStr
the carrier of UN is non empty set
a is non empty doubleLoopStr
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 set
aa is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
aa is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
UN is non empty doubleLoopStr
the carrier of UN is non empty set
a is non empty doubleLoopStr
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 set
aa is non empty doubleLoopStr
the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is set
bool [: the carrier of a, the carrier of aa:] is set
C is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
ii is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]
ii * C is V1() V4( the carrier of UN) V5( the carrier of aa) V6() non empty total V28( the carrier of UN, the carrier of aa) Element of bool [: the carrier of UN, the carrier of aa:]
[: the carrier of UN, the carrier of aa:] is set
bool [: the carrier of UN, the carrier of aa:] is set
ii is Element of the carrier of UN
c8 is Element of the carrier of UN
ii + c8 is Element of the carrier of UN
(ii * C) . (ii + c8) is Element of the carrier of aa
(ii * C) . ii is Element of the carrier of aa
(ii * C) . c8 is Element of the carrier of aa
((ii * C) . ii) + ((ii * C) . c8) is Element of the carrier of aa
C . ii is Element of the carrier of a
ii . (C . ii) is Element of the carrier of aa
C . c8 is Element of the carrier of a
ii . (C . c8) is Element of the carrier of aa
C . (ii + c8) is Element of the carrier of a
ii . (C . (ii + c8)) is Element of the carrier of aa
(C . ii) + (C . c8) is Element of the carrier of a
ii . ((C . ii) + (C . c8)) is Element of the carrier of aa
ii is Element of the carrier of UN
c8 is Element of the carrier of UN
ii * c8 is Element of the carrier of UN
(ii * C) . (ii * c8) is Element of the carrier of aa
(ii * C) . ii is Element of the carrier of aa
(ii * C) . c8 is Element of the carrier of aa
((ii * C) . ii) * ((ii * C) . c8) is Element of the carrier of aa
C . ii is Element of the carrier of a
ii . (C . ii) is Element of the carrier of aa
C . c8 is Element of the carrier of a
ii . (C . c8) is Element of the carrier of aa
C . (ii * c8) is Element of the carrier of a
ii . (C . (ii * c8)) is Element of the carrier of aa
(C . ii) * (C . c8) is Element of the carrier of a
ii . ((C . ii) * (C . c8)) is Element of the carrier of aa
1_ UN is Element of the carrier of UN
(ii * C) . (1_ UN) is Element of the carrier of aa
C . (1_ UN) is Element of the carrier of a
ii . (C . (1_ UN)) is Element of the carrier of aa
1_ a is Element of the carrier of a
ii . (1_ a) is Element of the carrier of aa
1_ aa is Element of the carrier of aa
UN is ()

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) 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 set
bool [: the carrier of the of UN, the carrier of the of UN:] is set
UN is non empty doubleLoopStr
id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) 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 set
bool [: the carrier of UN, the carrier of UN:] is set
id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) 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
(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
1_ UN is Element of the carrier of UN
(id UN) . (1_ UN) is Element of the carrier of UN
UN is non empty doubleLoopStr
id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) 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 set
bool [: the carrier of UN, the carrier of UN:] is set
id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]

[::] is set
bool [::] is set
id the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr is V1() V4( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) V5( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) non empty total V28( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) Element of bool [::]
( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()) is () ()

the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()) is non empty set

the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()) is non empty set
(( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,())) is V1() V4( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,())) V5( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,())) V6() non empty total V28( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,())) Element of bool [: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()):]
[: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()):] is set
bool [: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()):] is set
the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()) is V1() V4( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,())) V5( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,())) V6() non empty total V28( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,())) Element of bool [: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,()):]

id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) 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 set
bool [: the carrier of UN, the carrier of UN:] is set
id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]
(UN,UN,(id UN)) is () ()
the of (UN,UN,(id UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of the of (UN,UN,(id UN)) is non empty set
the of (UN,UN,(id UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of the of (UN,UN,(id UN)) is non empty set
((UN,UN,(id UN))) is V1() V4( the carrier of the of (UN,UN,(id UN))) V5( the carrier of the of (UN,UN,(id UN))) V6() non empty total V28( the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN))) 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)), the carrier of the of (UN,UN,(id UN)):] is set
bool [: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):] is set
the of (UN,UN,(id UN)) is V1() V4( the carrier of the of (UN,UN,(id UN))) V5( the carrier of the of (UN,UN,(id UN))) V6() non empty total V28( the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN))) Element of bool [: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):]

(UN) is () ()
id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) 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 set
bool [: the carrier of UN, the carrier of UN:] is set
id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]
(UN,UN,(id UN)) is () ()

(aa) is () () ()
id aa is V1() V4( the carrier of aa) V5( the carrier of aa) V6() non empty total V28( the carrier of aa, the carrier of aa) unity-preserving multiplicative additive (aa,aa) 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 set
bool [: the carrier of aa, the carrier of aa:] is set
id the carrier of aa is V1() V4( the carrier of aa) V5( the carrier of aa) non empty total V28( the carrier of aa, the carrier of aa) Element of bool [: the carrier of aa, the carrier of aa:]
(aa,aa,(id aa)) is () ()

UN is () ()

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) 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 set
bool [: the carrier of the of UN, the carrier of the of UN:] is set
( the of UN, the of UN, the of UN) is () ()
(UN) is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]
the of ( the of UN, the of UN, the of UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of the of ( the of UN, the of UN, the of UN) is non empty set
the of ( the of UN, the of UN, the of UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of the of ( the of UN, the of UN, the of UN) is non empty set
(( the of UN, the of UN, the of UN)) is V1() V4( the carrier of the of ( the of UN, the of UN, the of UN)) V5( the carrier of the of ( the of UN, the of UN, the of UN)) V6() non empty total V28( the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN)) Element of bool [: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):]
[: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):] is set
bool [: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):] is set
the of ( the of UN, the of UN, the of UN) is V1() V4( the carrier of the of ( the of UN, the of UN, the of UN)) V5( the carrier of the of ( the of UN, the of UN, the of UN)) V6() non empty total V28( the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN)) Element of bool [: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):]
aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)
C is Element of the carrier of the of ( the of UN, the of UN, the of UN)
aa + C is Element of the carrier of the of ( the of UN, the of UN, the of UN)
(( the of UN, the of UN, the of UN)) . (aa + C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)
(( the of UN, the of UN, the of UN)) . aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)
(( the of UN, the of UN, the of UN)) . C is Element of the carrier of the of ( the of UN, the of UN, the of UN)
((( the of UN, the of UN, the of UN)) . aa) + ((( the of UN, the of UN, the of UN)) . C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)
aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)
C is Element of the carrier of the of ( the of UN, the of UN, the of UN)
aa * C is Element of the carrier of the of ( the of UN, the of UN, the of UN)
(( the of UN, the of UN, the of UN)) . (aa * C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)
(( the of UN, the of UN, the of UN)) . aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)
(( the of UN, the of UN, the of UN)) . C is Element of the carrier of the of ( the of UN, the of UN, the of UN)
((( the of UN, the of UN, the of UN)) . aa) * ((( the of UN, the of UN, the of UN)) . C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)

aa is () ()

the of aa is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) 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 set
bool [: the carrier of the of aa, the carrier of the of aa:] is set
( the of aa, the of aa, the of aa) is () ()
(( the of aa, the of aa, the of aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ( the of aa, the of aa, the of aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(( the of aa, the of aa, the of aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ( the of aa, the of aa, the of aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the () () (UN,a) is () () (UN,a)

(UN) is () () ()
id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) 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 set
bool [: the carrier of UN, the carrier of UN:] is set
id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]
(UN,UN,(id UN)) is () ()

UN is () ()

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) 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 set
bool [: the carrier of the of UN, the carrier of the of UN:] is set
(UN) is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

aa is () ()

(aa) is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) 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 set
bool [: the carrier of the of aa, the carrier of the of aa:] is set
the of aa is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) Element of bool [: the carrier of the of aa, the carrier of the of aa:]
C is () ()

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 set
bool [: the carrier of UN, the carrier of a:] is set
aa is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,aa) is () ()

the carrier of the of (UN,a,aa) is non empty set

the carrier of the of (UN,a,aa) is non empty set
((UN,a,aa)) is V1() V4( the carrier of the of (UN,a,aa)) V5( the carrier of the of (UN,a,aa)) V6() non empty total V28( the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa)) 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), the carrier of the of (UN,a,aa):] is set
bool [: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):] is set
the of (UN,a,aa) is V1() V4( the carrier of the of (UN,a,aa)) V5( the carrier of the of (UN,a,aa)) V6() non empty total V28( the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa)) Element of bool [: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):]

UN is () ()

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) 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 set
bool [: the carrier of the of UN, the carrier of the of UN:] is set
( the of UN, the of UN, the of UN) is () ()
a is () ()

UN is () ()

a is () ()

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) 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 set
bool [: the carrier of the of UN, the carrier of the of UN:] is set
( the of UN, the of UN, the of UN) is () ()

the of a is V1() V4( the carrier of the of a) V5( the carrier of the of a) V6() non empty total V28( the carrier of the of a, the carrier of the of a) 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 set
bool [: the carrier of the of a, the carrier of the of a:] is set
( the of a, the of a, the of a) is () ()

UN is () () ()

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 set
bool [: the carrier of UN, the carrier of a:] is set
aa is () () (UN,a)

the of aa is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) 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 set
bool [: the carrier of the of aa, the carrier of the of aa:] is set
C is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,C) is () ()

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 set
bool [: the carrier of UN, the carrier of a:] is set
aa is () () (UN,a)
C is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,C) is () ()
UN 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 set
bool [: the carrier of a, the carrier of aa:] is set
C is () () (a,aa)
ii is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,ii) is () ()
UN is () ()

a is () ()

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) 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 set
bool [: the carrier of the of UN, the carrier of the of UN:] is set
( the of UN, the of UN, the of UN) is () ()

the of a is V1() V4( the carrier of the of a) V5( the carrier of the of a) V6() non empty total V28( the carrier of the of a, the carrier of the of a) 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 set
bool [: the carrier of the of a, the carrier of the of a:] is set
( the of a, the of a, the of a) is () ()

the carrier of C is non empty set
the carrier of ii is non empty set
[: the carrier of C, the carrier of ii:] is set
bool [: the carrier of C, the carrier of ii:] is set
ia is V1() V4( the carrier of C) V5( the carrier of ii) V6() non empty total V28( the carrier of C, the carrier of ii) Element of bool [: the carrier of C, the carrier of ii:]
(C,ii,ia) is () ()
the carrier of aa is non empty set
[: the carrier of aa, the carrier of C:] is set
bool [: the carrier of aa, the carrier of C:] is set
ii is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,ii) is () ()
ia * ii is V1() V4( the carrier of aa) V5( the carrier of ii) V6() non empty total V28( the carrier of aa, the carrier of ii) Element of bool [: the carrier of aa, the carrier of ii:]
[: the carrier of aa, the carrier of ii:] is set
bool [: the carrier of aa, the carrier of ii:] is set
(aa,ii,(ia * ii)) is () ()
c8 is () () ()

the carrier of H1 is non empty set

the carrier of f is non empty set
[: the carrier of H1, the carrier of f:] is set
bool [: the carrier of H1, the carrier of f:] is set

the carrier of G1 is non empty set
[: the carrier of G1, the carrier of H1:] is set
bool [: the carrier of G1, the carrier of H1:] is set
f is V1() V4( the carrier of H1) V5( the carrier of f) V6() non empty total V28( the carrier of H1, the carrier of f) Element of bool [: the carrier of H1, the carrier of f:]
(H1,f,f) is () ()
G is V1() V4( the carrier of G1) V5( the carrier of H1) V6() non empty total V28( the carrier of G1, the carrier of H1) Element of bool [: the carrier of G1, the carrier of H1:]
(G1,H1,G) is () ()
f * G is V1() V4( the carrier of G1) V5( the carrier of f) V6() non empty total V28( the carrier of G1, the carrier of f) Element of bool [: the carrier of G1, the carrier of f:]
[: the carrier of G1, the carrier of f:] is set
bool [: the carrier of G1, the carrier of f:] is set
(G1,f,(f * G)) is () ()

ia is () () ()
ii is () () ()

ii is () () (aa,C)
the carrier of aa is non empty set
the carrier of c8 is non empty set
[: the carrier of aa, the carrier of c8:] is set
bool [: the carrier of aa, the carrier of c8:] is set
H1 is () () (aa,c8)
f is V1() V4( the carrier of aa) V5( the carrier of c8) V6() non empty total V28( the carrier of aa, the carrier of c8) Element of bool [: the carrier of aa, the carrier of c8:]
(aa,c8,f) is () ()
the carrier of G1 is non empty set
[: the carrier of c8, the carrier of G1:] is set
bool [: the carrier of c8, the carrier of G1:] is set
f is () () (c8,G1)
G is V1() V4( the carrier of c8) V5( the carrier of G1) V6() non empty total V28( the carrier of c8, the carrier of G1) Element of bool [: the carrier of c8, the carrier of G1:]
(c8,G1,G) is () ()
G * f is V1() V4( the carrier of aa) V5( the carrier of G1) V6() non empty total V28( the carrier of aa, the carrier of G1) Element of bool [: the carrier of aa, the carrier of G1:]
[: the carrier of aa, the carrier of G1:] is set
bool [: the carrier of aa, the carrier of G1:] is set
(aa,G1,(G * f)) is () ()

C is () ()

the of C is V1() V4( the carrier of the of C) V5( the carrier of the of C) V6() non empty total V28( the carrier of the of C, the carrier of the of C) 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 set
bool [: the carrier of the of C, the carrier of the of C:] is set
( the of C, the of C, the of C) is () ()
ii is () ()

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 set
bool [: the carrier of UN, the carrier of a:] is set
ia is () () (UN,a)
ii is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,ii) is () ()
c8 is () ()

the of c8 is V1() V4( the carrier of the of c8) V5( the carrier of the of c8) V6() non empty total V28( the carrier of the of c8, the carrier of the of c8) Element of bool [: the carrier of the of c8, the carrier of the of c8:]
the carrier of the of c8 is non empty set
the carrier of the of c8 is non empty set
[: the carrier of the of c8, the carrier of the of c8:] is set
bool [: the carrier of the of c8, the carrier of the of c8:] is set
( the of c8, the of c8, the of c8) is () ()
G1 is () ()

the carrier of aa is non empty set
[: the carrier of a, the carrier of aa:] is set
bool [: the carrier of a, the carrier of aa:] is set
H1 is () () (a,aa)
f is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,f) is () ()
(G1,ii) is () () ()
f * ii is V1() V4( the carrier of UN) V5( the carrier of aa) V6() non empty total V28( the carrier of UN, the carrier of aa) Element of bool [: the carrier of UN, the carrier of aa:]
[: the carrier of UN, the carrier of aa:] is set
bool [: the carrier of UN, the carrier of aa:] is set
(UN,aa,(f * ii)) is () ()

C is () () (UN,a)
ii is () () (aa,UN)
(C,ii) is () () ()
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 set
bool [: the carrier of UN, the carrier of a:] is set
ia is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,ia) is () ()
the carrier of aa is non empty set
[: the carrier of aa, the carrier of UN:] is set
bool [: the carrier of aa, the carrier of UN:] is set
ii is V1() V4( the carrier of aa) V5( the carrier of UN) V6() non empty total V28( the carrier of aa, the carrier of UN) Element of bool [: the carrier of aa, the carrier of UN:]
(aa,UN,ii) is () ()

ia * ii is V1() V4( the carrier of aa) V5( the carrier of a) V6() non empty total V28( the carrier of aa, the carrier of a) Element of bool [: the carrier of aa, the carrier of a:]
[: the carrier of aa, the carrier of a:] is set
bool [: the carrier of aa, the carrier of a:] is set
(aa,a,(ia * ii)) is () ()

C is () () (a,aa)
ii is () () (UN,a)
(C,ii) is () () ()
a is () () ()

UN is () () ()

(a,UN) is () () ()

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 set
bool [: the carrier of (UN), the carrier of (a):] is set
ia is () () ((UN),(a))
ii is V1() V4( the carrier of (UN)) V5( the carrier of (a)) V6() non empty total V28( the carrier of (UN), the carrier of (a)) Element of bool [: the carrier of (UN), the carrier of (a):]
((UN),(a),ii) is () ()
the carrier of (UN) is non empty set
[: the carrier of (UN), the carrier of (UN):] is set
bool [: the carrier of (UN), the carrier of (UN):] is set
c8 is () () ((UN),(UN))
G1 is V1() V4( the carrier of (UN)) V5( the carrier of (UN)) V6() non empty total V28( the carrier of (UN), the carrier of (UN)) Element of bool [: the carrier of (UN), the carrier of (UN):]
((UN),(UN),G1) is () ()
ii * G1 is V1() V4( the carrier of (UN)) V5( the carrier of (a)) V6() non empty total V28( the carrier of (UN), the carrier of (a)) Element of bool [: the carrier of (UN), the carrier of (a):]
[: the carrier of (UN), the carrier of (a):] is set
bool [: the carrier of (UN), the carrier of (a):] is set
((UN),(a),(ii * G1)) is () ()
a is () () ()

UN is () () ()

(a,UN) is () () ()

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 set
bool [: the carrier of aa, the carrier of C:] is set

the carrier of ii is non empty set
[: the carrier of C, the carrier of ii:] is set
bool [: the carrier of C, the carrier of ii:] is set
ia is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,ia) is () ()
ii is V1() V4( the carrier of C) V5( the carrier of ii) V6() non empty total V28( the carrier of C, the carrier of ii) Element of bool [: the carrier of C, the carrier of ii:]
(C,ii,ii) is () ()
ii * ia is V1() V4( the carrier of aa) V5( the carrier of ii) V6() non empty total V28( the carrier of aa, the carrier of ii) Element of bool [: the carrier of aa, the carrier of ii:]
[: the carrier of aa, the carrier of ii:] is set
bool [: the carrier of aa, the carrier of ii:] is set
(aa,ii,(ii * ia)) is () ()

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 set
bool [: the carrier of aa, the carrier of C:] is set

the carrier of ii is non empty set
[: the carrier of C, the carrier of ii:] is set
bool [: the carrier of C, the carrier of ii:] is set
ia is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,ia) is () ()
ii is V1() V4( the carrier of C) V5( the carrier of ii) V6() non empty total V28( the carrier of C, the carrier of ii) Element of bool [: the carrier of C, the carrier of ii:]
(C,ii,ii) is () ()
ii * ia is V1() V4( the carrier of aa) V5( the carrier of ii) V6() non empty total V28( the carrier of aa, the carrier of ii) Element of bool [: the carrier of aa, the carrier of ii:]
[: the carrier of aa, the carrier of ii:] is set
bool [: the carrier of aa, the carrier of ii:] is set
(aa,ii,(ii * ia)) is () ()

ii is () () (UN,a)
ia is () () (a,aa)
(ia,ii) is () () ()
ii is () () (aa,C)
(ii,(ia,ii)) is () () ()
(ii,ia) is () () ()
((ii,ia),ii) is () () ()
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 set
bool [: the carrier of UN, the carrier of a:] is set
c8 is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]
(UN,a,c8) is () ()
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 set
bool [: the carrier of aa, the carrier of C:] is set
G1 is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]
(aa,C,G1) is () ()
[: the carrier of a, the carrier of aa:] is set
bool [: the carrier of a, the carrier of aa:] is set
H1 is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]
(a,aa,H1) is () ()

G1 * H1 is V1() V4( the carrier of a) V5( the carrier of C) V6() non empty total V28( the carrier of a, the carrier of C) Element of bool [: the carrier of a, the carrier of C:]
[: the carrier of a, the carrier of C:] is set
bool [: the carrier of a, the carrier of C:] is set
(a,C,(G1 * H1)) is () ()

H1 * c8 is V1() V4( the carrier of UN) V5( the carrier of aa) V6() non empty total V28( the carrier of UN, the carrier of aa) Element of bool [: the carrier of UN, the carrier of aa:]
[: the carrier of UN, the carrier of aa:] is set
bool [: the carrier of UN, the carrier of aa:] is set
(UN,aa,(H1 * c8)) is () ()
G1 * (H1 * c8) is V1() V4( the carrier of UN) V5( the carrier of C) V6() non empty total V28( the carrier of UN, the carrier of C) Element of bool [: the carrier of UN, the carrier of C:]
[: the carrier of UN, the carrier of C:] is set
bool [: the carrier of UN, the carrier of C:] is set
(UN,C,(G1 * (H1 * c8))) is () ()
(G1 * H1) * c8 is V1() V4( the carrier of UN) V5( the carrier of C) V6() non empty total V28( the carrier of UN, the carrier of C) Element of bool [: the carrier of UN, the carrier of C:]
(UN,C,((G1 * H1) * c8)) is () ()
aa is () () ()

a is () () ()

UN is () () ()

(a,UN) is () () ()
(aa,(a,UN)) is () () ()
(aa,a) is () () ()
((aa,a),UN) is () () ()

c8 is () () ((a),(aa))
H1 is () () ((UN),(a))
G1 is () () ((UN),(UN))
(H1,G1) is () () ()
(c8,(H1,G1)) is () () ()
(c8,H1) is () () ()
((c8,H1),G1) is () () ()

(UN) is () () (UN,UN)
id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) 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 set
bool [: the carrier of UN, the carrier of UN:] is set
id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]
(UN,UN,(id UN)) is () ()

aa is () () ()

((UN),aa) is () () ()

the carrier of (aa) is non empty set
[: the carrier of (aa), the carrier of UN:] is set
bool [: the carrier of (aa), the carrier of UN:] is set
ii is () () ((aa),UN)
ia is V1() V4( the carrier of (aa)) V5( the carrier of UN) V6() non empty total V28( the carrier of (aa), the carrier of UN) Element of bool [: the carrier of (aa), the carrier of UN:]
((aa),UN,ia) is () ()
(id UN) * ia is V1() V4( the carrier of (aa)) V5( the carrier of UN) V6() non empty total V28( the carrier of (aa), the carrier of UN) Element of bool [: the carrier of (aa), the carrier of UN:]
aa is () () ()

(aa,(UN)) is () () ()

the of aa is non empty right_complementable V96() V97() V98() unital associative