K132() is Element of bool K128()
K128() is set
bool K128() is set
K47() is set
bool K47() is set
bool K132() is set
{} is empty 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
Z_3 is non empty right_complementable almost_left_invertible strict V96() V97() V98() unital associative commutative right-distributive left-distributive right_unital well-unital V148() left_unital Fanoian doubleLoopStr
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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 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:]
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 right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
id 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 ) V6() 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 ) unity-preserving multiplicative additive ( 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 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 :]
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 non empty set
[: 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 :] is set
bool [: 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 :] 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 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 :]
( 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 the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is () ()
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 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 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 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 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 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 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 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 ,(id 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 ,(id 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 ,(id 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 ,(id 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 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 ,(id 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 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 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 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 ,(id 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 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 ,(id 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 ,(id 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 ,(id 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 ,(id 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 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 ,(id 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 the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )):]
UN is 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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 () ()
((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) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((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) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is () ()
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 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 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)
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is () ()
(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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 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 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
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a 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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
((UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
UN is () ()
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 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 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:]
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is () ()
(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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 () ()
(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 UN is non empty set
a 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 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 of (UN,a,aa) 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,a,aa) is non empty set
the of (UN,a,aa) 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,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,a,aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN,a,aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 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 () ()
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
a is () ()
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 UN is non empty set
a 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 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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 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 () ()
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 UN is non empty set
a 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 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 () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa 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 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 () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
a is () ()
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () ()
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ii 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 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 () () ()
H1 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 H1 is non empty set
f 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 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
G1 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 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 () ()
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ia is () () ()
ii is () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () ()
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
C is () ()
(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () ()
(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ii 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 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 () ()
(c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () ()
(G1) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(G1) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of G1 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 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 () ()
((G1,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (G1,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((G1,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (G1,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () ()
(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (C,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((C,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (C,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
C is () () (a,aa)
ii is () () (UN,a)
(C,ii) is () () ()
a is () () ()
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(a,UN) is () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a 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 (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 () () ()
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(a,UN) is () () ()
((a,UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (a,UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
((a,UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (a,UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa 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 aa is non empty set
C 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 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
ii 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 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 () ()
aa 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 aa is non empty set
C 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 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
ii 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 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 () ()
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () ()
(ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () ()
(ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((ii,ia)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (ii,ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((ia,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (ia,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 () () ()
(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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is () () ()
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(a,UN) is () () ()
(aa,(a,UN)) is () () ()
(aa,a) is () () ()
((aa,a),UN) is () () ()
(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
(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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(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 () ()
((UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
((UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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
aa is () () ()
(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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN),aa) is () () ()
(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 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 (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) 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 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(aa,(UN)) is () () ()
(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 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 (aa) is non empty set
[: the carrier of UN, the carrier of (aa):] is set
bool [: the carrier of UN, the carrier of (aa):] is set
ii is () () (UN,(aa))
ia 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):]
(UN,(aa),ia) is () ()
ia * (id UN) 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 non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
{ the non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr } is non empty set
aa is Element of { the non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr }
UN is non empty () set
a is Element of UN
UN 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 (UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
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 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 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 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 ) V6() 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 ) unity-preserving multiplicative additive ( 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 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 :]
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 non empty set
[: 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 :] is set
bool [: 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 :] 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 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 :]
( 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 the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is () ()
{( 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
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 right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a 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)
{ the () () (UN,a)} is non empty set
C is non empty () set
ii is () (C)
UN is non empty set
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
C is Element of UN
C is set
C is non empty () set
ii is () (C)
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is () () (UN,a)
{aa} is non empty set
C is Element of {aa}
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a 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)
the carrier of UN is non empty set
the carrier of a is non empty set
Maps (UN,a) is non empty MapsSet of UN,a
K87( the carrier of UN, the carrier of a) is V9() non empty set
{ (UN,a,b1) where b1 is V1() V4( the carrier of UN) V5( the carrier of a) V6() total V28( the carrier of UN, the carrier of a) Element of Maps (UN,a) : b1 is (UN,a) } is set
[: the carrier of UN, the carrier of a:] is set
bool [: the carrier of UN, the carrier of a:] is set
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 () ()
ia is V1() V4( the carrier of UN) V5( the carrier of a) V6() total V28( the carrier of UN, the carrier of a) Element of Maps (UN,a)
(UN,a,ia) is () ()
ii is non empty set
c8 is set
G1 is V1() V4( the carrier of UN) V5( the carrier of a) V6() total V28( the carrier of UN, the carrier of a) Element of Maps (UN,a)
(UN,a,G1) is () ()
c8 is Element of ii
c8 is set
G1 is () () (UN,a)
(G1) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(G1) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of G1 is V1() V4( the carrier of the of G1) V5( the carrier of the of G1) V6() non empty total V28( the carrier of the of G1, the carrier of the of G1) Element of bool [: the carrier of the of G1, the carrier of the of G1:]
the carrier of the of G1 is non empty set
the carrier of the of G1 is non empty set
[: the carrier of the of G1, the carrier of the of G1:] is set
bool [: the carrier of the of G1, the carrier of the of G1:] is set
H1 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:]
f is V1() V4( the carrier of UN) V5( the carrier of a) V6() total V28( the carrier of UN, the carrier of a) Element of Maps (UN,a)
(UN,a,f) is () ()
c8 is non empty () (UN,a)
G1 is set
H1 is set
aa is non empty () (UN,a)
C is non empty () (UN,a)
ii is set
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty () (UN,a)
C is Element of aa
UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
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 V25() V26() V27() set
[C,ii,ia] is V25() V26() set
[C,ii] is V25() set
[[C,ii],ia] is V25() set
[[C,ii,ia],ii] is V25() set
c8 is set
G1 is set
[[C,ii,ia,ii],c8,G1] is V25() V26() set
[[C,ii,ia,ii],c8] is V25() set
[[[C,ii,ia,ii],c8],G1] is V25() set
H1 is set
f is set
f is set
G is set
[H1,f,f,G] is V25() V26() V27() set
[H1,f,f] is V25() V26() set
[H1,f] is V25() set
[[H1,f],f] is V25() set
[[H1,f,f],G] is V25() set
ii is set
ia is set
[[H1,f,f,G],ii,ia] is V25() V26() set
[[H1,f,f,G],ii] is V25() set
[[[H1,f,f,G],ii],ia] is V25() set
G2 is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of G2 is non empty set
the addF of G2 is V1() V4([: the carrier of G2, the carrier of G2:]) V5( the carrier of G2) V6() total V28([: the carrier of G2, the carrier of G2:], the carrier of G2) Element of bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:]
[: the carrier of G2, the carrier of G2:] is set
[:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is set
bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is set
comp G2 is V1() V4( the carrier of G2) V5( the carrier of G2) V6() non empty total V28( the carrier of G2, the carrier of G2) Element of bool [: the carrier of G2, the carrier of G2:]
bool [: the carrier of G2, the carrier of G2:] is set
0. G2 is V48(G2) Element of the carrier of G2
the ZeroF of G2 is Element of the carrier of G2
the multF of G2 is V1() V4([: the carrier of G2, the carrier of G2:]) V5( the carrier of G2) V6() total V28([: the carrier of G2, the carrier of G2:], the carrier of G2) Element of bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:]
1. G2 is Element of the carrier of G2
the OneF of G2 is Element of the carrier of G2
G2 is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of G2 is non empty set
the addF of G2 is V1() V4([: the carrier of G2, the carrier of G2:]) V5( the carrier of G2) V6() total V28([: the carrier of G2, the carrier of G2:], the carrier of G2) Element of bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:]
[: the carrier of G2, the carrier of G2:] is set
[:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is set
bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is set
comp G2 is V1() V4( the carrier of G2) V5( the carrier of G2) V6() non empty total V28( the carrier of G2, the carrier of G2) Element of bool [: the carrier of G2, the carrier of G2:]
bool [: the carrier of G2, the carrier of G2:] is set
0. G2 is V48(G2) Element of the carrier of G2
the ZeroF of G2 is Element of the carrier of G2
the multF of G2 is V1() V4([: the carrier of G2, the carrier of G2:]) V5( the carrier of G2) V6() total V28([: the carrier of G2, the carrier of G2:], the carrier of G2) Element of bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:]
1. G2 is Element of the carrier of G2
the OneF of G2 is Element of the carrier of G2
G1 is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of G1 is non empty set
the addF of G1 is V1() V4([: the carrier of G1, the carrier of G1:]) V5( the carrier of G1) V6() total V28([: the carrier of G1, the carrier of G1:], the carrier of G1) Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
[: the carrier of G1, the carrier of G1:] is set
[:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is set
bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is set
comp G1 is V1() V4( the carrier of G1) V5( the carrier of G1) V6() non empty total V28( the carrier of G1, the carrier of G1) Element of bool [: the carrier of G1, the carrier of G1:]
bool [: the carrier of G1, the carrier of G1:] is set
0. G1 is V48(G1) Element of the carrier of G1
the ZeroF of G1 is Element of the carrier of G1
the multF of G1 is V1() V4([: the carrier of G1, the carrier of G1:]) V5( the carrier of G1) V6() total V28([: the carrier of G1, the carrier of G1:], the carrier of G1) Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
1. G1 is Element of the carrier of G1
the OneF of G1 is Element of the carrier of G1
G1 is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of G1 is non empty set
the addF of G1 is V1() V4([: the carrier of G1, the carrier of G1:]) V5( the carrier of G1) V6() total V28([: the carrier of G1, the carrier of G1:], the carrier of G1) Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
[: the carrier of G1, the carrier of G1:] is set
[:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is set
bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:] is set
comp G1 is V1() V4( the carrier of G1) V5( the carrier of G1) V6() non empty total V28( the carrier of G1, the carrier of G1) Element of bool [: the carrier of G1, the carrier of G1:]
bool [: the carrier of G1, the carrier of G1:] is set
0. G1 is V48(G1) Element of the carrier of G1
the ZeroF of G1 is Element of the carrier of G1
the multF of G1 is V1() V4([: the carrier of G1, the carrier of G1:]) V5( the carrier of G1) V6() total V28([: the carrier of G1, the carrier of G1:], the carrier of G1) Element of bool [:[: the carrier of G1, the carrier of G1:], the carrier of G1:]
1. G1 is Element of the carrier of G1
the OneF of G1 is Element of the carrier of G1
UN is non empty universal set
aa is Element of UN
C is Element of UN
ii is Element of UN
ia is Element of UN
[aa,C,ii,ia] is V25() V26() V27() set
[aa,C,ii] is V25() V26() set
[aa,C] is V25() set
[[aa,C],ii] is V25() set
[[aa,C,ii],ia] is V25() set
ii is Element of UN
c8 is Element of UN
[[aa,C,ii,ia],ii,c8] is V25() V26() set
[[aa,C,ii,ia],ii] is V25() set
[[[aa,C,ii,ia],ii],c8] is V25() set
UN is non empty 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
C is set
ii is set
ii is set
UN is non empty universal set
(UN) is set
a is set
UN is non empty universal set
(UN) is set
UN is non empty 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 V25() V26() V27() set
[C,ii,ia] is V25() V26() set
[C,ii] is V25() set
[[C,ii],ia] is V25() set
[[C,ii,ia],ii] is V25() set
c8 is set
G1 is set
[[C,ii,ia,ii],c8,G1] is V25() V26() set
[[C,ii,ia,ii],c8] is V25() set
[[[C,ii,ia,ii],c8],G1] is V25() set
H1 is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of H1 is non empty set
the addF of H1 is V1() V4([: the carrier of H1, the carrier of H1:]) V5( the carrier of H1) V6() total V28([: the carrier of H1, the carrier of H1:], the carrier of H1) Element of bool [:[: the carrier of H1, the carrier of H1:], the carrier of H1:]
[: the carrier of H1, the carrier of H1:] is set
[:[: the carrier of H1, the carrier of H1:], the carrier of H1:] is set
bool [:[: the carrier of H1, the carrier of H1:], the carrier of H1:] is set
comp H1 is V1() V4( the carrier of H1) V5( the carrier of H1) V6() non empty total V28( the carrier of H1, the carrier of H1) Element of bool [: the carrier of H1, the carrier of H1:]
bool [: the carrier of H1, the carrier of H1:] is set
0. H1 is V48(H1) Element of the carrier of H1
the ZeroF of H1 is Element of the carrier of H1
the multF of H1 is V1() V4([: the carrier of H1, the carrier of H1:]) V5( the carrier of H1) V6() total V28([: the carrier of H1, the carrier of H1:], the carrier of H1) Element of bool [:[: the carrier of H1, the carrier of H1:], the carrier of H1:]
1. H1 is Element of the carrier of H1
the OneF of H1 is Element of the carrier of H1
UN is non empty universal set
(UN) is non empty set
a is Element of (UN)
UN 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 (UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)) is non empty () ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN))
{ (b1,b2) where b1, b2 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN) : (b1,b2) } is set
( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)) is () () ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN))
id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN) 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 (UN)) 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 (UN)) V6() 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 (UN), the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)) unity-preserving multiplicative additive ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)) Element of bool [: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN):]
the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN) is non empty set
[: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN):] is set
bool [: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN):] 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 (UN) 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 (UN)) 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 (UN)) 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 (UN), the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)) Element of bool [: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN):]
( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN), the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN),(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN))) is () ()
union { (b1,b2) where b1, b2 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN) : (b1,b2) } is set
ii is non empty set
ia is set
ii is set
c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
(c8,G1) is non empty () (c8,G1)
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
(ii,c8) is non empty () (ii,c8)
ia is set
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ia is non empty () set
ii is set
G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
H1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
c8 is set
a is non empty () set
aa is non empty () set
C is set
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
UN is non empty () set
(UN) is non empty () set
a is () ((UN))
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ii is () () (aa,C)
(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ii is () () (aa,C)
(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is non empty () set
a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
(a) is () () (a,a)
id a is V1() V4( the carrier of a) V5( the carrier of a) V6() non empty total V28( the carrier of a, the carrier of a) unity-preserving multiplicative additive (a,a) 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 set
bool [: the carrier of a, the carrier of a:] is set
id the carrier of a is V1() V4( the carrier of a) V5( the carrier of a) non empty total V28( the carrier of a, the carrier of a) Element of bool [: the carrier of a, the carrier of a:]
(a,a,(id a)) is () ()
(UN) is non empty () set
UN is non empty () set
(UN) is non empty () set
[:(UN),UN:] is set
bool [:(UN),UN:] is set
a is V1() V4((UN)) V5(UN) V6() non empty total V28((UN),UN) Element of bool [:(UN),UN:]
aa is () ((UN))
a . aa is Element of UN
(UN,aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
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
a is V1() V4((UN)) V5(UN) V6() non empty total V28((UN),UN) Element of bool [:(UN),UN:]
aa is V1() V4((UN)) V5(UN) V6() non empty total V28((UN),UN) Element of bool [:(UN),UN:]
C is () ((UN))
a . C is Element of UN
(UN,C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa . C is Element of UN
a is V1() V4((UN)) V5(UN) V6() non empty total V28((UN),UN) Element of bool [:(UN),UN:]
aa is () ((UN))
a . aa is Element of UN
(UN,aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
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
a is V1() V4((UN)) V5(UN) V6() non empty total V28((UN),UN) Element of bool [:(UN),UN:]
aa is V1() V4((UN)) V5(UN) V6() non empty total V28((UN),UN) Element of bool [:(UN),UN:]
C is () ((UN))
a . C is Element of UN
(UN,C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
aa . C is Element of UN
UN is non empty () set
(UN) is non empty () set
aa is () ((UN))
(UN,aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
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
C is () ((UN))
(UN,C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
UN is non empty () set
(UN) is non empty () set
aa is () ((UN))
(UN,aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
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
C is () ((UN))
(UN,C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(aa,C) is () () ()
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
G1 is () () (ia,ii)
c8 is () () (ii,ia)
(ii,ia,ii,G1,c8) is () () (ii,ii)
(G1,c8) is () () ()
UN is non empty () set
(UN) is non empty () set
[:(UN),(UN):] is set
[:[:(UN),(UN):],(UN):] is set
bool [:[:(UN),(UN):],(UN):] is set
aa is () ((UN))
(UN,aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
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
C is () ((UN))
(UN,C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(aa,C) is () () ()
aa is V1() V4([:(UN),(UN):]) V5((UN)) V6() Element of bool [:[:(UN),(UN):],(UN):]
dom aa is V1() V4((UN)) V5((UN)) Element of bool [:(UN),(UN):]
bool [:(UN),(UN):] is set
C is () ((UN))
ii is () ((UN))
[C,ii] is V25() set
(UN,C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(UN,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ia is () ((UN))
(UN,ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ii is () ((UN))
(UN,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
[ia,ii] is V25() set
c8 is () ((UN))
G1 is () ((UN))
[c8,G1] is V25() set
aa . (c8,G1) is set
(c8,G1) is () () ()
aa is V1() V4([:(UN),(UN):]) V5((UN)) V6() Element of bool [:[:(UN),(UN):],(UN):]
dom aa is V1() V4((UN)) V5((UN)) Element of bool [:(UN),(UN):]
bool [:(UN),(UN):] is set
C is V1() V4([:(UN),(UN):]) V5((UN)) V6() Element of bool [:[:(UN),(UN):],(UN):]
dom C is V1() V4((UN)) V5((UN)) Element of bool [:(UN),(UN):]
ia is set
ii is () ((UN))
c8 is () ((UN))
[ii,c8] is V25() set
(UN,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(UN,c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ia is set
ii is set
[ia,ii] is V25() set
aa . (ia,ii) is set
C . (ia,ii) is set
c8 is () ((UN))
G1 is () ((UN))
aa . (c8,G1) is set
(c8,G1) is () () ()
ia is set
ii is () ((UN))
c8 is () ((UN))
[ii,c8] is V25() set
(UN,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(UN,c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital (UN)
the of c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is non empty universal set
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is strict CatStr
UN is non empty universal set
(UN) is CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is strict CatStr
UN is non empty universal set
(UN) is non empty non void V53() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is strict CatStr
the carrier' of (UN) is non empty set
[: the carrier' of (UN), the carrier' of (UN):] is set
the Comp of (UN) is V1() V4([: the carrier' of (UN), the carrier' of (UN):]) V5( the carrier' of (UN)) V6() 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 set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is set
dom the Comp of (UN) is V1() V4( the carrier' of (UN)) V5( the carrier' of (UN)) Element of bool [: the carrier' of (UN), the carrier' of (UN):]
bool [: the carrier' of (UN), the carrier' of (UN):] is set
ii is Element of the carrier' of (UN)
C is Element of the carrier' of (UN)
[ii,C] is V25() set
dom ii is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Source of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is 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 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):]
the Target of (UN) . C is Element of the carrier of (UN)
ii is () (((UN)))
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ia is () (((UN)))
((UN),ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is non empty universal set
(UN) is non empty non void V53() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is 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)
c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
G1 is set
H1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
f is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
H1 is set
f is set
f is set
G is set
[H1,f,f,G] is V25() V26() V27() set
[H1,f,f] is V25() V26() set
[H1,f] is V25() set
[[H1,f],f] is V25() set
[[H1,f,f],G] is V25() set
ii is set
ia is set
[[H1,f,f,G],ii,ia] is V25() V26() set
[[H1,f,f,G],ii] is V25() set
[[[H1,f,f,G],ii],ia] is V25() set
G2 is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of G2 is non empty set
the addF of G2 is V1() V4([: the carrier of G2, the carrier of G2:]) V5( the carrier of G2) V6() total V28([: the carrier of G2, the carrier of G2:], the carrier of G2) Element of bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:]
[: the carrier of G2, the carrier of G2:] is set
[:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is set
bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:] is set
comp G2 is V1() V4( the carrier of G2) V5( the carrier of G2) V6() non empty total V28( the carrier of G2, the carrier of G2) Element of bool [: the carrier of G2, the carrier of G2:]
bool [: the carrier of G2, the carrier of G2:] is set
0. G2 is V48(G2) Element of the carrier of G2
the ZeroF of G2 is Element of the carrier of G2
the multF of G2 is V1() V4([: the carrier of G2, the carrier of G2:]) V5( the carrier of G2) V6() total V28([: the carrier of G2, the carrier of G2:], the carrier of G2) Element of bool [:[: the carrier of G2, the carrier of G2:], the carrier of G2:]
1. G2 is Element of the carrier of G2
the OneF of G2 is Element of the carrier of G2
UN is non empty universal set
(UN) is non empty non void V53() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is strict CatStr
the carrier' of (UN) is non empty set
dom ((UN)) is V1() V4(((UN))) V5(((UN))) Element of bool [:((UN)),((UN)):]
bool [:((UN)),((UN)):] is 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 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):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is 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 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):]
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)))
c8 is () (((UN)))
((UN),c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
[c8,ii] is V25() set
(c8,ii) is () () ()
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN),c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
[ia,ii] is V25() set
[: the carrier' of (UN), the carrier' of (UN):] is set
the Comp of (UN) is V1() V4([: the carrier' of (UN), the carrier' of (UN):]) V5( the carrier' of (UN)) V6() 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 set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is set
dom the Comp of (UN) is V1() V4( the carrier' of (UN)) V5( the carrier' of (UN)) Element of bool [: the carrier' of (UN), the carrier' of (UN):]
bool [: the carrier' of (UN), the carrier' of (UN):] is set
((UN)) . (c8,ii) is set
UN is non empty universal set
(UN) is non empty non void V53() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is 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 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):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is 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 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):]
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 right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ia is () () (((UN)))
((UN),ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(ii,ia) is () () ()
ii is () (((UN)))
((ii,ia)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (ii,ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN),ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((ii,ia)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of (ii,ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is non empty universal set
(UN) is non empty non void V53() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is 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 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):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is 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 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):]
the Target of (UN) . 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)
aa is Element of the carrier' of (UN)
cod aa is Element of 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)
ii (*) (C (*) aa) is Element of the carrier' of (UN)
ii (*) C is Element of the carrier' of (UN)
(ii (*) C) (*) aa is Element of the carrier' of (UN)
c8 is () () (((UN)))
ii is () () (((UN)))
(c8,ii) is () () ()
dom (ii (*) C) is Element of the carrier of (UN)
the Source of (UN) . (ii (*) C) is Element of the carrier of (UN)
((UN),c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of c8 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ia is () () (((UN)))
((UN),ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
(ii,ia) is () () ()
cod (C (*) aa) is Element of the carrier of (UN)
the Target of (UN) . (C (*) aa) is Element of the carrier of (UN)
G1 is () () (((UN)))
(c8,G1) is () () ()
H1 is () () (((UN)))
(H1,ia) is () () ()
UN is non empty universal set
(UN) is non empty non void V53() strict CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is strict CatStr
the carrier' of (UN) is non empty set
aa is Element of the carrier' of (UN)
the Comp of (UN) is V1() V4([: the carrier' of (UN), the carrier' of (UN):]) V5( the carrier' of (UN)) V6() Element of bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):]
[: the carrier' of (UN), the carrier' of (UN):] is set
[:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is set
bool [:[: the carrier' of (UN), the carrier' of (UN):], the carrier' of (UN):] is set
proj1 the Comp of (UN) is V1() set
cod aa is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Target of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is set
the Target of (UN) . aa is Element of the carrier of (UN)
C is Element of the carrier' of (UN)
[C,aa] is V25() set
dom C is Element of the carrier of (UN)
the Source of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Source of (UN) . C is Element of the carrier 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)
[ii,aa] is V25() set
the carrier' of (UN) is non empty set
aa is Element of the carrier' of (UN)
cod aa is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Target of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is set
the Target of (UN) . aa is Element of the carrier of (UN)
dom aa is Element of the carrier of (UN)
the Source of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
the Source of (UN) . aa is Element of the carrier of (UN)
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)
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)
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)
the carrier' of (UN) is non empty set
aa is Element of the carrier' of (UN)
cod aa is Element of the carrier of (UN)
the carrier of (UN) is non empty set
the Target of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is set
the Target of (UN) . aa is Element of the carrier of (UN)
ii is Element of the carrier' of (UN)
dom ii is Element of the carrier of (UN)
the Source of (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)) Element of bool [: the carrier' of (UN), 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)
dom C is Element of the carrier of (UN)
the Source of (UN) . C is Element of the carrier of (UN)
C (*) aa is Element of the carrier' of (UN)
ii (*) (C (*) aa) is Element of the carrier' of (UN)
ii (*) C is Element of the carrier' of (UN)
(ii (*) C) (*) aa is Element of the carrier' of (UN)
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 set
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = aa & cod b1 = aa ) } is set
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
ii is set
((UN),C) is () () (((UN)))
(C) is () () (C,C)
id C is V1() V4( the carrier of C) V5( the carrier of C) V6() non empty total V28( the carrier of C, the carrier of C) unity-preserving multiplicative additive (C,C) 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 set
bool [: the carrier of C, the carrier of C:] is set
id the carrier of C is V1() V4( the carrier of C) V5( the carrier of C) non empty total V28( the carrier of C, the carrier of C) Element of bool [: the carrier of C, the carrier of C:]
(C,C,(id C)) is () ()
ii is set
c8 is set
G1 is set
H1 is set
[ii,c8,G1,H1] is V25() V26() V27() set
[ii,c8,G1] is V25() V26() set
[ii,c8] is V25() set
[[ii,c8],G1] is V25() set
[[ii,c8,G1],H1] is V25() set
f is set
f is set
[[ii,c8,G1,H1],f,f] is V25() V26() set
[[ii,c8,G1,H1],f] is V25() set
[[[ii,c8,G1,H1],f],f] is V25() set
ii is non empty right_complementable strict V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the carrier of ii is non empty set
the addF of ii is V1() V4([: the carrier of ii, the carrier of ii:]) V5( the carrier of ii) V6() total V28([: the carrier of ii, the carrier of ii:], the carrier of ii) Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]
[: the carrier of ii, the carrier of ii:] is set
[:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set
bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:] is set
comp ii is V1() V4( the carrier of ii) V5( the carrier of ii) V6() non empty total V28( the carrier of ii, the carrier of ii) Element of bool [: the carrier of ii, the carrier of ii:]
bool [: the carrier of ii, the carrier of ii:] is set
0. ii is V48(ii) Element of the carrier of ii
the ZeroF of ii is Element of the carrier of ii
the multF of ii is V1() V4([: the carrier of ii, the carrier of ii:]) V5( the carrier of ii) V6() total V28([: the carrier of ii, the carrier of ii:], the carrier of ii) Element of bool [:[: the carrier of ii, the carrier of ii:], the carrier of ii:]
1. ii is Element of the carrier of ii
the OneF of ii is Element of the carrier of ii
ii is Element of the carrier' of (UN)
dom ii is Element of the carrier of (UN)
the Source of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is set
the Source of (UN) . ii is Element of the carrier of (UN)
ia is ()
(ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
cod ii is Element of the carrier of (UN)
the Target of (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)) 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 right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
UN is non empty universal set
(UN) is non empty non void V53() strict Category-like transitive associative reflexive CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is strict CatStr
the carrier of (UN) is non empty set
a is Element of the carrier of (UN)
aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
((UN),aa) is () () (((UN)))
(aa) is () () (aa,aa)
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 () ()
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 set
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = a & cod b1 = ii ) } is set
Hom (ii,a) is Element of bool the carrier' of (UN)
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = ii & cod b1 = a ) } is set
ia is Morphism of a,ii
ia (*) C is Element of the carrier' of (UN)
ii is () (((UN)))
G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
H1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the carrier of G1 is non empty set
the carrier of H1 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 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,f) is () ()
Hom (a,a) is Element of bool the carrier' of (UN)
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = a & cod b1 = a ) } is set
dom ia is Element of the carrier of (UN)
the Source of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is 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 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):]
the Target of (UN) . C is Element of the carrier of (UN)
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
c8 is () (((UN)))
((UN),c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of c8 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 aa, the carrier of H1:] is set
bool [: the carrier of aa, the carrier of H1:] is set
[ii,c8] is V25() set
dom ((UN)) is V1() V4(((UN))) V5(((UN))) Element of bool [:((UN)),((UN)):]
bool [:((UN)),((UN)):] is set
((UN)) . (ia,C) is set
(ii,c8) is () () ()
f is V1() V4( the carrier of aa) V5( the carrier of H1) V6() non empty total V28( the carrier of aa, the carrier of H1) Element of bool [: the carrier of aa, the carrier of H1:]
f * (id aa) is V1() V4( the carrier of aa) V5( the carrier of H1) V6() non empty total V28( the carrier of aa, the carrier of H1) Element of bool [: the carrier of aa, the carrier of H1:]
(aa,H1,(f * (id aa))) is () ()
ia is Morphism of ii,a
C (*) ia is Element of the carrier' of (UN)
ii is () (((UN)))
G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
H1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the carrier of G1 is non empty set
the carrier of H1 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 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,f) is () ()
Hom (a,a) is Element of bool the carrier' of (UN)
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = a & cod b1 = a ) } is set
cod ia is Element of the carrier of (UN)
the Target of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is 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 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):]
the Source of (UN) . C is Element of the carrier of (UN)
((UN),ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
c8 is () (((UN)))
((UN),c8) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
the of c8 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 G1, the carrier of aa:] is set
bool [: the carrier of G1, the carrier of aa:] is set
[c8,ii] is V25() set
dom ((UN)) is V1() V4(((UN))) V5(((UN))) Element of bool [:((UN)),((UN)):]
bool [:((UN)),((UN)):] is set
((UN)) . (C,ia) is set
(c8,ii) is () () ()
f is V1() V4( the carrier of G1) V5( the carrier of aa) V6() non empty total V28( the carrier of G1, the carrier of aa) Element of bool [: the carrier of G1, the carrier of aa:]
(id aa) * f is V1() V4( the carrier of G1) V5( the carrier of aa) V6() non empty total V28( the carrier of G1, the carrier of aa) Element of bool [: the carrier of G1, the carrier of aa:]
(G1,aa,((id aa) * f)) is () ()
UN is non empty universal set
(UN) is non empty non void V53() strict Category-like transitive associative reflexive CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is strict CatStr
the carrier of (UN) is non empty set
aa is Element of the carrier of (UN)
the carrier' of (UN) is non empty set
C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
((UN),C) is () () (((UN)))
(C) is () () (C,C)
id C is V1() V4( the carrier of C) V5( the carrier of C) V6() non empty total V28( the carrier of C, the carrier of C) unity-preserving multiplicative additive (C,C) 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 set
bool [: the carrier of C, the carrier of C:] is set
id the carrier of C is V1() V4( the carrier of C) V5( the carrier of C) non empty total V28( the carrier of C, the carrier of C) Element of bool [: the carrier of C, the carrier of C:]
(C,C,(id C)) is () ()
ii is Element of the carrier' of (UN)
dom ii is Element of the carrier of (UN)
the Source of (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)) Element of bool [: the carrier' of (UN), the carrier of (UN):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is set
the Source of (UN) . ii is Element of the carrier of (UN)
ia is ()
(ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
cod ii is Element of the carrier of (UN)
the Target of (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)) 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 right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ii is Morphism of aa,aa
c8 is Element of the carrier of (UN)
H1 is Element of the carrier of (UN)
Hom (aa,c8) is Element of bool the carrier' of (UN)
bool the carrier' of (UN) is set
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = aa & cod b1 = c8 ) } is set
G1 is Morphism of aa,c8
G1 (*) ii is Element of the carrier' of (UN)
Hom (H1,aa) is Element of bool the carrier' of (UN)
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = H1 & cod b1 = aa ) } is set
f is Morphism of H1,aa
ii (*) f is Element of the carrier' of (UN)
UN is non empty universal set
(UN) is non empty non void V53() strict Category-like transitive associative reflexive with_identities CatStr
(UN) is non empty () set
((UN)) is non empty () set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
[:((UN)),(UN):] is set
bool [:((UN)),(UN):] is set
((UN)) is V1() V4(((UN))) V5((UN)) V6() non empty total V28(((UN)),(UN)) Element of bool [:((UN)),(UN):]
((UN)) is V1() V4([:((UN)),((UN)):]) V5(((UN))) V6() Element of bool [:[:((UN)),((UN)):],((UN)):]
[:((UN)),((UN)):] is set
[:[:((UN)),((UN)):],((UN)):] is set
bool [:[:((UN)),((UN)):],((UN)):] is set
CatStr(# (UN),((UN)),((UN)),((UN)),((UN)) #) is 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 right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital ((UN))
((UN),aa) is () () (((UN)))
(aa) is () () (aa,aa)
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 () ()
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 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):]
[: the carrier' of (UN), the carrier of (UN):] is set
bool [: the carrier' of (UN), the carrier of (UN):] is set
the Source of (UN) . ii is Element of the carrier of (UN)
ia is ()
(ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
cod ii is Element of the carrier of (UN)
the Target of (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)) 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 right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr
ii is Morphism of a,a
c8 is Element of the carrier of (UN)
H1 is Element of the carrier of (UN)
Hom (a,c8) is Element of bool the carrier' of (UN)
bool the carrier' of (UN) is set
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = a & cod b1 = c8 ) } is set
G1 is Morphism of a,c8
G1 (*) ii is Element of the carrier' of (UN)
Hom (H1,a) is Element of bool the carrier' of (UN)
{ b1 where b1 is Element of the carrier' of (UN) : ( dom b1 = H1 & cod b1 = a ) } is set
f is Morphism of H1,a
ii (*) f is Element of the carrier' of (UN)