:: REALSET2 semantic presentation

K88() is set
K92() is non empty V21() V22() V23() V29() V34() V35() Element of bool K88()
bool K88() is non empty set
K87() is non empty V21() V22() V23() V29() V34() V35() set
bool K87() is non empty V29() set
bool K92() is non empty V29() set
{} is empty trivial V21() V22() V23() V25() V26() V27() V29() V34() V36( {} ) set
1 is non empty V21() V22() V23() V27() V29() V34() Element of K92()
{{}} is non empty trivial V36(1) set
2 is non empty V21() V22() V23() V27() V29() V34() Element of K92()
{{},1} is non empty set
0 is empty trivial V21() V22() V23() V25() V26() V27() V29() V34() V36( {} ) Element of K92()
(0,0) .--> 0 is Relation-like Function-like set
[0,0] is non empty set
{0,0} is non empty set
{0} is non empty trivial V36(1) set
{{0,0},{0}} is non empty set
{[0,0]} is non empty trivial V36(1) set
{[0,0]} --> 0 is Relation-like {[0,0]} -defined {0} -valued Function-like V18({[0,0]},{0}) Element of bool [:{[0,0]},{0}:]
[:{[0,0]},{0}:] is non empty set
bool [:{[0,0]},{0}:] is non empty set
(0,1) .--> 1 is Relation-like Function-like set
[0,1] is non empty set
{0,1} is non empty set
{{0,1},{0}} is non empty set
{[0,1]} is non empty trivial V36(1) set
{[0,1]} --> 1 is Relation-like {[0,1]} -defined {1} -valued Function-like V18({[0,1]},{1}) Element of bool [:{[0,1]},{1}:]
{1} is non empty trivial V36(1) set
[:{[0,1]},{1}:] is non empty set
bool [:{[0,1]},{1}:] is non empty set
((0,0) .--> 0) +* ((0,1) .--> 1) is Relation-like Function-like set
(1,0) .--> 1 is Relation-like Function-like set
[1,0] is non empty set
{1,0} is non empty set
{{1,0},{1}} is non empty set
{[1,0]} is non empty trivial V36(1) set
{[1,0]} --> 1 is Relation-like {[1,0]} -defined {1} -valued Function-like V18({[1,0]},{1}) Element of bool [:{[1,0]},{1}:]
[:{[1,0]},{1}:] is non empty set
bool [:{[1,0]},{1}:] is non empty set
(((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1) is Relation-like Function-like set
(1,1) .--> 0 is Relation-like Function-like set
[1,1] is non empty set
{1,1} is non empty set
{{1,1},{1}} is non empty set
{[1,1]} is non empty trivial V36(1) set
{[1,1]} --> 0 is Relation-like {[1,1]} -defined {0} -valued Function-like V18({[1,1]},{0}) Element of bool [:{[1,1]},{0}:]
[:{[1,1]},{0}:] is non empty set
bool [:{[1,1]},{0}:] is non empty set
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0) is Relation-like Function-like set
[:2,2:] is non empty set
[:[:2,2:],2:] is non empty set
bool [:[:2,2:],2:] is non empty set
dom (((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0)) is set
dom ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) is set
dom ((1,1) .--> 0) is set
(dom ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1))) \/ (dom ((1,1) .--> 0)) is set
[:K92(),K92():] is non empty V29() set
[1,1] is non empty Element of [:K92(),K92():]
{[1,1]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
bool [:K92(),K92():] is non empty V29() set
(dom ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1))) \/ {[1,1]} is non empty set
dom (((0,0) .--> 0) +* ((0,1) .--> 1)) is set
dom ((1,0) .--> 1) is set
(dom (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ (dom ((1,0) .--> 1)) is set
((dom (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ (dom ((1,0) .--> 1))) \/ {[1,1]} is non empty set
[1,0] is non empty Element of [:K92(),K92():]
{[1,0]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
(dom (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ {[1,0]} is non empty set
((dom (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ {[1,0]}) \/ {[1,1]} is non empty set
dom ((0,0) .--> 0) is set
dom ((0,1) .--> 1) is set
(dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 1)) is set
((dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 1))) \/ {[1,0]} is non empty set
(((dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 1))) \/ {[1,0]}) \/ {[1,1]} is non empty set
[0,1] is non empty Element of [:K92(),K92():]
{[0,1]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
(dom ((0,0) .--> 0)) \/ {[0,1]} is non empty set
((dom ((0,0) .--> 0)) \/ {[0,1]}) \/ {[1,0]} is non empty set
(((dom ((0,0) .--> 0)) \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} is non empty set
[0,0] is non empty Element of [:K92(),K92():]
{[0,0]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
{[0,0]} \/ {[0,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
({[0,0]} \/ {[0,1]}) \/ {[1,0]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
(({[0,0]} \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1]} \/ {[1,0]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
({[0,0],[0,1]} \/ {[1,0]}) \/ {[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1],[1,0]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1],[1,0]} \/ {[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1],[1,0],[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
rng ((0,0) .--> 0) is set
{1} is non empty trivial V36(1) Element of bool K92()
rng ((0,1) .--> 1) is set
(rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 1)) is set
rng ((1,0) .--> 1) is set
rng (((0,0) .--> 0) +* ((0,1) .--> 1)) is set
(rng (((0,0) .--> 0) +* ((0,1) .--> 1))) \/ (rng ((1,0) .--> 1)) is set
rng ((1,1) .--> 0) is set
rng ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) is set
(rng ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1))) \/ (rng ((1,1) .--> 0)) is set
rng (((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0)) is set
(0,1) .--> 0 is Relation-like Function-like set
{[0,1]} --> 0 is Relation-like {[0,1]} -defined {0} -valued Function-like V18({[0,1]},{0}) Element of bool [:{[0,1]},{0}:]
[:{[0,1]},{0}:] is non empty set
bool [:{[0,1]},{0}:] is non empty set
((0,0) .--> 0) +* ((0,1) .--> 0) is Relation-like Function-like set
(1,0) .--> 0 is Relation-like Function-like set
{[1,0]} --> 0 is Relation-like {[1,0]} -defined {0} -valued Function-like V18({[1,0]},{0}) Element of bool [:{[1,0]},{0}:]
[:{[1,0]},{0}:] is non empty set
bool [:{[1,0]},{0}:] is non empty set
(((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0) is Relation-like Function-like set
(1,1) .--> 1 is Relation-like Function-like set
{[1,1]} --> 1 is Relation-like {[1,1]} -defined {1} -valued Function-like V18({[1,1]},{1}) Element of bool [:{[1,1]},{1}:]
[:{[1,1]},{1}:] is non empty set
bool [:{[1,1]},{1}:] is non empty set
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1) is Relation-like Function-like set
rng ((1,1) .--> 1) is set
{1} is non empty trivial V36(1) Element of bool K92()
dom (((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1)) is set
dom ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) is set
dom ((1,1) .--> 1) is set
(dom ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0))) \/ (dom ((1,1) .--> 1)) is set
[:K92(),K92():] is non empty V29() set
[1,1] is non empty Element of [:K92(),K92():]
{[1,1]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
bool [:K92(),K92():] is non empty V29() set
(dom ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0))) \/ {[1,1]} is non empty set
dom (((0,0) .--> 0) +* ((0,1) .--> 0)) is set
dom ((1,0) .--> 0) is set
(dom (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ (dom ((1,0) .--> 0)) is set
((dom (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ (dom ((1,0) .--> 0))) \/ {[1,1]} is non empty set
[1,0] is non empty Element of [:K92(),K92():]
{[1,0]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
(dom (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ {[1,0]} is non empty set
((dom (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ {[1,0]}) \/ {[1,1]} is non empty set
dom ((0,0) .--> 0) is set
dom ((0,1) .--> 0) is set
(dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 0)) is set
((dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 0))) \/ {[1,0]} is non empty set
(((dom ((0,0) .--> 0)) \/ (dom ((0,1) .--> 0))) \/ {[1,0]}) \/ {[1,1]} is non empty set
[0,1] is non empty Element of [:K92(),K92():]
{[0,1]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
(dom ((0,0) .--> 0)) \/ {[0,1]} is non empty set
((dom ((0,0) .--> 0)) \/ {[0,1]}) \/ {[1,0]} is non empty set
(((dom ((0,0) .--> 0)) \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} is non empty set
[0,0] is non empty Element of [:K92(),K92():]
{[0,0]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
{[0,0]} \/ {[0,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
({[0,0]} \/ {[0,1]}) \/ {[1,0]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
(({[0,0]} \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1]} \/ {[1,0]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
({[0,0],[0,1]} \/ {[1,0]}) \/ {[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1],[1,0]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1],[1,0]} \/ {[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
{[0,0],[0,1],[1,0],[1,1]} is Relation-like K92() -defined K92() -valued non empty Element of bool [:K92(),K92():]
rng ((0,0) .--> 0) is set
rng ((0,1) .--> 0) is set
(rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 0)) is set
rng ((1,0) .--> 0) is set
rng (((0,0) .--> 0) +* ((0,1) .--> 0)) is set
(rng (((0,0) .--> 0) +* ((0,1) .--> 0))) \/ (rng ((1,0) .--> 0)) is set
rng ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) is set
(rng ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0))) \/ (rng ((1,1) .--> 1)) is set
rng (((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1)) is set
() is Relation-like [:2,2:] -defined 2 -valued Function-like V18([:2,2:],2) Element of bool [:[:2,2:],2:]
() is Relation-like [:2,2:] -defined 2 -valued Function-like V18([:2,2:],2) Element of bool [:[:2,2:],2:]
In (0,2) is V21() V22() V23() Element of 2
In (1,2) is V21() V22() V23() Element of 2
A is non empty non trivial set
dom ((1,1) .--> 0) is set
[:K92(),K92():] is non empty V29() set
[1,1] is non empty Element of [:K92(),K92():]
{[1,1]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
bool [:K92(),K92():] is non empty V29() set
dom ((1,0) .--> 1) is set
[1,0] is non empty Element of [:K92(),K92():]
{[1,0]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
dom ((0,1) .--> 1) is set
[0,1] is non empty Element of [:K92(),K92():]
{[0,1]} is Relation-like K92() -defined K92() -valued non empty trivial V36(1) Element of bool [:K92(),K92():]
() . ((In (0,2)),(In (0,2))) is V21() V22() V23() Element of 2
[(In (0,2)),(In (0,2))] is non empty set
{(In (0,2)),(In (0,2))} is non empty set
{(In (0,2))} is non empty trivial V36(1) set
{{(In (0,2)),(In (0,2))},{(In (0,2))}} is non empty set
() . [(In (0,2)),(In (0,2))] is set
[(In (0,2)),(In (0,2))] is non empty Element of [:2,2:]
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . ((In (0,2)),(In (0,2))) is set
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . [(In (0,2)),(In (0,2))] is set
(((0,0) .--> 0) +* ((0,1) .--> 1)) . ((In (0,2)),(In (0,2))) is set
(((0,0) .--> 0) +* ((0,1) .--> 1)) . [(In (0,2)),(In (0,2))] is set
((0,0) .--> 0) . ((In (0,2)),(In (0,2))) is set
((0,0) .--> 0) . [(In (0,2)),(In (0,2))] is set
() . ((In (0,2)),(In (1,2))) is V21() V22() V23() Element of 2
[(In (0,2)),(In (1,2))] is non empty set
{(In (0,2)),(In (1,2))} is non empty set
{{(In (0,2)),(In (1,2))},{(In (0,2))}} is non empty set
() . [(In (0,2)),(In (1,2))] is set
[(In (0,2)),(In (1,2))] is non empty Element of [:2,2:]
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . ((In (0,2)),(In (1,2))) is set
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . [(In (0,2)),(In (1,2))] is set
(((0,0) .--> 0) +* ((0,1) .--> 1)) . ((In (0,2)),(In (1,2))) is set
(((0,0) .--> 0) +* ((0,1) .--> 1)) . [(In (0,2)),(In (1,2))] is set
((0,1) .--> 1) . ((In (0,2)),(In (1,2))) is set
((0,1) .--> 1) . [(In (0,2)),(In (1,2))] is set
() . ((In (1,2)),(In (0,2))) is V21() V22() V23() Element of 2
[(In (1,2)),(In (0,2))] is non empty set
{(In (1,2)),(In (0,2))} is non empty set
{(In (1,2))} is non empty trivial V36(1) set
{{(In (1,2)),(In (0,2))},{(In (1,2))}} is non empty set
() . [(In (1,2)),(In (0,2))] is set
[(In (1,2)),(In (0,2))] is non empty Element of [:2,2:]
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . ((In (1,2)),(In (0,2))) is set
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . [(In (1,2)),(In (0,2))] is set
((1,0) .--> 1) . ((In (1,2)),(In (0,2))) is set
((1,0) .--> 1) . [(In (1,2)),(In (0,2))] is set
() . ((In (1,2)),(In (1,2))) is V21() V22() V23() Element of 2
[(In (1,2)),(In (1,2))] is non empty set
{(In (1,2)),(In (1,2))} is non empty set
{{(In (1,2)),(In (1,2))},{(In (1,2))}} is non empty set
() . [(In (1,2)),(In (1,2))] is set
[(In (1,2)),(In (1,2))] is non empty Element of [:2,2:]
((1,1) .--> 0) . ((In (1,2)),(In (1,2))) is set
((1,1) .--> 0) . [(In (1,2)),(In (1,2))] is set
dom ((1,1) .--> 1) is set
dom ((1,0) .--> 0) is set
dom ((0,1) .--> 0) is set
() . ((In (0,2)),(In (0,2))) is V21() V22() V23() Element of 2
() . [(In (0,2)),(In (0,2))] is set
[(In (0,2)),(In (0,2))] is non empty Element of [:2,2:]
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (0,2)),(In (0,2))) is set
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . [(In (0,2)),(In (0,2))] is set
(((0,0) .--> 0) +* ((0,1) .--> 0)) . ((In (0,2)),(In (0,2))) is set
(((0,0) .--> 0) +* ((0,1) .--> 0)) . [(In (0,2)),(In (0,2))] is set
((0,0) .--> 0) . ((In (0,2)),(In (0,2))) is set
((0,0) .--> 0) . [(In (0,2)),(In (0,2))] is set
() . ((In (0,2)),(In (1,2))) is V21() V22() V23() Element of 2
() . [(In (0,2)),(In (1,2))] is set
[(In (0,2)),(In (1,2))] is non empty Element of [:2,2:]
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (0,2)),(In (1,2))) is set
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . [(In (0,2)),(In (1,2))] is set
(((0,0) .--> 0) +* ((0,1) .--> 0)) . ((In (0,2)),(In (1,2))) is set
(((0,0) .--> 0) +* ((0,1) .--> 0)) . [(In (0,2)),(In (1,2))] is set
((0,1) .--> 0) . ((In (0,2)),(In (1,2))) is set
((0,1) .--> 0) . [(In (0,2)),(In (1,2))] is set
() . ((In (1,2)),(In (0,2))) is V21() V22() V23() Element of 2
() . [(In (1,2)),(In (0,2))] is set
[(In (1,2)),(In (0,2))] is non empty Element of [:2,2:]
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (1,2)),(In (0,2))) is set
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . [(In (1,2)),(In (0,2))] is set
((1,0) .--> 0) . ((In (1,2)),(In (0,2))) is set
((1,0) .--> 0) . [(In (1,2)),(In (0,2))] is set
() . ((In (1,2)),(In (1,2))) is V21() V22() V23() Element of 2
() . [(In (1,2)),(In (1,2))] is set
[(In (1,2)),(In (1,2))] is non empty Element of [:2,2:]
((1,1) .--> 1) . ((In (1,2)),(In (1,2))) is set
((1,1) .--> 1) . [(In (1,2)),(In (1,2))] is set
{(In (0,2))} is non empty trivial V36(1) Element of bool 2
bool 2 is non empty set
A \ {(In (0,2))} is Element of bool A
bool A is non empty set
{(In (1,2))} is non empty trivial V36(1) Element of bool 2
[:(A \ {(In (0,2))}),(A \ {(In (0,2))}):] is set
[(In (1,2)),(In (1,2))] is non empty Element of [:2,2:]
{[(In (1,2)),(In (1,2))]} is Relation-like 2 -defined 2 -valued non empty trivial V36(1) Element of bool [:2,2:]
bool [:2,2:] is non empty set
nm is set
() . nm is set
nd is Element of A
{nd} is non empty trivial V36(1) Element of bool A
A \ {nd} is non empty Element of bool A
[:A,A:] is non empty set
[:[:A,A:],A:] is non empty set
bool [:[:A,A:],A:] is non empty set
dL is Element of A
om1 is Element of A
() . (dL,om1) is set
[dL,om1] is non empty set
{dL,om1} is non empty set
{dL} is non empty trivial V36(1) set
{{dL,om1},{dL}} is non empty set
() . [dL,om1] is set
L is Element of A
() . ((() . (dL,om1)),L) is set
[(() . (dL,om1)),L] is non empty set
{(() . (dL,om1)),L} is non empty set
{(() . (dL,om1))} is non empty trivial V36(1) set
{{(() . (dL,om1)),L},{(() . (dL,om1))}} is non empty set
() . [(() . (dL,om1)),L] is set
() . (om1,L) is set
[om1,L] is non empty set
{om1,L} is non empty set
{om1} is non empty trivial V36(1) set
{{om1,L},{om1}} is non empty set
() . [om1,L] is set
() . (dL,(() . (om1,L))) is set
[dL,(() . (om1,L))] is non empty set
{dL,(() . (om1,L))} is non empty set
{{dL,(() . (om1,L))},{dL}} is non empty set
() . [dL,(() . (om1,L))] is set
od0 is Relation-like [:A,A:] -defined A -valued Function-like V18([:A,A:],A) Element of bool [:[:A,A:],A:]
om0 is Relation-like [:A,A:] -defined A -valued Function-like V18([:A,A:],A) Element of bool [:[:A,A:],A:]
nm is Element of A \ {nd}
doubleLoopStr(# A,od0,om0,nm,nd #) is non empty non trivial strict doubleLoopStr
dL is non empty doubleLoopStr
the carrier of dL is non empty set
0. dL is V48(dL) Element of the carrier of dL
the ZeroF of dL is Element of the carrier of dL
om1 is Element of the carrier of dL
om1 + (0. dL) is Element of the carrier of dL
the addF of dL is Relation-like [: the carrier of dL, the carrier of dL:] -defined the carrier of dL -valued Function-like V18([: the carrier of dL, the carrier of dL:], the carrier of dL) Element of bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:]
[: the carrier of dL, the carrier of dL:] is non empty set
[:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
the addF of dL . (om1,(0. dL)) is Element of the carrier of dL
[om1,(0. dL)] is non empty set
{om1,(0. dL)} is non empty set
{om1} is non empty trivial V36(1) set
{{om1,(0. dL)},{om1}} is non empty set
the addF of dL . [om1,(0. dL)] is set
om1 is Element of the carrier of dL
L is Element of the carrier of dL
om1 + L is Element of the carrier of dL
the addF of dL is Relation-like [: the carrier of dL, the carrier of dL:] -defined the carrier of dL -valued Function-like V18([: the carrier of dL, the carrier of dL:], the carrier of dL) Element of bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:]
[: the carrier of dL, the carrier of dL:] is non empty set
[:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
the addF of dL . (om1,L) is Element of the carrier of dL
[om1,L] is non empty set
{om1,L} is non empty set
{om1} is non empty trivial V36(1) set
{{om1,L},{om1}} is non empty set
the addF of dL . [om1,L] is set
x is Element of the carrier of dL
(om1 + L) + x is Element of the carrier of dL
the addF of dL . ((om1 + L),x) is Element of the carrier of dL
[(om1 + L),x] is non empty set
{(om1 + L),x} is non empty set
{(om1 + L)} is non empty trivial V36(1) set
{{(om1 + L),x},{(om1 + L)}} is non empty set
the addF of dL . [(om1 + L),x] is set
L + x is Element of the carrier of dL
the addF of dL . (L,x) is Element of the carrier of dL
[L,x] is non empty set
{L,x} is non empty set
{L} is non empty trivial V36(1) set
{{L,x},{L}} is non empty set
the addF of dL . [L,x] is set
om1 + (L + x) is Element of the carrier of dL
the addF of dL . (om1,(L + x)) is Element of the carrier of dL
[om1,(L + x)] is non empty set
{om1,(L + x)} is non empty set
{{om1,(L + x)},{om1}} is non empty set
the addF of dL . [om1,(L + x)] is set
om1 is Element of the carrier of dL
L is Element of the carrier of dL
om1 + L is Element of the carrier of dL
the addF of dL is Relation-like [: the carrier of dL, the carrier of dL:] -defined the carrier of dL -valued Function-like V18([: the carrier of dL, the carrier of dL:], the carrier of dL) Element of bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:]
[: the carrier of dL, the carrier of dL:] is non empty set
[:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
the addF of dL . (om1,L) is Element of the carrier of dL
[om1,L] is non empty set
{om1,L} is non empty set
{om1} is non empty trivial V36(1) set
{{om1,L},{om1}} is non empty set
the addF of dL . [om1,L] is set
L + om1 is Element of the carrier of dL
the addF of dL . (L,om1) is Element of the carrier of dL
[L,om1] is non empty set
{L,om1} is non empty set
{L} is non empty trivial V36(1) set
{{L,om1},{L}} is non empty set
the addF of dL . [L,om1] is set
L is non empty set
[:L,L:] is non empty set
[:[:L,L:],L:] is non empty set
bool [:[:L,L:],L:] is non empty set
x is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]
x is Element of L
addLoopStr(# L,x,x #) is non empty strict addLoopStr
the carrier of addLoopStr(# L,x,x #) is non empty set
y is Element of the carrier of addLoopStr(# L,x,x #)
y + y is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) is Relation-like [: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] -defined the carrier of addLoopStr(# L,x,x #) -valued Function-like V18([: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #)) Element of bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):]
[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] is non empty set
[:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
the addF of addLoopStr(# L,x,x #) . (y,y) is Element of the carrier of addLoopStr(# L,x,x #)
[y,y] is non empty set
{y,y} is non empty set
{y} is non empty trivial V36(1) set
{{y,y},{y}} is non empty set
the addF of addLoopStr(# L,x,x #) . [y,y] is set
0. addLoopStr(# L,x,x #) is V48( addLoopStr(# L,x,x #)) Element of the carrier of addLoopStr(# L,x,x #)
the ZeroF of addLoopStr(# L,x,x #) is Element of the carrier of addLoopStr(# L,x,x #)
y is Element of L
c₁₆ is Element of L
x . (y,c₁₆) is Element of L
[y,c₁₆] is non empty set
{y,c₁₆} is non empty set
{y} is non empty trivial V36(1) set
{{y,c₁₆},{y}} is non empty set
x . [y,c₁₆] is set
ra is Element of L
x . ((x . (y,c₁₆)),ra) is Element of L
[(x . (y,c₁₆)),ra] is non empty set
{(x . (y,c₁₆)),ra} is non empty set
{(x . (y,c₁₆))} is non empty trivial V36(1) set
{{(x . (y,c₁₆)),ra},{(x . (y,c₁₆))}} is non empty set
x . [(x . (y,c₁₆)),ra] is set
x . (c₁₆,ra) is Element of L
[c₁₆,ra] is non empty set
{c₁₆,ra} is non empty set
{c₁₆} is non empty trivial V36(1) set
{{c₁₆,ra},{c₁₆}} is non empty set
x . [c₁₆,ra] is set
x . (y,(x . (c₁₆,ra))) is Element of L
[y,(x . (c₁₆,ra))] is non empty set
{y,(x . (c₁₆,ra))} is non empty set
{{y,(x . (c₁₆,ra))},{y}} is non empty set
x . [y,(x . (c₁₆,ra))] is set
the carrier of addLoopStr(# L,x,x #) is non empty set
y is Element of the carrier of addLoopStr(# L,x,x #)
c₁₆ is Element of the carrier of addLoopStr(# L,x,x #)
y + c₁₆ is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) is Relation-like [: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] -defined the carrier of addLoopStr(# L,x,x #) -valued Function-like V18([: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #)) Element of bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):]
[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] is non empty set
[:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
the addF of addLoopStr(# L,x,x #) . (y,c₁₆) is Element of the carrier of addLoopStr(# L,x,x #)
[y,c₁₆] is non empty set
{y,c₁₆} is non empty set
{y} is non empty trivial V36(1) set
{{y,c₁₆},{y}} is non empty set
the addF of addLoopStr(# L,x,x #) . [y,c₁₆] is set
ra is Element of the carrier of addLoopStr(# L,x,x #)
(y + c₁₆) + ra is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) . ((y + c₁₆),ra) is Element of the carrier of addLoopStr(# L,x,x #)
[(y + c₁₆),ra] is non empty set
{(y + c₁₆),ra} is non empty set
{(y + c₁₆)} is non empty trivial V36(1) set
{{(y + c₁₆),ra},{(y + c₁₆)}} is non empty set
the addF of addLoopStr(# L,x,x #) . [(y + c₁₆),ra] is set
c₁₆ + ra is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) . (c₁₆,ra) is Element of the carrier of addLoopStr(# L,x,x #)
[c₁₆,ra] is non empty set
{c₁₆,ra} is non empty set
{c₁₆} is non empty trivial V36(1) set
{{c₁₆,ra},{c₁₆}} is non empty set
the addF of addLoopStr(# L,x,x #) . [c₁₆,ra] is set
y + (c₁₆ + ra) is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) . (y,(c₁₆ + ra)) is Element of the carrier of addLoopStr(# L,x,x #)
[y,(c₁₆ + ra)] is non empty set
{y,(c₁₆ + ra)} is non empty set
{{y,(c₁₆ + ra)},{y}} is non empty set
the addF of addLoopStr(# L,x,x #) . [y,(c₁₆ + ra)] is set
y is Element of the carrier of addLoopStr(# L,x,x #)
c₁₆ is Element of the carrier of addLoopStr(# L,x,x #)
y + c₁₆ is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) is Relation-like [: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] -defined the carrier of addLoopStr(# L,x,x #) -valued Function-like V18([: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #)) Element of bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):]
[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] is non empty set
[:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
the addF of addLoopStr(# L,x,x #) . (y,c₁₆) is Element of the carrier of addLoopStr(# L,x,x #)
[y,c₁₆] is non empty set
{y,c₁₆} is non empty set
{y} is non empty trivial V36(1) set
{{y,c₁₆},{y}} is non empty set
the addF of addLoopStr(# L,x,x #) . [y,c₁₆] is set
c₁₆ + y is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) . (c₁₆,y) is Element of the carrier of addLoopStr(# L,x,x #)
[c₁₆,y] is non empty set
{c₁₆,y} is non empty set
{c₁₆} is non empty trivial V36(1) set
{{c₁₆,y},{c₁₆}} is non empty set
the addF of addLoopStr(# L,x,x #) . [c₁₆,y] is set
0. addLoopStr(# L,x,x #) is V48( addLoopStr(# L,x,x #)) Element of the carrier of addLoopStr(# L,x,x #)
the ZeroF of addLoopStr(# L,x,x #) is Element of the carrier of addLoopStr(# L,x,x #)
y is Element of the carrier of addLoopStr(# L,x,x #)
y + (0. addLoopStr(# L,x,x #)) is Element of the carrier of addLoopStr(# L,x,x #)
the addF of addLoopStr(# L,x,x #) is Relation-like [: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] -defined the carrier of addLoopStr(# L,x,x #) -valued Function-like V18([: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #)) Element of bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):]
[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):] is non empty set
[:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
bool [:[: the carrier of addLoopStr(# L,x,x #), the carrier of addLoopStr(# L,x,x #):], the carrier of addLoopStr(# L,x,x #):] is non empty set
the addF of addLoopStr(# L,x,x #) . (y,(0. addLoopStr(# L,x,x #))) is Element of the carrier of addLoopStr(# L,x,x #)
[y,(0. addLoopStr(# L,x,x #))] is non empty set
{y,(0. addLoopStr(# L,x,x #))} is non empty set
{y} is non empty trivial V36(1) set
{{y,(0. addLoopStr(# L,x,x #))},{y}} is non empty set
the addF of addLoopStr(# L,x,x #) . [y,(0. addLoopStr(# L,x,x #))] is set
L is Element of the carrier of dL
x is Element of the carrier of dL
x is Element of the carrier of dL
x + x is Element of the carrier of dL
the addF of dL is Relation-like [: the carrier of dL, the carrier of dL:] -defined the carrier of dL -valued Function-like V18([: the carrier of dL, the carrier of dL:], the carrier of dL) Element of bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:]
[: the carrier of dL, the carrier of dL:] is non empty set
[:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:] is non empty set
the addF of dL . (x,x) is Element of the carrier of dL
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of dL . [x,x] is set
L * (x + x) is Element of the carrier of dL
the multF of dL is Relation-like [: the carrier of dL, the carrier of dL:] -defined the carrier of dL -valued Function-like V18([: the carrier of dL, the carrier of dL:], the carrier of dL) Element of bool [:[: the carrier of dL, the carrier of dL:], the carrier of dL:]
the multF of dL . (L,(x + x)) is Element of the carrier of dL
[L,(x + x)] is non empty set
{L,(x + x)} is non empty set
{L} is non empty trivial V36(1) set
{{L,(x + x)},{L}} is non empty set
the multF of dL . [L,(x + x)] is set
L * x is Element of the carrier of dL
the multF of dL . (L,x) is Element of the carrier of dL
[L,x] is non empty set
{L,x} is non empty set
{{L,x},{L}} is non empty set
the multF of dL . [L,x] is set
L * x is Element of the carrier of dL
the multF of dL . (L,x) is Element of the carrier of dL
[L,x] is non empty set
{L,x} is non empty set
{{L,x},{L}} is non empty set
the multF of dL . [L,x] is set
(L * x) + (L * x) is Element of the carrier of dL
the addF of dL . ((L * x),(L * x)) is Element of the carrier of dL
[(L * x),(L * x)] is non empty set
{(L * x),(L * x)} is non empty set
{(L * x)} is non empty trivial V36(1) set
{{(L * x),(L * x)},{(L * x)}} is non empty set
the addF of dL . [(L * x),(L * x)] is set
(x + x) * L is Element of the carrier of dL
the multF of dL . ((x + x),L) is Element of the carrier of dL
[(x + x),L] is non empty set
{(x + x),L} is non empty set
{(x + x)} is non empty trivial V36(1) set
{{(x + x),L},{(x + x)}} is non empty set
the multF of dL . [(x + x),L] is set
x * L is Element of the carrier of dL
the multF of dL . (x,L) is Element of the carrier of dL
[x,L] is non empty set
{x,L} is non empty set
{{x,L},{x}} is non empty set
the multF of dL . [x,L] is set
x * L is Element of the carrier of dL
the multF of dL . (x,L) is Element of the carrier of dL
[x,L] is non empty set
{x,L} is non empty set
{x} is non empty trivial V36(1) set
{{x,L},{x}} is non empty set
the multF of dL . [x,L] is set
(x * L) + (x * L) is Element of the carrier of dL
the addF of dL . ((x * L),(x * L)) is Element of the carrier of dL
[(x * L),(x * L)] is non empty set
{(x * L),(x * L)} is non empty set
{(x * L)} is non empty trivial V36(1) set
{{(x * L),(x * L)},{(x * L)}} is non empty set
the addF of dL . [(x * L),(x * L)] is set
doubleLoopStr(# 2,(),(),(In (1,2)),(In (0,2)) #) is non empty strict doubleLoopStr
() is doubleLoopStr
the carrier of () is set
0. () is V48(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
1. () is Element of the carrier of ()
the OneF of () is Element of the carrier of ()
the carrier of () is non empty non trivial set
L is Element of the carrier of ()
x is Element of the carrier of ()
L + x is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (L,x) is Element of the carrier of ()
[L,x] is non empty set
{L,x} is non empty set
{L} is non empty trivial V36(1) set
{{L,x},{L}} is non empty set
the addF of () . [L,x] is set
x is Element of the carrier of ()
(L + x) + x is Element of the carrier of ()
the addF of () . ((L + x),x) is Element of the carrier of ()
[(L + x),x] is non empty set
{(L + x),x} is non empty set
{(L + x)} is non empty trivial V36(1) set
{{(L + x),x},{(L + x)}} is non empty set
the addF of () . [(L + x),x] is set
x + x is Element of the carrier of ()
the addF of () . (x,x) is Element of the carrier of ()
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of () . [x,x] is set
L + (x + x) is Element of the carrier of ()
the addF of () . (L,(x + x)) is Element of the carrier of ()
[L,(x + x)] is non empty set
{L,(x + x)} is non empty set
{{L,(x + x)},{L}} is non empty set
the addF of () . [L,(x + x)] is set
L is Element of the carrier of ()
x is Element of the carrier of ()
x is Element of the carrier of ()
x + x is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the addF of () . (x,x) is Element of the carrier of ()
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of () . [x,x] is set
L * (x + x) is Element of the carrier of ()
the multF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the multF of () . (L,(x + x)) is Element of the carrier of ()
[L,(x + x)] is non empty set
{L,(x + x)} is non empty set
{L} is non empty trivial V36(1) set
{{L,(x + x)},{L}} is non empty set
the multF of () . [L,(x + x)] is set
L * x is Element of the carrier of ()
the multF of () . (L,x) is Element of the carrier of ()
[L,x] is non empty set
{L,x} is non empty set
{{L,x},{L}} is non empty set
the multF of () . [L,x] is set
L * x is Element of the carrier of ()
the multF of () . (L,x) is Element of the carrier of ()
[L,x] is non empty set
{L,x} is non empty set
{{L,x},{L}} is non empty set
the multF of () . [L,x] is set
(L * x) + (L * x) is Element of the carrier of ()
the addF of () . ((L * x),(L * x)) is Element of the carrier of ()
[(L * x),(L * x)] is non empty set
{(L * x),(L * x)} is non empty set
{(L * x)} is non empty trivial V36(1) set
{{(L * x),(L * x)},{(L * x)}} is non empty set
the addF of () . [(L * x),(L * x)] is set
(x + x) * L is Element of the carrier of ()
the multF of () . ((x + x),L) is Element of the carrier of ()
[(x + x),L] is non empty set
{(x + x),L} is non empty set
{(x + x)} is non empty trivial V36(1) set
{{(x + x),L},{(x + x)}} is non empty set
the multF of () . [(x + x),L] is set
x * L is Element of the carrier of ()
the multF of () . (x,L) is Element of the carrier of ()
[x,L] is non empty set
{x,L} is non empty set
{{x,L},{x}} is non empty set
the multF of () . [x,L] is set
x * L is Element of the carrier of ()
the multF of () . (x,L) is Element of the carrier of ()
[x,L] is non empty set
{x,L} is non empty set
{x} is non empty trivial V36(1) set
{{x,L},{x}} is non empty set
the multF of () . [x,L] is set
(x * L) + (x * L) is Element of the carrier of ()
the addF of () . ((x * L),(x * L)) is Element of the carrier of ()
[(x * L),(x * L)] is non empty set
{(x * L),(x * L)} is non empty set
{(x * L)} is non empty trivial V36(1) set
{{(x * L),(x * L)},{(x * L)}} is non empty set
the addF of () . [(x * L),(x * L)] is set
the carrier of () is non empty non trivial set
L is set
L is Element of the carrier of ()
L is Element of the carrier of ()
L is non empty set
[:L,L:] is non empty set
[:[:L,L:],L:] is non empty set
bool [:[:L,L:],L:] is non empty set
x is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]
y is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]
c₁₆ is Element of L
x is Element of L
doubleLoopStr(# L,x,y,c₁₆,x #) is non empty strict doubleLoopStr
[:(A \ {nd}),(A \ {nd}):] is non empty set
om1 is Relation-like [:A,A:] -defined A -valued Function-like V18([:A,A:],A) DnT of nd,A
om1 ! (A,nd) is Relation-like [:(A \ {nd}),(A \ {nd}):] -defined A \ {nd} -valued Function-like V18([:(A \ {nd}),(A \ {nd}):],A \ {nd}) Element of bool [:[:(A \ {nd}),(A \ {nd}):],(A \ {nd}):]
[:[:(A \ {nd}),(A \ {nd}):],(A \ {nd}):] is non empty set
bool [:[:(A \ {nd}),(A \ {nd}):],(A \ {nd}):] is non empty set
om1 || (A \ {nd}) is Relation-like Function-like set
om1 | [:(A \ {nd}),(A \ {nd}):] is Relation-like set
L is non empty set
[:L,L:] is non empty set
[:[:L,L:],L:] is non empty set
bool [:[:L,L:],L:] is non empty set
x is Element of L
x is Relation-like [:L,L:] -defined L -valued Function-like V18([:L,L:],L) Element of bool [:[:L,L:],L:]
addLoopStr(# L,x,x #) is non empty strict addLoopStr
0. doubleLoopStr(# A,od0,om0,nm,nd #) is V48( doubleLoopStr(# A,od0,om0,nm,nd #)) Element of the carrier of doubleLoopStr(# A,od0,om0,nm,nd #)
the carrier of doubleLoopStr(# A,od0,om0,nm,nd #) is non empty non trivial set
the ZeroF of doubleLoopStr(# A,od0,om0,nm,nd #) is Element of the carrier of doubleLoopStr(# A,od0,om0,nm,nd #)
1. doubleLoopStr(# A,od0,om0,nm,nd #) is Element of the carrier of doubleLoopStr(# A,od0,om0,nm,nd #)
the OneF of doubleLoopStr(# A,od0,om0,nm,nd #) is Element of the carrier of doubleLoopStr(# A,od0,om0,nm,nd #)
x is non empty non degenerated non trivial doubleLoopStr
the multF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the carrier of x is non empty non trivial set
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
0. x is V48(x) Element of the carrier of x
the ZeroF of x is Element of the carrier of x
NonZero x is non empty Element of bool the carrier of x
bool the carrier of x is non empty set
[#] x is non empty non proper Element of bool the carrier of x
{(0. x)} is non empty trivial V36(1) set
([#] x) \ {(0. x)} is Element of bool the carrier of x
1. x is V48(x) Element of the carrier of x
the OneF of x is Element of the carrier of x
the multF of x || (NonZero x) is Relation-like Function-like set
[:(NonZero x),(NonZero x):] is non empty set
the multF of x | [:(NonZero x),(NonZero x):] is Relation-like set
x is Element of the carrier of x
x + x is Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the addF of x . (x,x) is Element of the carrier of x
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of x . [x,x] is set
x is non empty set
[:x,x:] is non empty set
[:[:x,x:],x:] is non empty set
bool [:[:x,x:],x:] is non empty set
c₁₆ is Element of x
y is Relation-like [:x,x:] -defined x -valued Function-like V18([:x,x:],x) Element of bool [:[:x,x:],x:]
addLoopStr(# x,y,c₁₆ #) is non empty strict addLoopStr
L is non empty non degenerated non trivial doubleLoopStr
NonZero L is non empty Element of bool the carrier of L
the carrier of L is non empty non trivial set
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
[:(NonZero L),(NonZero L):] is non empty set
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
x is set
the multF of L . x is set
y is set
c₁₆ is set
[y,c₁₆] is non empty set
{y,c₁₆} is non empty set
{y} is non empty trivial V36(1) set
{{y,c₁₆},{y}} is non empty set
C2a is Element of the carrier of L
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
ra is Element of the carrier of L
ra * C2a is Element of the carrier of L
the multF of L . (ra,C2a) is Element of the carrier of L
[ra,C2a] is non empty set
{ra,C2a} is non empty set
{ra} is non empty trivial V36(1) set
{{ra,C2a},{ra}} is non empty set
the multF of L . [ra,C2a] is set
1. L is V48(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
the multF of L || (NonZero L) is Relation-like Function-like set
the multF of L | [:(NonZero L),(NonZero L):] is Relation-like set
y is non empty set
[:y,y:] is non empty set
[:[:y,y:],y:] is non empty set
bool [:[:y,y:],y:] is non empty set
c₁₆ is Relation-like [:y,y:] -defined y -valued Function-like V18([:y,y:],y) Element of bool [:[:y,y:],y:]
ra is Element of y
addLoopStr(# y,c₁₆,ra #) is non empty strict addLoopStr
the carrier of addLoopStr(# y,c₁₆,ra #) is non empty set
b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
b + b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) is Relation-like [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] -defined the carrier of addLoopStr(# y,c₁₆,ra #) -valued Function-like V18([: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #)) Element of bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):]
[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
[:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . (b,b) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,b] is non empty set
{b,b} is non empty set
{b} is non empty trivial V36(1) set
{{b,b},{b}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [b,b] is set
b + b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) . (b,b) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,b] is non empty set
{b,b} is non empty set
{b} is non empty trivial V36(1) set
{{b,b},{b}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [b,b] is set
[b,b] is non empty Element of [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):]
[b,b] is non empty Element of [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):]
x is Element of the carrier of L
y is Element of the carrier of L
x * y is Element of the carrier of L
the multF of L . (x,y) is Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
y * x is Element of the carrier of L
the multF of L . (y,x) is Element of the carrier of L
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial V36(1) set
{{y,x},{y}} is non empty set
the multF of L . [y,x] is set
the carrier of addLoopStr(# y,c₁₆,ra #) is non empty set
b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
b is Element of the carrier of L
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
x is Element of the carrier of L
x * b is Element of the carrier of L
the multF of L . (x,b) is Element of the carrier of L
[x,b] is non empty set
{x,b} is non empty set
{x} is non empty trivial V36(1) set
{{x,b},{x}} is non empty set
the multF of L . [x,b] is set
b * x is Element of the carrier of L
the multF of L . (b,x) is Element of the carrier of L
[b,x] is non empty set
{b,x} is non empty set
{b} is non empty trivial V36(1) set
{{b,x},{b}} is non empty set
the multF of L . [b,x] is set
y is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
b + y is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) is Relation-like [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] -defined the carrier of addLoopStr(# y,c₁₆,ra #) -valued Function-like V18([: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #)) Element of bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):]
[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
[:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . (b,y) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,y] is non empty set
{b,y} is non empty set
{b} is non empty trivial V36(1) set
{{b,y},{b}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [b,y] is set
0. addLoopStr(# y,c₁₆,ra #) is V48( addLoopStr(# y,c₁₆,ra #)) Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the ZeroF of addLoopStr(# y,c₁₆,ra #) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,y] is non empty Element of [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):]
the carrier of addLoopStr(# y,c₁₆,ra #) is non empty set
b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
b + b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) is Relation-like [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] -defined the carrier of addLoopStr(# y,c₁₆,ra #) -valued Function-like V18([: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #)) Element of bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):]
[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
[:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . (b,b) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,b] is non empty set
{b,b} is non empty set
{b} is non empty trivial V36(1) set
{{b,b},{b}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [b,b] is set
x is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
(b + b) + x is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) . ((b + b),x) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[(b + b),x] is non empty set
{(b + b),x} is non empty set
{(b + b)} is non empty trivial V36(1) set
{{(b + b),x},{(b + b)}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [(b + b),x] is set
b + x is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) . (b,x) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,x] is non empty set
{b,x} is non empty set
{b} is non empty trivial V36(1) set
{{b,x},{b}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [b,x] is set
b + (b + x) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) . (b,(b + x)) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,(b + x)] is non empty set
{b,(b + x)} is non empty set
{{b,(b + x)},{b}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [b,(b + x)] is set
[b,x] is non empty Element of [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):]
c₁₆ . (b,x) is set
c₁₆ . [b,x] is set
x is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
x || y is Relation-like Function-like set
x | [:y,y:] is Relation-like set
(x || y) . (b,x) is set
(x || y) . [b,x] is set
[b,((x || y) . (b,x))] is non empty set
{b,((x || y) . (b,x))} is non empty set
{{b,((x || y) . (b,x))},{b}} is non empty set
[b,b] is non empty Element of [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):]
c₁₆ . (b,b) is set
c₁₆ . [b,b] is set
(x || y) . (b,b) is set
(x || y) . [b,b] is set
[((x || y) . (b,b)),x] is non empty set
{((x || y) . (b,b)),x} is non empty set
{((x || y) . (b,b))} is non empty trivial V36(1) set
{{((x || y) . (b,b)),x},{((x || y) . (b,b))}} is non empty set
x . (((x || y) . (b,b)),x) is set
x . [((x || y) . (b,b)),x] is set
y is Element of the carrier of L
x is Element of the carrier of L
y * x is Element of the carrier of L
the multF of L . (y,x) is Element of the carrier of L
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial V36(1) set
{{y,x},{y}} is non empty set
the multF of L . [y,x] is set
y is Element of the carrier of L
(y * x) * y is Element of the carrier of L
the multF of L . ((y * x),y) is Element of the carrier of L
[(y * x),y] is non empty set
{(y * x),y} is non empty set
{(y * x)} is non empty trivial V36(1) set
{{(y * x),y},{(y * x)}} is non empty set
the multF of L . [(y * x),y] is set
x * y is Element of the carrier of L
the multF of L . (x,y) is Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
y * (x * y) is Element of the carrier of L
the multF of L . (y,(x * y)) is Element of the carrier of L
[y,(x * y)] is non empty set
{y,(x * y)} is non empty set
{{y,(x * y)},{y}} is non empty set
the multF of L . [y,(x * y)] is set
x . (b,((x || y) . (b,x))) is set
x . [b,((x || y) . (b,x))] is set
the carrier of addLoopStr(# y,c₁₆,ra #) is non empty set
b is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
0. addLoopStr(# y,c₁₆,ra #) is V48( addLoopStr(# y,c₁₆,ra #)) Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the ZeroF of addLoopStr(# y,c₁₆,ra #) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
b + (0. addLoopStr(# y,c₁₆,ra #)) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
the addF of addLoopStr(# y,c₁₆,ra #) is Relation-like [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] -defined the carrier of addLoopStr(# y,c₁₆,ra #) -valued Function-like V18([: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #)) Element of bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):]
[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
[:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
bool [:[: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):], the carrier of addLoopStr(# y,c₁₆,ra #):] is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . (b,(0. addLoopStr(# y,c₁₆,ra #))) is Element of the carrier of addLoopStr(# y,c₁₆,ra #)
[b,(0. addLoopStr(# y,c₁₆,ra #))] is non empty set
{b,(0. addLoopStr(# y,c₁₆,ra #))} is non empty set
{b} is non empty trivial V36(1) set
{{b,(0. addLoopStr(# y,c₁₆,ra #))},{b}} is non empty set
the addF of addLoopStr(# y,c₁₆,ra #) . [b,(0. addLoopStr(# y,c₁₆,ra #))] is set
[b,(0. addLoopStr(# y,c₁₆,ra #))] is non empty Element of [: the carrier of addLoopStr(# y,c₁₆,ra #), the carrier of addLoopStr(# y,c₁₆,ra #):]
b is Element of the carrier of L
b * (1. L) is Element of the carrier of L
the multF of L . (b,(1. L)) is Element of the carrier of L
[b,(1. L)] is non empty set
{b,(1. L)} is non empty set
{b} is non empty trivial V36(1) set
{{b,(1. L)},{b}} is non empty set
the multF of L . [b,(1. L)] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the carrier of L is non empty non trivial set
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is non empty non trivial strict addLoopStr
the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is non empty non trivial set
x is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
y is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
x + y is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is Relation-like [: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] -defined the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) -valued Function-like V18([: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):]
[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
[:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . (x,y) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [x,y] is set
c₁₆ is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
(x + y) + c₁₆ is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . ((x + y),c₁₆) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[(x + y),c₁₆] is non empty set
{(x + y),c₁₆} is non empty set
{(x + y)} is non empty trivial V36(1) set
{{(x + y),c₁₆},{(x + y)}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [(x + y),c₁₆] is set
y + c₁₆ is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . (y,c₁₆) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[y,c₁₆] is non empty set
{y,c₁₆} is non empty set
{y} is non empty trivial V36(1) set
{{y,c₁₆},{y}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [y,c₁₆] is set
x + (y + c₁₆) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . (x,(y + c₁₆)) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[x,(y + c₁₆)] is non empty set
{x,(y + c₁₆)} is non empty set
{{x,(y + c₁₆)},{x}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [x,(y + c₁₆)] is set
ra is left_complementable right_complementable complementable Element of the carrier of L
C2a is left_complementable right_complementable complementable Element of the carrier of L
ra + C2a is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (ra,C2a) is left_complementable right_complementable complementable Element of the carrier of L
[ra,C2a] is non empty set
{ra,C2a} is non empty set
{ra} is non empty trivial V36(1) set
{{ra,C2a},{ra}} is non empty set
the addF of L . [ra,C2a] is set
b is left_complementable right_complementable complementable Element of the carrier of L
(ra + C2a) + b is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . ((ra + C2a),b) is left_complementable right_complementable complementable Element of the carrier of L
[(ra + C2a),b] is non empty set
{(ra + C2a),b} is non empty set
{(ra + C2a)} is non empty trivial V36(1) set
{{(ra + C2a),b},{(ra + C2a)}} is non empty set
the addF of L . [(ra + C2a),b] is set
C2a + b is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (C2a,b) is left_complementable right_complementable complementable Element of the carrier of L
[C2a,b] is non empty set
{C2a,b} is non empty set
{C2a} is non empty trivial V36(1) set
{{C2a,b},{C2a}} is non empty set
the addF of L . [C2a,b] is set
ra + (C2a + b) is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (ra,(C2a + b)) is left_complementable right_complementable complementable Element of the carrier of L
[ra,(C2a + b)] is non empty set
{ra,(C2a + b)} is non empty set
{{ra,(C2a + b)},{ra}} is non empty set
the addF of L . [ra,(C2a + b)] is set
the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is non empty non trivial set
x is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is V48( addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)) Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the ZeroF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
x + (0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is Relation-like [: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] -defined the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) -valued Function-like V18([: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):]
[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
[:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . (x,(0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #))) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[x,(0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #))] is non empty set
{x,(0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #))} is non empty set
{x} is non empty trivial V36(1) set
{{x,(0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #))},{x}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [x,(0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #))] is set
y is left_complementable right_complementable complementable Element of the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
y + (0. L) is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (y,(0. L)) is left_complementable right_complementable complementable Element of the carrier of L
[y,(0. L)] is non empty set
{y,(0. L)} is non empty set
{y} is non empty trivial V36(1) set
{{y,(0. L)},{y}} is non empty set
the addF of L . [y,(0. L)] is set
the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is non empty non trivial set
x is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
y is left_complementable right_complementable complementable Element of the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
c₁₆ is left_complementable right_complementable complementable Element of the carrier of L
y + c₁₆ is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (y,c₁₆) is left_complementable right_complementable complementable Element of the carrier of L
[y,c₁₆] is non empty set
{y,c₁₆} is non empty set
{y} is non empty trivial V36(1) set
{{y,c₁₆},{y}} is non empty set
the addF of L . [y,c₁₆] is set
ra is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
x + ra is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is Relation-like [: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] -defined the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) -valued Function-like V18([: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):]
[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
[:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . (x,ra) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[x,ra] is non empty set
{x,ra} is non empty set
{x} is non empty trivial V36(1) set
{{x,ra},{x}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [x,ra] is set
0. addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is V48( addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)) Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the ZeroF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is non empty non trivial set
x is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
y is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
x + y is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) is Relation-like [: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] -defined the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) -valued Function-like V18([: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)) Element of bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):]
[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
[:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
bool [:[: the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #), the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):], the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #):] is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . (x,y) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [x,y] is set
y + x is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . (y,x) is Element of the carrier of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #)
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial V36(1) set
{{y,x},{y}} is non empty set
the addF of addLoopStr(# the carrier of L, the addF of L, the ZeroF of L #) . [y,x] is set
c₁₆ is left_complementable right_complementable complementable Element of the carrier of L
ra is left_complementable right_complementable complementable Element of the carrier of L
c₁₆ + ra is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (c₁₆,ra) is left_complementable right_complementable complementable Element of the carrier of L
[c₁₆,ra] is non empty set
{c₁₆,ra} is non empty set
{c₁₆} is non empty trivial V36(1) set
{{c₁₆,ra},{c₁₆}} is non empty set
the addF of L . [c₁₆,ra] is set
ra + c₁₆ is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (ra,c₁₆) is left_complementable right_complementable complementable Element of the carrier of L
[ra,c₁₆] is non empty set
{ra,c₁₆} is non empty set
{ra} is non empty trivial V36(1) set
{{ra,c₁₆},{ra}} is non empty set
the addF of L . [ra,c₁₆] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
x is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of x is non empty non trivial set
x is left_complementable right_complementable complementable Element of the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
x + (0. L) is left_complementable right_complementable complementable Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x,(0. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(0. L)] is non empty set
{x,(0. L)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(0. L)},{x}} is non empty set
the addF of L . [x,(0. L)] is set
0. x is V48(x) left_complementable right_complementable complementable Element of the carrier of x
the ZeroF of x is left_complementable right_complementable complementable Element of the carrier of x
y is left_complementable right_complementable complementable Element of the carrier of x
(0. x) + y is left_complementable right_complementable complementable Element of the carrier of x
the addF of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is non empty set
the addF of x . ((0. x),y) is left_complementable right_complementable complementable Element of the carrier of x
[(0. x),y] is non empty set
{(0. x),y} is non empty set
{(0. x)} is non empty trivial V36(1) set
{{(0. x),y},{(0. x)}} is non empty set
the addF of x . [(0. x),y] is set
L is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() addLoopStr
the carrier of L is non empty set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
x + x is left_complementable right_complementable complementable Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of L . [x,x] is set
x + x is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of L . [x,x] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
x is Element of NonZero L
x is Element of NonZero L
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
y is Element of NonZero L
(x * x) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((x * x),y) is left_complementable right_complementable complementable Element of the carrier of L
[(x * x),y] is non empty set
{(x * x),y} is non empty set
{(x * x)} is non empty trivial V36(1) set
{{(x * x),y},{(x * x)}} is non empty set
the multF of L . [(x * x),y] is set
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
x * (x * y) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(x * y)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(x * y)] is non empty set
{x,(x * y)} is non empty set
{{x,(x * y)},{x}} is non empty set
the multF of L . [x,(x * y)] is set
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
bool H₁(L) is non empty set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
(L) ! (H₁(L),(0. L)) is Relation-like [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] -defined H₁(L) \ {(0. L)} -valued Function-like V18([:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],H₁(L) \ {(0. L)}) Element of bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):]
{(0. L)} is non empty trivial V36(1) Element of bool H₁(L)
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
the carrier of L \ {(0. L)} is non empty Element of bool the carrier of L
(L) || ( the carrier of L \ {(0. L)}) is Relation-like Function-like set
[:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is non empty set
(L) | [:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is Relation-like set
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
C2a is Element of H₁(L) \ {(0. L)}
addLoopStr(# (H₁(L) \ {(0. L)}),((L) ! (H₁(L),(0. L))),C2a #) is non empty strict addLoopStr
b is non empty strict left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() addLoopStr
the carrier of b is non empty set
b is left_complementable right_complementable complementable Element of the carrier of b
x is left_complementable right_complementable complementable Element of the carrier of b
y is left_complementable right_complementable complementable Element of the carrier of b
(L) || (H₁(L) \ {(0. L)}) is Relation-like Function-like set
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
(L) | [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is Relation-like set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
dom ((L) || (H₁(L) \ {(0. L)})) is set
the addF of b is Relation-like [: the carrier of b, the carrier of b:] -defined the carrier of b -valued Function-like V18([: the carrier of b, the carrier of b:], the carrier of b) Element of bool [:[: the carrier of b, the carrier of b:], the carrier of b:]
[: the carrier of b, the carrier of b:] is non empty set
[:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
bool [:[: the carrier of b, the carrier of b:], the carrier of b:] is non empty set
x is Element of H₁(L) \ {(0. L)}
y is Element of H₁(L) \ {(0. L)}
(L) . (x,y) is left_complementable right_complementable complementable Element of H₁(L)
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
(L) . [x,y] is set
the addF of b . (x,y) is set
the addF of b . [x,y] is set
[x,y] is non empty Element of [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):]
x is Element of H₁(L) \ {(0. L)}
y is Element of H₁(L) \ {(0. L)}
the addF of b . (x,y) is set
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the addF of b . [x,y] is set
(L) . (x,y) is left_complementable right_complementable complementable Element of H₁(L)
(L) . [x,y] is set
[x,y] is non empty Element of [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):]
z is Relation-like [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] -defined H₁(L) \ {(0. L)} -valued Function-like V18([:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],H₁(L) \ {(0. L)}) Element of bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):]
z . (x,y) is Element of H₁(L) \ {(0. L)}
z . [x,y] is set
x is Element of H₁(L) \ {(0. L)}
y is Element of H₁(L) \ {(0. L)}
the addF of b . (x,y) is set
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the addF of b . [x,y] is set
z is Element of H₁(L) \ {(0. L)}
(L) . (( the addF of b . (x,y)),z) is set
[( the addF of b . (x,y)),z] is non empty set
{( the addF of b . (x,y)),z} is non empty set
{( the addF of b . (x,y))} is non empty trivial V36(1) set
{{( the addF of b . (x,y)),z},{( the addF of b . (x,y))}} is non empty set
(L) . [( the addF of b . (x,y)),z] is set
the addF of b . (( the addF of b . (x,y)),z) is set
the addF of b . [( the addF of b . (x,y)),z] is set
(L) . (y,z) is left_complementable right_complementable complementable Element of H₁(L)
[y,z] is non empty set
{y,z} is non empty set
{y} is non empty trivial V36(1) set
{{y,z},{y}} is non empty set
(L) . [y,z] is set
the addF of b . (x,((L) . (y,z))) is set
[x,((L) . (y,z))] is non empty set
{x,((L) . (y,z))} is non empty set
{{x,((L) . (y,z))},{x}} is non empty set
the addF of b . [x,((L) . (y,z))] is set
(L) . (x,((L) . (y,z))) is left_complementable right_complementable complementable Element of H₁(L)
(L) . [x,((L) . (y,z))] is set
x is left_complementable right_complementable complementable Element of the carrier of L
y is left_complementable right_complementable complementable Element of the carrier of L
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
z is left_complementable right_complementable complementable Element of the carrier of L
(x * y) * z is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((x * y),z) is left_complementable right_complementable complementable Element of the carrier of L
[(x * y),z] is non empty set
{(x * y),z} is non empty set
{(x * y)} is non empty trivial V36(1) set
{{(x * y),z},{(x * y)}} is non empty set
the multF of L . [(x * y),z] is set
the addF of b . (b,x) is left_complementable right_complementable complementable Element of the carrier of b
[b,x] is non empty set
{b,x} is non empty set
{b} is non empty trivial V36(1) set
{{b,x},{b}} is non empty set
the addF of b . [b,x] is set
(L) . (( the addF of b . (b,x)),y) is set
[( the addF of b . (b,x)),y] is non empty set
{( the addF of b . (b,x)),y} is non empty set
{( the addF of b . (b,x))} is non empty trivial V36(1) set
{{( the addF of b . (b,x)),y},{( the addF of b . (b,x))}} is non empty set
(L) . [( the addF of b . (b,x)),y] is set
b + x is left_complementable right_complementable complementable Element of the carrier of b
(b + x) + y is left_complementable right_complementable complementable Element of the carrier of b
the addF of b . ((b + x),y) is left_complementable right_complementable complementable Element of the carrier of b
[(b + x),y] is non empty set
{(b + x),y} is non empty set
{(b + x)} is non empty trivial V36(1) set
{{(b + x),y},{(b + x)}} is non empty set
the addF of b . [(b + x),y] is set
x + y is left_complementable right_complementable complementable Element of the carrier of b
the addF of b . (x,y) is left_complementable right_complementable complementable Element of the carrier of b
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the addF of b . [x,y] is set
b + (x + y) is left_complementable right_complementable complementable Element of the carrier of b
the addF of b . (b,(x + y)) is left_complementable right_complementable complementable Element of the carrier of b
[b,(x + y)] is non empty set
{b,(x + y)} is non empty set
{{b,(x + y)},{b}} is non empty set
the addF of b . [b,(x + y)] is set
(L) . (x,y) is set
(L) . [x,y] is set
the addF of b . (b,((L) . (x,y))) is set
[b,((L) . (x,y))] is non empty set
{b,((L) . (x,y))} is non empty set
{{b,((L) . (x,y))},{b}} is non empty set
the addF of b . [b,((L) . (x,y))] is set
y * z is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (y,z) is left_complementable right_complementable complementable Element of the carrier of L
[y,z] is non empty set
{y,z} is non empty set
{y} is non empty trivial V36(1) set
{{y,z},{y}} is non empty set
the multF of L . [y,z] is set
x * (y * z) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(y * z)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(y * z)] is non empty set
{x,(y * z)} is non empty set
{{x,(y * z)},{x}} is non empty set
the multF of L . [x,(y * z)] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
x is Element of NonZero L
x is Element of NonZero L
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
bool H₁(L) is non empty set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
(L) ! (H₁(L),(0. L)) is Relation-like [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] -defined H₁(L) \ {(0. L)} -valued Function-like V18([:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],H₁(L) \ {(0. L)}) Element of bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):]
{(0. L)} is non empty trivial V36(1) Element of bool H₁(L)
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
the carrier of L \ {(0. L)} is non empty Element of bool the carrier of L
(L) || ( the carrier of L \ {(0. L)}) is Relation-like Function-like set
[:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is non empty set
(L) | [:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is Relation-like set
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
ra is Element of H₁(L) \ {(0. L)}
addLoopStr(# (H₁(L) \ {(0. L)}),((L) ! (H₁(L),(0. L))),ra #) is non empty strict addLoopStr
C2a is non empty strict left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() addLoopStr
the carrier of C2a is non empty set
b is left_complementable right_complementable complementable Element of the carrier of C2a
b is left_complementable right_complementable complementable Element of the carrier of C2a
(L) || (H₁(L) \ {(0. L)}) is Relation-like Function-like set
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
(L) | [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is Relation-like set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
dom ((L) || (H₁(L) \ {(0. L)})) is set
the addF of C2a is Relation-like [: the carrier of C2a, the carrier of C2a:] -defined the carrier of C2a -valued Function-like V18([: the carrier of C2a, the carrier of C2a:], the carrier of C2a) Element of bool [:[: the carrier of C2a, the carrier of C2a:], the carrier of C2a:]
[: the carrier of C2a, the carrier of C2a:] is non empty set
[:[: the carrier of C2a, the carrier of C2a:], the carrier of C2a:] is non empty set
bool [:[: the carrier of C2a, the carrier of C2a:], the carrier of C2a:] is non empty set
x is Element of H₁(L) \ {(0. L)}
y is Element of H₁(L) \ {(0. L)}
(L) . (x,y) is left_complementable right_complementable complementable Element of H₁(L)
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
(L) . [x,y] is set
the addF of C2a . (x,y) is set
the addF of C2a . [x,y] is set
[x,y] is non empty Element of [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):]
x is left_complementable right_complementable complementable Element of the carrier of L
y is left_complementable right_complementable complementable Element of the carrier of L
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
b + b is left_complementable right_complementable complementable Element of the carrier of C2a
the addF of C2a . (b,b) is left_complementable right_complementable complementable Element of the carrier of C2a
[b,b] is non empty set
{b,b} is non empty set
{b} is non empty trivial V36(1) set
{{b,b},{b}} is non empty set
the addF of C2a . [b,b] is set
b + b is left_complementable right_complementable complementable Element of the carrier of C2a
the addF of C2a . (b,b) is left_complementable right_complementable complementable Element of the carrier of C2a
[b,b] is non empty set
{b,b} is non empty set
{b} is non empty trivial V36(1) set
{{b,b},{b}} is non empty set
the addF of C2a . [b,b] is set
y * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (y,x) is left_complementable right_complementable complementable Element of the carrier of L
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial V36(1) set
{{y,x},{y}} is non empty set
the multF of L . [y,x] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
x is Element of NonZero L
x * (1. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(1. L)] is non empty set
{x,(1. L)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(1. L)},{x}} is non empty set
the multF of L . [x,(1. L)] is set
(1. L) * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((1. L),x) is left_complementable right_complementable complementable Element of the carrier of L
[(1. L),x] is non empty set
{(1. L),x} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),x},{(1. L)}} is non empty set
the multF of L . [(1. L),x] is set
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
bool H₁(L) is non empty set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
(L) ! (H₁(L),(0. L)) is Relation-like [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] -defined H₁(L) \ {(0. L)} -valued Function-like V18([:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],H₁(L) \ {(0. L)}) Element of bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):]
{(0. L)} is non empty trivial V36(1) Element of bool H₁(L)
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
the carrier of L \ {(0. L)} is non empty Element of bool the carrier of L
(L) || ( the carrier of L \ {(0. L)}) is Relation-like Function-like set
[:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is non empty set
(L) | [:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is Relation-like set
c₁₆ is Element of H₁(L) \ {(0. L)}
addLoopStr(# (H₁(L) \ {(0. L)}),((L) ! (H₁(L),(0. L))),c₁₆ #) is non empty strict addLoopStr
ra is non empty strict left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() addLoopStr
the carrier of ra is non empty set
(L) || (H₁(L) \ {(0. L)}) is Relation-like Function-like set
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
(L) | [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is Relation-like set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
dom ((L) || (H₁(L) \ {(0. L)})) is set
the addF of ra is Relation-like [: the carrier of ra, the carrier of ra:] -defined the carrier of ra -valued Function-like V18([: the carrier of ra, the carrier of ra:], the carrier of ra) Element of bool [:[: the carrier of ra, the carrier of ra:], the carrier of ra:]
[: the carrier of ra, the carrier of ra:] is non empty set
[:[: the carrier of ra, the carrier of ra:], the carrier of ra:] is non empty set
bool [:[: the carrier of ra, the carrier of ra:], the carrier of ra:] is non empty set
b is Element of H₁(L) \ {(0. L)}
b is Element of H₁(L) \ {(0. L)}
(L) . (b,b) is left_complementable right_complementable complementable Element of H₁(L)
[b,b] is non empty set
{b,b} is non empty set
{b} is non empty trivial V36(1) set
{{b,b},{b}} is non empty set
(L) . [b,b] is set
the addF of ra . (b,b) is set
the addF of ra . [b,b] is set
[b,b] is non empty Element of [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):]
C2a is left_complementable right_complementable complementable Element of the carrier of ra
(L) . ((1. L),C2a) is set
[(1. L),C2a] is non empty set
{(1. L),C2a} is non empty set
{{(1. L),C2a},{(1. L)}} is non empty set
(L) . [(1. L),C2a] is set
0. ra is V48(ra) left_complementable right_complementable complementable Element of the carrier of ra
the ZeroF of ra is left_complementable right_complementable complementable Element of the carrier of ra
(0. ra) + C2a is left_complementable right_complementable complementable Element of the carrier of ra
the addF of ra . ((0. ra),C2a) is left_complementable right_complementable complementable Element of the carrier of ra
[(0. ra),C2a] is non empty set
{(0. ra),C2a} is non empty set
{(0. ra)} is non empty trivial V36(1) set
{{(0. ra),C2a},{(0. ra)}} is non empty set
the addF of ra . [(0. ra),C2a] is set
(L) . (C2a,(1. L)) is set
[C2a,(1. L)] is non empty set
{C2a,(1. L)} is non empty set
{C2a} is non empty trivial V36(1) set
{{C2a,(1. L)},{C2a}} is non empty set
(L) . [C2a,(1. L)] is set
C2a + (0. ra) is left_complementable right_complementable complementable Element of the carrier of ra
the addF of ra . (C2a,(0. ra)) is left_complementable right_complementable complementable Element of the carrier of ra
[C2a,(0. ra)] is non empty set
{C2a,(0. ra)} is non empty set
{{C2a,(0. ra)},{C2a}} is non empty set
the addF of ra . [C2a,(0. ra)] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
x is Element of NonZero L
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
bool H₁(L) is non empty set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
[: the carrier of L, the carrier of L:] is non empty set
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
(L) ! (H₁(L),(0. L)) is Relation-like [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] -defined H₁(L) \ {(0. L)} -valued Function-like V18([:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],H₁(L) \ {(0. L)}) Element of bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):]
{(0. L)} is non empty trivial V36(1) Element of bool H₁(L)
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
the carrier of L \ {(0. L)} is non empty Element of bool the carrier of L
(L) || ( the carrier of L \ {(0. L)}) is Relation-like Function-like set
[:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is non empty set
(L) | [:( the carrier of L \ {(0. L)}),( the carrier of L \ {(0. L)}):] is Relation-like set
c₁₆ is Element of H₁(L) \ {(0. L)}
addLoopStr(# (H₁(L) \ {(0. L)}),((L) ! (H₁(L),(0. L))),c₁₆ #) is non empty strict addLoopStr
ra is non empty strict left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() addLoopStr
the carrier of ra is non empty set
C2a is left_complementable right_complementable complementable Element of the carrier of ra
0. ra is V48(ra) left_complementable right_complementable complementable Element of the carrier of ra
the ZeroF of ra is left_complementable right_complementable complementable Element of the carrier of ra
b is left_complementable right_complementable complementable Element of the carrier of ra
C2a + b is left_complementable right_complementable complementable Element of the carrier of ra
the addF of ra is Relation-like [: the carrier of ra, the carrier of ra:] -defined the carrier of ra -valued Function-like V18([: the carrier of ra, the carrier of ra:], the carrier of ra) Element of bool [:[: the carrier of ra, the carrier of ra:], the carrier of ra:]
[: the carrier of ra, the carrier of ra:] is non empty set
[:[: the carrier of ra, the carrier of ra:], the carrier of ra:] is non empty set
bool [:[: the carrier of ra, the carrier of ra:], the carrier of ra:] is non empty set
the addF of ra . (C2a,b) is left_complementable right_complementable complementable Element of the carrier of ra
[C2a,b] is non empty set
{C2a,b} is non empty set
{C2a} is non empty trivial V36(1) set
{{C2a,b},{C2a}} is non empty set
the addF of ra . [C2a,b] is set
b + C2a is left_complementable right_complementable complementable Element of the carrier of ra
the addF of ra . (b,C2a) is left_complementable right_complementable complementable Element of the carrier of ra
[b,C2a] is non empty set
{b,C2a} is non empty set
{b} is non empty trivial V36(1) set
{{b,C2a},{b}} is non empty set
the addF of ra . [b,C2a] is set
b is Element of NonZero L
x * b is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,b) is left_complementable right_complementable complementable Element of the carrier of L
[x,b] is non empty set
{x,b} is non empty set
{x} is non empty trivial V36(1) set
{{x,b},{x}} is non empty set
the multF of L . [x,b] is set
b * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (b,x) is left_complementable right_complementable complementable Element of the carrier of L
[b,x] is non empty set
{b,x} is non empty set
{b} is non empty trivial V36(1) set
{{b,x},{b}} is non empty set
the multF of L . [b,x] is set
(L) || (H₁(L) \ {(0. L)}) is Relation-like Function-like set
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
(L) | [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is Relation-like set
[:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
bool [:[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):],(H₁(L) \ {(0. L)}):] is non empty set
dom ((L) || (H₁(L) \ {(0. L)})) is set
x is Element of H₁(L) \ {(0. L)}
y is Element of H₁(L) \ {(0. L)}
(L) . (x,y) is left_complementable right_complementable complementable Element of H₁(L)
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
(L) . [x,y] is set
the addF of ra . (x,y) is set
the addF of ra . [x,y] is set
[x,y] is non empty Element of [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):]
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
comp L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
x + x is left_complementable right_complementable complementable Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of L . [x,x] is set
(comp L) . x is left_complementable right_complementable complementable Element of the carrier of L
- x is left_complementable right_complementable complementable Element of the carrier of L
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
comp L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V18( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
bool [: the carrier of L, the carrier of L:] is non empty set
x is left_complementable right_complementable complementable Element of the carrier of L
(comp L) . x is left_complementable right_complementable complementable Element of the carrier of L
(comp L) . ((comp L) . x) is left_complementable right_complementable complementable Element of the carrier of L
- x is left_complementable right_complementable complementable Element of the carrier of L
- (- x) is left_complementable right_complementable complementable Element of the carrier of L
(comp L) . (- x) is left_complementable right_complementable complementable Element of the carrier of L
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
y is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of y is non empty non trivial set
C2a is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of C2a is non empty non trivial set
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of L . [x,x] is set
(y) is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) DnT of 0. y, the carrier of y
[: the carrier of y, the carrier of y:] is non empty set
0. y is V48(y) left_complementable right_complementable complementable Element of the carrier of y
the ZeroF of y is left_complementable right_complementable complementable Element of the carrier of y
the multF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set
c₁₆ is left_complementable right_complementable complementable Element of the carrier of y
ra is left_complementable right_complementable complementable Element of the carrier of y
(y) . (c₁₆,ra) is left_complementable right_complementable complementable Element of the carrier of y
[c₁₆,ra] is non empty set
{c₁₆,ra} is non empty set
{c₁₆} is non empty trivial V36(1) set
{{c₁₆,ra},{c₁₆}} is non empty set
(y) . [c₁₆,ra] is set
comp C2a is Relation-like the carrier of C2a -defined the carrier of C2a -valued Function-like V18( the carrier of C2a, the carrier of C2a) Element of bool [: the carrier of C2a, the carrier of C2a:]
[: the carrier of C2a, the carrier of C2a:] is non empty set
bool [: the carrier of C2a, the carrier of C2a:] is non empty set
b is left_complementable right_complementable complementable Element of the carrier of C2a
(comp C2a) . b is left_complementable right_complementable complementable Element of the carrier of C2a
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
y is left_complementable right_complementable complementable Element of the carrier of L
x - y is left_complementable right_complementable complementable Element of the carrier of L
- y is left_complementable right_complementable complementable Element of the carrier of L
x + (- y) is left_complementable right_complementable complementable Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x,(- y)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(- y)] is non empty set
{x,(- y)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(- y)},{x}} is non empty set
the addF of L . [x,(- y)] is set
x * (x - y) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the multF of L . (x,(x - y)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(x - y)] is non empty set
{x,(x - y)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(x - y)},{x}} is non empty set
the multF of L . [x,(x - y)] is set
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
(x * x) - (x * y) is left_complementable right_complementable complementable Element of the carrier of L
- (x * y) is left_complementable right_complementable complementable Element of the carrier of L
(x * x) + (- (x * y)) is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . ((x * x),(- (x * y))) is left_complementable right_complementable complementable Element of the carrier of L
[(x * x),(- (x * y))] is non empty set
{(x * x),(- (x * y))} is non empty set
{(x * x)} is non empty trivial V36(1) set
{{(x * x),(- (x * y))},{(x * x)}} is non empty set
the addF of L . [(x * x),(- (x * y))] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
x - x is left_complementable right_complementable complementable Element of the carrier of L
- x is left_complementable right_complementable complementable Element of the carrier of L
x + (- x) is left_complementable right_complementable complementable Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x,(- x)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(- x)] is non empty set
{x,(- x)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(- x)},{x}} is non empty set
the addF of L . [x,(- x)] is set
y is left_complementable right_complementable complementable Element of the carrier of L
(x - x) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
the multF of L . ((x - x),y) is left_complementable right_complementable complementable Element of the carrier of L
[(x - x),y] is non empty set
{(x - x),y} is non empty set
{(x - x)} is non empty trivial V36(1) set
{{(x - x),y},{(x - x)}} is non empty set
the multF of L . [(x - x),y] is set
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
(x * y) - (x * y) is left_complementable right_complementable complementable Element of the carrier of L
- (x * y) is left_complementable right_complementable complementable Element of the carrier of L
(x * y) + (- (x * y)) is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . ((x * y),(- (x * y))) is left_complementable right_complementable complementable Element of the carrier of L
[(x * y),(- (x * y))] is non empty set
{(x * y),(- (x * y))} is non empty set
{(x * y)} is non empty trivial V36(1) set
{{(x * y),(- (x * y))},{(x * y)}} is non empty set
the addF of L . [(x * y),(- (x * y))] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
x is left_complementable right_complementable complementable Element of the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
x * (0. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,(0. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(0. L)] is non empty set
{x,(0. L)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(0. L)},{x}} is non empty set
the multF of L . [x,(0. L)] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
(0. L) * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((0. L),x) is left_complementable right_complementable complementable Element of the carrier of L
[(0. L),x] is non empty set
{(0. L),x} is non empty set
{(0. L)} is non empty trivial V36(1) set
{{(0. L),x},{(0. L)}} is non empty set
the multF of L . [(0. L),x] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
- (x * x) is left_complementable right_complementable complementable Element of the carrier of L
- x is left_complementable right_complementable complementable Element of the carrier of L
x * (- x) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(- x)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(- x)] is non empty set
{x,(- x)} is non empty set
{{x,(- x)},{x}} is non empty set
the multF of L . [x,(- x)] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the carrier of L is non empty non trivial set
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
(1. L) * (0. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((1. L),(0. L)) is left_complementable right_complementable complementable Element of the carrier of L
[(1. L),(0. L)] is non empty set
{(1. L),(0. L)} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),(0. L)},{(1. L)}} is non empty set
the multF of L . [(1. L),(0. L)] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the carrier of L is non empty non trivial set
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
(0. L) * (1. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . ((0. L),(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
[(0. L),(1. L)] is non empty set
{(0. L),(1. L)} is non empty set
{(0. L)} is non empty trivial V36(1) set
{{(0. L),(1. L)},{(0. L)}} is non empty set
the multF of L . [(0. L),(1. L)] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
[: the carrier of L, the carrier of L:] is non empty set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
(L) . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
(L) . [x,x] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the carrier of L is non empty non trivial set
x is left_complementable right_complementable complementable Element of H₁(L)
x is left_complementable right_complementable complementable Element of H₁(L)
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
y is left_complementable right_complementable complementable Element of H₁(L)
(x * x) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((x * x),y) is left_complementable right_complementable complementable Element of the carrier of L
[(x * x),y] is non empty set
{(x * x),y} is non empty set
{(x * x)} is non empty trivial V36(1) set
{{(x * x),y},{(x * x)}} is non empty set
the multF of L . [(x * x),y] is set
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
x * (x * y) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(x * y)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(x * y)] is non empty set
{x,(x * y)} is non empty set
{{x,(x * y)},{x}} is non empty set
the multF of L . [x,(x * y)] is set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
(0. L) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((0. L),y) is left_complementable right_complementable complementable Element of the carrier of L
[(0. L),y] is non empty set
{(0. L),y} is non empty set
{(0. L)} is non empty trivial V36(1) set
{{(0. L),y},{(0. L)}} is non empty set
the multF of L . [(0. L),y] is set
(0. L) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((0. L),y) is left_complementable right_complementable complementable Element of the carrier of L
[(0. L),y] is non empty set
{(0. L),y} is non empty set
{(0. L)} is non empty trivial V36(1) set
{{(0. L),y},{(0. L)}} is non empty set
the multF of L . [(0. L),y] is set
x * (0. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(0. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(0. L)] is non empty set
{x,(0. L)} is non empty set
{{x,(0. L)},{x}} is non empty set
the multF of L . [x,(0. L)] is set
x * (0. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(0. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(0. L)] is non empty set
{x,(0. L)} is non empty set
{{x,(0. L)},{x}} is non empty set
the multF of L . [x,(0. L)] is set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the carrier of L is non empty non trivial set
x is left_complementable right_complementable complementable Element of H₁(L)
x is left_complementable right_complementable complementable Element of H₁(L)
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
L is non empty non degenerated non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed V99() right-distributive left-distributive distributive () doubleLoopStr
the carrier of L is non empty non trivial set
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of H₁(L)
x * (1. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(1. L)] is non empty set
{x,(1. L)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(1. L)},{x}} is non empty set
the multF of L . [x,(1. L)] is set
(1. L) * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((1. L),x) is left_complementable right_complementable complementable Element of the carrier of L
[(1. L),x] is non empty set
{(1. L),x} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),x},{(1. L)}} is non empty set
the multF of L . [(1. L),x] is set
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
NonZero L is non empty Element of bool the carrier of L
the carrier of L is non empty non trivial set
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
[:(NonZero L),(NonZero L):] is non empty set
bool [:(NonZero L),(NonZero L):] is non empty set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
[: the carrier of L, the carrier of L:] is non empty set
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
bool H₁(L) is non empty set
x is set
x is Element of NonZero L
y is Element of H₁(L) \ {(0. L)}
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
y * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (y,x) is left_complementable right_complementable complementable Element of the carrier of L
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial V36(1) set
{{y,x},{y}} is non empty set
the multF of L . [y,x] is set
c₁₆ is set
(L) . (x,c₁₆) is set
[x,c₁₆] is non empty set
{x,c₁₆} is non empty set
{x} is non empty trivial V36(1) set
{{x,c₁₆},{x}} is non empty set
(L) . [x,c₁₆] is set
[:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
bool [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):] is non empty set
x is Relation-like H₁(L) \ {(0. L)} -defined H₁(L) \ {(0. L)} -valued Function-like V18(H₁(L) \ {(0. L)},H₁(L) \ {(0. L)}) Element of bool [:(H₁(L) \ {(0. L)}),(H₁(L) \ {(0. L)}):]
x is Relation-like NonZero L -defined NonZero L -valued Function-like V18( NonZero L, NonZero L) Element of bool [:(NonZero L),(NonZero L):]
x is Element of NonZero L
x . x is Element of NonZero L
(L) . (x,(x . x)) is set
[x,(x . x)] is non empty set
{x,(x . x)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(x . x)},{x}} is non empty set
(L) . [x,(x . x)] is set
x is Relation-like NonZero L -defined NonZero L -valued Function-like V18( NonZero L, NonZero L) Element of bool [:(NonZero L),(NonZero L):]
x is Relation-like NonZero L -defined NonZero L -valued Function-like V18( NonZero L, NonZero L) Element of bool [:(NonZero L),(NonZero L):]
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
H₁(L) \ {(0. L)} is non empty Element of bool H₁(L)
bool H₁(L) is non empty set
y is set
x . y is set
x . y is set
ra is left_complementable right_complementable complementable Element of the carrier of L
ra * (1. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (ra,(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
[ra,(1. L)] is non empty set
{ra,(1. L)} is non empty set
{ra} is non empty trivial V36(1) set
{{ra,(1. L)},{ra}} is non empty set
the multF of L . [ra,(1. L)] is set
c₁₆ is left_complementable right_complementable complementable Element of the carrier of L
C2a is left_complementable right_complementable complementable Element of the carrier of L
c₁₆ * C2a is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (c₁₆,C2a) is left_complementable right_complementable complementable Element of the carrier of L
[c₁₆,C2a] is non empty set
{c₁₆,C2a} is non empty set
{c₁₆} is non empty trivial V36(1) set
{{c₁₆,C2a},{c₁₆}} is non empty set
the multF of L . [c₁₆,C2a] is set
ra * (c₁₆ * C2a) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (ra,(c₁₆ * C2a)) is left_complementable right_complementable complementable Element of the carrier of L
[ra,(c₁₆ * C2a)] is non empty set
{ra,(c₁₆ * C2a)} is non empty set
{{ra,(c₁₆ * C2a)},{ra}} is non empty set
the multF of L . [ra,(c₁₆ * C2a)] is set
c₁₆ * ra is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (c₁₆,ra) is left_complementable right_complementable complementable Element of the carrier of L
[c₁₆,ra] is non empty set
{c₁₆,ra} is non empty set
{{c₁₆,ra},{c₁₆}} is non empty set
the multF of L . [c₁₆,ra] is set
(c₁₆ * ra) * C2a is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((c₁₆ * ra),C2a) is left_complementable right_complementable complementable Element of the carrier of L
[(c₁₆ * ra),C2a] is non empty set
{(c₁₆ * ra),C2a} is non empty set
{(c₁₆ * ra)} is non empty trivial V36(1) set
{{(c₁₆ * ra),C2a},{(c₁₆ * ra)}} is non empty set
the multF of L . [(c₁₆ * ra),C2a] is set
(1. L) * C2a is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((1. L),C2a) is left_complementable right_complementable complementable Element of the carrier of L
[(1. L),C2a] is non empty set
{(1. L),C2a} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),C2a},{(1. L)}} is non empty set
the multF of L . [(1. L),C2a] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
(L) is Relation-like NonZero L -defined NonZero L -valued Function-like V18( NonZero L, NonZero L) Element of bool [:(NonZero L),(NonZero L):]
[:(NonZero L),(NonZero L):] is non empty set
bool [:(NonZero L),(NonZero L):] is non empty set
x is Element of NonZero L
x is Element of NonZero L
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
(L) . x is Element of NonZero L
x * (1. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(1. L)] is non empty set
{x,(1. L)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(1. L)},{x}} is non empty set
the multF of L . [x,(1. L)] is set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
(L) . (x,(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
(L) . [x,(1. L)] is set
y is left_complementable right_complementable complementable Element of the carrier of L
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
x * (x * y) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(x * y)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(x * y)] is non empty set
{x,(x * y)} is non empty set
{{x,(x * y)},{x}} is non empty set
the multF of L . [x,(x * y)] is set
(1. L) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((1. L),y) is left_complementable right_complementable complementable Element of the carrier of L
[(1. L),y] is non empty set
{(1. L),y} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),y},{(1. L)}} is non empty set
the multF of L . [(1. L),y] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
(L) is Relation-like NonZero L -defined NonZero L -valued Function-like V18( NonZero L, NonZero L) Element of bool [:(NonZero L),(NonZero L):]
[:(NonZero L),(NonZero L):] is non empty set
bool [:(NonZero L),(NonZero L):] is non empty set
x is Element of NonZero L
(L) . x is Element of NonZero L
(L) . ((L) . x) is Element of NonZero L
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
x * (1. L) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(1. L)] is non empty set
{x,(1. L)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(1. L)},{x}} is non empty set
the multF of L . [x,(1. L)] is set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
(L) . (x,(1. L)) is left_complementable right_complementable complementable Element of the carrier of L
(L) . [x,(1. L)] is set
x is left_complementable right_complementable complementable Element of the carrier of L
y is left_complementable right_complementable complementable Element of the carrier of L
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
x * (x * y) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,(x * y)) is left_complementable right_complementable complementable Element of the carrier of L
[x,(x * y)] is non empty set
{x,(x * y)} is non empty set
{{x,(x * y)},{x}} is non empty set
the multF of L . [x,(x * y)] is set
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
(x * x) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((x * x),y) is left_complementable right_complementable complementable Element of the carrier of L
[(x * x),y] is non empty set
{(x * x),y} is non empty set
{(x * x)} is non empty trivial V36(1) set
{{(x * x),y},{(x * x)}} is non empty set
the multF of L . [(x * x),y] is set
(L) . ((1. L),((L) . ((L) . x))) is set
[(1. L),((L) . ((L) . x))] is non empty set
{(1. L),((L) . ((L) . x))} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),((L) . ((L) . x))},{(1. L)}} is non empty set
(L) . [(1. L),((L) . ((L) . x))] is set
(1. L) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((1. L),y) is left_complementable right_complementable complementable Element of the carrier of L
[(1. L),y] is non empty set
{(1. L),y} is non empty set
{{(1. L),y},{(1. L)}} is non empty set
the multF of L . [(1. L),y] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
[: the carrier of L, the carrier of L:] is non empty set
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
(L) is Relation-like NonZero L -defined NonZero L -valued Function-like V18( NonZero L, NonZero L) Element of bool [:(NonZero L),(NonZero L):]
[:(NonZero L),(NonZero L):] is non empty set
bool [:(NonZero L),(NonZero L):] is non empty set
x is Element of NonZero L
x is Element of NonZero L
(L) . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
(L) . [x,x] is set
(L) . x is Element of NonZero L
[x,x] is non empty Element of [:(NonZero L),(NonZero L):]
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
x is left_complementable right_complementable complementable Element of the carrier of L
x is left_complementable right_complementable complementable Element of the carrier of L
x + x is left_complementable right_complementable complementable Element of the carrier of L
the addF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the addF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the addF of L . [x,x] is set
y is left_complementable right_complementable complementable Element of the carrier of L
x + y is left_complementable right_complementable complementable Element of the carrier of L
the addF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the addF of L . [x,y] is set
L is non empty non degenerated non trivial left_complementable right_complementable complementable almost_left_invertible Abelian add-associative right_zeroed V99() V107() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital () doubleLoopStr
the carrier of L is non empty non trivial set
NonZero L is non empty Element of bool the carrier of L
bool the carrier of L is non empty set
[#] L is non empty non proper Element of bool the carrier of L
0. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the ZeroF of L is left_complementable right_complementable complementable Element of the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
x is Element of NonZero L
x is left_complementable right_complementable complementable Element of H₁(L)
x * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is left_complementable right_complementable complementable Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
y is left_complementable right_complementable complementable Element of H₁(L)
x * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (x,y) is left_complementable right_complementable complementable Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
(L) is Relation-like NonZero L -defined NonZero L -valued Function-like V18( NonZero L, NonZero L) Element of bool [:(NonZero L),(NonZero L):]
[:(NonZero L),(NonZero L):] is non empty set
bool [:(NonZero L),(NonZero L):] is non empty set
(L) . x is Element of NonZero L
1. L is V48(L) left_complementable right_complementable complementable Element of the carrier of L
the OneF of L is left_complementable right_complementable complementable Element of the carrier of L
(1. L) * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((1. L),x) is left_complementable right_complementable complementable Element of the carrier of L
[(1. L),x] is non empty set
{(1. L),x} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),x},{(1. L)}} is non empty set
the multF of L . [(1. L),x] is set
(L) is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) DnT of 0. L, the carrier of L
(L) . ((1. L),x) is left_complementable right_complementable complementable Element of H₁(L)
(L) . [(1. L),x] is set
c₁₆ is left_complementable right_complementable complementable Element of the carrier of L
ra is left_complementable right_complementable complementable Element of the carrier of L
c₁₆ * ra is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (c₁₆,ra) is left_complementable right_complementable complementable Element of the carrier of L
[c₁₆,ra] is non empty set
{c₁₆,ra} is non empty set
{c₁₆} is non empty trivial V36(1) set
{{c₁₆,ra},{c₁₆}} is non empty set
the multF of L . [c₁₆,ra] is set
(c₁₆ * ra) * x is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((c₁₆ * ra),x) is left_complementable right_complementable complementable Element of the carrier of L
[(c₁₆ * ra),x] is non empty set
{(c₁₆ * ra),x} is non empty set
{(c₁₆ * ra)} is non empty trivial V36(1) set
{{(c₁₆ * ra),x},{(c₁₆ * ra)}} is non empty set
the multF of L . [(c₁₆ * ra),x] is set
c₁₆ * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (c₁₆,y) is left_complementable right_complementable complementable Element of the carrier of L
[c₁₆,y] is non empty set
{c₁₆,y} is non empty set
{{c₁₆,y},{c₁₆}} is non empty set
the multF of L . [c₁₆,y] is set
ra * (c₁₆ * y) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . (ra,(c₁₆ * y)) is left_complementable right_complementable complementable Element of the carrier of L
[ra,(c₁₆ * y)] is non empty set
{ra,(c₁₆ * y)} is non empty set
{ra} is non empty trivial V36(1) set
{{ra,(c₁₆ * y)},{ra}} is non empty set
the multF of L . [ra,(c₁₆ * y)] is set
(c₁₆ * ra) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((c₁₆ * ra),y) is left_complementable right_complementable complementable Element of the carrier of L
[(c₁₆ * ra),y] is non empty set
{(c₁₆ * ra),y} is non empty set
{{(c₁₆ * ra),y},{(c₁₆ * ra)}} is non empty set
the multF of L . [(c₁₆ * ra),y] is set
(L) . ((1. L),y) is left_complementable right_complementable complementable Element of H₁(L)
[(1. L),y] is non empty set
{(1. L),y} is non empty set
{{(1. L),y},{(1. L)}} is non empty set
(L) . [(1. L),y] is set
(1. L) * y is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . ((1. L),y) is left_complementable right_complementable complementable Element of the carrier of L
the multF of L . [(1. L),y] is set
L is non empty non degenerated non trivial doubleLoopStr
the carrier of L is non empty non trivial set
x is Element of the carrier of L
x is Element of the carrier of L
x * x is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
x * x is Element of the carrier of L
the multF of L . (x,x) is Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
x is Element of the carrier of L
x is Element of the carrier of L
x * x is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,x) is Element of the carrier of L
[x,x] is non empty set
{x,x} is non empty set
{x} is non empty trivial V36(1) set
{{x,x},{x}} is non empty set
the multF of L . [x,x] is set
y is Element of the carrier of L
(x * x) * y is Element of the carrier of L
the multF of L . ((x * x),y) is Element of the carrier of L
[(x * x),y] is non empty set
{(x * x),y} is non empty set
{(x * x)} is non empty trivial V36(1) set
{{(x * x),y},{(x * x)}} is non empty set
the multF of L . [(x * x),y] is set
x * y is Element of the carrier of L
the multF of L . (x,y) is Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
x * (x * y) is Element of the carrier of L
the multF of L . (x,(x * y)) is Element of the carrier of L
[x,(x * y)] is non empty set
{x,(x * y)} is non empty set
{{x,(x * y)},{x}} is non empty set
the multF of L . [x,(x * y)] is set
1. L is V48(L) Element of the carrier of L
the OneF of L is Element of the carrier of L
x is Element of the carrier of L
x * (1. L) is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,(1. L)) is Element of the carrier of L
[x,(1. L)] is non empty set
{x,(1. L)} is non empty set
{x} is non empty trivial V36(1) set
{{x,(1. L)},{x}} is non empty set
the multF of L . [x,(1. L)] is set
x is Element of the carrier of L
(1. L) * x is Element of the carrier of L
the multF of L . ((1. L),x) is Element of the carrier of L
[(1. L),x] is non empty set
{(1. L),x} is non empty set
{(1. L)} is non empty trivial V36(1) set
{{(1. L),x},{(1. L)}} is non empty set
the multF of L . [(1. L),x] is set
x is Element of the carrier of L
0. L is V48(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
{(0. L)} is non empty trivial V36(1) Element of bool the carrier of L
bool the carrier of L is non empty set
NonZero L is non empty Element of bool the carrier of L
[#] L is non empty non proper Element of bool the carrier of L
{(0. L)} is non empty trivial V36(1) set
([#] L) \ {(0. L)} is Element of bool the carrier of L
x is Element of NonZero L
y is Element of NonZero L
x * y is Element of the carrier of L
the multF of L is Relation-like [: the carrier of L, the carrier of L:] -defined the carrier of L -valued Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the multF of L . (x,y) is Element of the carrier of L
[x,y] is non empty set
{x,y} is non empty set
{x} is non empty trivial V36(1) set
{{x,y},{x}} is non empty set
the multF of L . [x,y] is set
y * x is Element of the carrier of L
the multF of L . (y,x) is Element of the carrier of L
[y,x] is non empty set
{y,x} is non empty set
{y} is non empty trivial V36(1) set
{{y,x},{y}} is non empty set
the multF of L . [y,x] is set
y * x is Element of the carrier of L
the multF of L . (y,x) is Element of the carrier of L
[y,x] is non empty set
{y,x} is non empty set
{{y,x},{y}} is non empty set
the multF of L . [y,x] is set