:: 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