:: REALSET3 semantic presentation

K97() is Element of bool K93()
K93() is set
bool K93() is set
K92() is set
bool K92() is set
bool K97() is set
2 is V11() set
[:2,2:] is set
[:[:2,2:],2:] is set
bool [:[:2,2:],2:] is set
K14() is set
1 is V11() set

revf F is V1() V4( NonZero F) V5( NonZero F) Function-like V18( NonZero F, NonZero F) Element of bool [:(),():]
NonZero F is V11() Element of bool the carrier of F
the carrier of F is V11() non trivial set
bool the carrier of F is set
[#] F is V11() non proper Element of bool the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is set
K29( the carrier of F,([#] F),{(0. F)}) is Element of bool the carrier of F
[:(),():] is set
bool [:(),():] is set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
(revf F) . (1. F) is set
(1. F) * (1. F) is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the multF of F . ((1. F),(1. F)) is Element of the carrier of F
[(1. F),(1. F)] is set
the multF of F . [(1. F),(1. F)] is set

the carrier of F is V11() non trivial set
NonZero F is V11() Element of bool the carrier of F
bool the carrier of F is set
[#] F is V11() non proper Element of bool the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is set
K29( the carrier of F,([#] F),{(0. F)}) is Element of bool the carrier of F
revf F is V1() V4( NonZero F) V5( NonZero F) Function-like V18( NonZero F, NonZero F) Element of bool [:(),():]
[:(),():] is set
bool [:(),():] is set
omf F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) M10( the carrier of F, 0. F)
[: the carrier of F, the carrier of F:] is set
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
a is Element of NonZero F
b is Element of NonZero F
(revf F) . b is Element of NonZero F
(omf F) . (a,((revf F) . b)) is set
[a,((revf F) . b)] is set
(omf F) . [a,((revf F) . b)] is set
(revf F) . ((omf F) . (a,((revf F) . b))) is set
(revf F) . a is Element of NonZero F
(omf F) . (b,((revf F) . a)) is set
[b,((revf F) . a)] is set
(omf F) . [b,((revf F) . a)] is set
revfb is Element of NonZero F
c is Element of NonZero F
b * c is Element of the carrier of F
the multF of F . (b,c) is Element of the carrier of F
[b,c] is set
the multF of F . [b,c] is set
revfb * (b * c) is Element of the carrier of F
the multF of F . (revfb,(b * c)) is Element of the carrier of F
[revfb,(b * c)] is set
the multF of F . [revfb,(b * c)] is set
b * revfb is Element of the carrier of F
the multF of F . (b,revfb) is Element of the carrier of F
[b,revfb] is set
the multF of F . [b,revfb] is set
c * (b * revfb) is Element of the carrier of F
the multF of F . (c,(b * revfb)) is Element of the carrier of F
[c,(b * revfb)] is set
the multF of F . [c,(b * revfb)] is set
(omf F) . (b,revfb) is Element of the carrier of F
(omf F) . [b,revfb] is set
c * ((omf F) . (b,revfb)) is Element of the carrier of F
the multF of F . (c,((omf F) . (b,revfb))) is Element of the carrier of F
[c,((omf F) . (b,revfb))] is set
the multF of F . [c,((omf F) . (b,revfb))] is set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
c * (1. F) is Element of the carrier of F
the multF of F . (c,(1. F)) is Element of the carrier of F
[c,(1. F)] is set
the multF of F . [c,(1. F)] is set
a * revfb is Element of the carrier of F
the multF of F . (a,revfb) is Element of the carrier of F
[a,revfb] is set
the multF of F . [a,revfb] is set
(a * revfb) * (b * c) is Element of the carrier of F
the multF of F . ((a * revfb),(b * c)) is Element of the carrier of F
[(a * revfb),(b * c)] is set
the multF of F . [(a * revfb),(b * c)] is set
a * c is Element of the carrier of F
the multF of F . (a,c) is Element of the carrier of F
[a,c] is set
the multF of F . [a,c] is set
(omf F) . (a,c) is Element of the carrier of F
(omf F) . [a,c] is set

the carrier of F is V11() non trivial set
NonZero F is V11() Element of bool the carrier of F
bool the carrier of F is set
[#] F is V11() non proper Element of bool the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is set
K29( the carrier of F,([#] F),{(0. F)}) is Element of bool the carrier of F
revf F is V1() V4( NonZero F) V5( NonZero F) Function-like V18( NonZero F, NonZero F) Element of bool [:(),():]
[:(),():] is set
bool [:(),():] is set
omf F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) M10( the carrier of F, 0. F)
[: the carrier of F, the carrier of F:] is set
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
a is Element of NonZero F
b is Element of NonZero F
(omf F) . (a,b) is Element of the carrier of F
[a,b] is set
(omf F) . [a,b] is set
(revf F) . ((omf F) . (a,b)) is set
(revf F) . a is Element of NonZero F
(revf F) . b is Element of NonZero F
(omf F) . (((revf F) . a),((revf F) . b)) is set
[((revf F) . a),((revf F) . b)] is set
(omf F) . [((revf F) . a),((revf F) . b)] is set
(revf F) . ((revf F) . b) is Element of NonZero F
(omf F) . (a,((revf F) . ((revf F) . b))) is set
[a,((revf F) . ((revf F) . b))] is set
(omf F) . [a,((revf F) . ((revf F) . b))] is set
(revf F) . ((omf F) . (a,((revf F) . ((revf F) . b)))) is set
revfb is Element of NonZero F
c is Element of NonZero F
revfb * c is Element of the carrier of F
the multF of F . (revfb,c) is Element of the carrier of F
[revfb,c] is set
the multF of F . [revfb,c] is set
c * revfb is Element of the carrier of F
the multF of F . (c,revfb) is Element of the carrier of F
[c,revfb] is set
the multF of F . [c,revfb] is set

the carrier of F is V11() non trivial set
a is Element of the carrier of F
b is Element of the carrier of F
a - b is Element of the carrier of F
- b is Element of the carrier of F
a + (- b) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the addF of F . (a,(- b)) is Element of the carrier of F
[a,(- b)] is set
the addF of F . [a,(- b)] is set
c is Element of the carrier of F
revfb is Element of the carrier of F
c - revfb is Element of the carrier of F
- revfb is Element of the carrier of F
c + (- revfb) is Element of the carrier of F
the addF of F . (c,(- revfb)) is Element of the carrier of F
[c,(- revfb)] is set
the addF of F . [c,(- revfb)] is set
a + revfb is Element of the carrier of F
the addF of F . (a,revfb) is Element of the carrier of F
[a,revfb] is set
the addF of F . [a,revfb] is set
b + c is Element of the carrier of F
the addF of F . (b,c) is Element of the carrier of F
[b,c] is set
the addF of F . [b,c] is set
(c - revfb) + b is Element of the carrier of F
the addF of F . ((c - revfb),b) is Element of the carrier of F
[(c - revfb),b] is set
the addF of F . [(c - revfb),b] is set
a + (- b) is Element of the carrier of F
(a + (- b)) + b is Element of the carrier of F
the addF of F . ((a + (- b)),b) is Element of the carrier of F
[(a + (- b)),b] is set
the addF of F . [(a + (- b)),b] is set
b - b is Element of the carrier of F
b + (- b) is Element of the carrier of F
the addF of F . (b,(- b)) is Element of the carrier of F
[b,(- b)] is set
the addF of F . [b,(- b)] is set
a + (b - b) is Element of the carrier of F
the addF of F . (a,(b - b)) is Element of the carrier of F
[a,(b - b)] is set
the addF of F . [a,(b - b)] is set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
a + (0. F) is Element of the carrier of F
the addF of F . (a,(0. F)) is Element of the carrier of F
[a,(0. F)] is set
the addF of F . [a,(0. F)] is set
c + b is Element of the carrier of F
the addF of F . (c,b) is Element of the carrier of F
[c,b] is set
the addF of F . [c,b] is set
(c + b) + (- revfb) is Element of the carrier of F
the addF of F . ((c + b),(- revfb)) is Element of the carrier of F
[(c + b),(- revfb)] is set
the addF of F . [(c + b),(- revfb)] is set
((c + b) + (- revfb)) + revfb is Element of the carrier of F
the addF of F . (((c + b) + (- revfb)),revfb) is Element of the carrier of F
[((c + b) + (- revfb)),revfb] is set
the addF of F . [((c + b) + (- revfb)),revfb] is set
revfb - revfb is Element of the carrier of F
revfb + (- revfb) is Element of the carrier of F
the addF of F . (revfb,(- revfb)) is Element of the carrier of F
[revfb,(- revfb)] is set
the addF of F . [revfb,(- revfb)] is set
(c + b) + (revfb - revfb) is Element of the carrier of F
the addF of F . ((c + b),(revfb - revfb)) is Element of the carrier of F
[(c + b),(revfb - revfb)] is set
the addF of F . [(c + b),(revfb - revfb)] is set
(c + b) + (0. F) is Element of the carrier of F
the addF of F . ((c + b),(0. F)) is Element of the carrier of F
[(c + b),(0. F)] is set
the addF of F . [(c + b),(0. F)] is set
(b + c) - revfb is Element of the carrier of F
(b + c) + (- revfb) is Element of the carrier of F
the addF of F . ((b + c),(- revfb)) is Element of the carrier of F
[(b + c),(- revfb)] is set
the addF of F . [(b + c),(- revfb)] is set
a + (revfb - revfb) is Element of the carrier of F
the addF of F . (a,(revfb - revfb)) is Element of the carrier of F
[a,(revfb - revfb)] is set
the addF of F . [a,(revfb - revfb)] is set
((c - revfb) + b) - b is Element of the carrier of F
((c - revfb) + b) + (- b) is Element of the carrier of F
the addF of F . (((c - revfb) + b),(- b)) is Element of the carrier of F
[((c - revfb) + b),(- b)] is set
the addF of F . [((c - revfb) + b),(- b)] is set
(c - revfb) + (b - b) is Element of the carrier of F
the addF of F . ((c - revfb),(b - b)) is Element of the carrier of F
[(c - revfb),(b - b)] is set
the addF of F . [(c - revfb),(b - b)] is set
(c - revfb) + (0. F) is Element of the carrier of F
the addF of F . ((c - revfb),(0. F)) is Element of the carrier of F
[(c - revfb),(0. F)] is set
the addF of F . [(c - revfb),(0. F)] is set

the carrier of F is V11() non trivial set
NonZero F is V11() Element of bool the carrier of F
bool the carrier of F is set
[#] F is V11() non proper Element of bool the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is set
K29( the carrier of F,([#] F),{(0. F)}) is Element of bool the carrier of F
omf F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) M10( the carrier of F, 0. F)
[: the carrier of F, the carrier of F:] is set
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
revf F is V1() V4( NonZero F) V5( NonZero F) Function-like V18( NonZero F, NonZero F) Element of bool [:(),():]
[:(),():] is set
bool [:(),():] is set
a is Element of the carrier of F
b is Element of the carrier of F
c is Element of NonZero F
(revf F) . c is Element of NonZero F
(omf F) . (a,((revf F) . c)) is set
[a,((revf F) . c)] is set
(omf F) . [a,((revf F) . c)] is set
revfb is Element of NonZero F
(revf F) . revfb is Element of NonZero F
(omf F) . (b,((revf F) . revfb)) is set
[b,((revf F) . revfb)] is set
(omf F) . [b,((revf F) . revfb)] is set
(omf F) . (a,revfb) is Element of the carrier of F
[a,revfb] is set
(omf F) . [a,revfb] is set
(omf F) . (c,b) is Element of the carrier of F
[c,b] is set
(omf F) . [c,b] is set
revfc is Element of NonZero F
b * revfc is Element of the carrier of F
the multF of F . (b,revfc) is Element of the carrier of F
[b,revfc] is set
the multF of F . [b,revfc] is set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
b * (1. F) is Element of the carrier of F
the multF of F . (b,(1. F)) is Element of the carrier of F
[b,(1. F)] is set
the multF of F . [b,(1. F)] is set
revfb * revfc is Element of the carrier of F
the multF of F . (revfb,revfc) is Element of the carrier of F
[revfb,revfc] is set
the multF of F . [revfb,revfc] is set
(omf F) . (b,(revfb * revfc)) is Element of the carrier of F
[b,(revfb * revfc)] is set
(omf F) . [b,(revfb * revfc)] is set
revfc * revfb is Element of the carrier of F
the multF of F . (revfc,revfb) is Element of the carrier of F
[revfc,revfb] is set
the multF of F . [revfc,revfb] is set
b * (revfc * revfb) is Element of the carrier of F
the multF of F . (b,(revfc * revfb)) is Element of the carrier of F
[b,(revfc * revfb)] is set
the multF of F . [b,(revfc * revfb)] is set
(b * revfc) * revfb is Element of the carrier of F
the multF of F . ((b * revfc),revfb) is Element of the carrier of F
[(b * revfc),revfb] is set
the multF of F . [(b * revfc),revfb] is set
a * (1. F) is Element of the carrier of F
the multF of F . (a,(1. F)) is Element of the carrier of F
[a,(1. F)] is set
the multF of F . [a,(1. F)] is set
revfc is Element of NonZero F
c * revfc is Element of the carrier of F
the multF of F . (c,revfc) is Element of the carrier of F
[c,revfc] is set
the multF of F . [c,revfc] is set
(omf F) . (a,(c * revfc)) is Element of the carrier of F
[a,(c * revfc)] is set
(omf F) . [a,(c * revfc)] is set
revfc * c is Element of the carrier of F
the multF of F . (revfc,c) is Element of the carrier of F
[revfc,c] is set
the multF of F . [revfc,c] is set
a * (revfc * c) is Element of the carrier of F
the multF of F . (a,(revfc * c)) is Element of the carrier of F
[a,(revfc * c)] is set
the multF of F . [a,(revfc * c)] is set
a * revfc is Element of the carrier of F
the multF of F . (a,revfc) is Element of the carrier of F
[a,revfc] is set
the multF of F . [a,revfc] is set
(a * revfc) * c is Element of the carrier of F
the multF of F . ((a * revfc),c) is Element of the carrier of F
[(a * revfc),c] is set
the multF of F . [(a * revfc),c] is set
revfd is Element of the carrier of F
c * revfd is Element of the carrier of F
the multF of F . (c,revfd) is Element of the carrier of F
[c,revfd] is set
the multF of F . [c,revfd] is set
(omf F) . (c,((omf F) . (b,((revf F) . revfb)))) is set
[c,((omf F) . (b,((revf F) . revfb)))] is set
(omf F) . [c,((omf F) . (b,((revf F) . revfb)))] is set
c * (b * revfc) is Element of the carrier of F
the multF of F . (c,(b * revfc)) is Element of the carrier of F
[c,(b * revfc)] is set
the multF of F . [c,(b * revfc)] is set
(c * (b * revfc)) * revfb is Element of the carrier of F
the multF of F . ((c * (b * revfc)),revfb) is Element of the carrier of F
[(c * (b * revfc)),revfb] is set
the multF of F . [(c * (b * revfc)),revfb] is set
c * ((b * revfc) * revfb) is Element of the carrier of F
the multF of F . (c,((b * revfc) * revfb)) is Element of the carrier of F
[c,((b * revfc) * revfb)] is set
the multF of F . [c,((b * revfc) * revfb)] is set
revfc is Element of NonZero F
(omf F) . (b,revfc) is Element of the carrier of F
[b,revfc] is set
(omf F) . [b,revfc] is set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
a * (1. F) is Element of the carrier of F
the multF of F . (a,(1. F)) is Element of the carrier of F
[a,(1. F)] is set
the multF of F . [a,(1. F)] is set
(omf F) . (a,(1. F)) is Element of the carrier of F
(omf F) . [a,(1. F)] is set
revfb * revfc is Element of the carrier of F
the multF of F . (revfb,revfc) is Element of the carrier of F
[revfb,revfc] is set
the multF of F . [revfb,revfc] is set
a * (revfb * revfc) is Element of the carrier of F
the multF of F . (a,(revfb * revfc)) is Element of the carrier of F
[a,(revfb * revfc)] is set
the multF of F . [a,(revfb * revfc)] is set
a * revfb is Element of the carrier of F
the multF of F . (a,revfb) is Element of the carrier of F
the multF of F . [a,revfb] is set
(a * revfb) * revfc is Element of the carrier of F
the multF of F . ((a * revfb),revfc) is Element of the carrier of F
[(a * revfb),revfc] is set
the multF of F . [(a * revfb),revfc] is set
c * b is Element of the carrier of F
the multF of F . (c,b) is Element of the carrier of F
the multF of F . [c,b] is set
(c * b) * revfc is Element of the carrier of F
the multF of F . ((c * b),revfc) is Element of the carrier of F
[(c * b),revfc] is set
the multF of F . [(c * b),revfc] is set
b * revfc is Element of the carrier of F
the multF of F . (b,revfc) is Element of the carrier of F
the multF of F . [b,revfc] is set
c * (b * revfc) is Element of the carrier of F
the multF of F . (c,(b * revfc)) is Element of the carrier of F
[c,(b * revfc)] is set
the multF of F . [c,(b * revfc)] is set
revfd is Element of the carrier of F
revfd * c is Element of the carrier of F
the multF of F . (revfd,c) is Element of the carrier of F
[revfd,c] is set
the multF of F . [revfd,c] is set
revfc is Element of NonZero F
(revfd * c) * revfc is Element of the carrier of F
the multF of F . ((revfd * c),revfc) is Element of the carrier of F
[(revfd * c),revfc] is set
the multF of F . [(revfd * c),revfc] is set
c * revfc is Element of the carrier of F
the multF of F . (c,revfc) is Element of the carrier of F
[c,revfc] is set
the multF of F . [c,revfc] is set
revfd * (c * revfc) is Element of the carrier of F
the multF of F . (revfd,(c * revfc)) is Element of the carrier of F
[revfd,(c * revfc)] is set
the multF of F . [revfd,(c * revfc)] is set
((omf F) . (b,revfc)) * (1. F) is Element of the carrier of F
the multF of F . (((omf F) . (b,revfc)),(1. F)) is Element of the carrier of F
[((omf F) . (b,revfc)),(1. F)] is set
the multF of F . [((omf F) . (b,revfc)),(1. F)] is set

the carrier of F is V11() non trivial set
NonZero F is V11() Element of bool the carrier of F
bool the carrier of F is set
[#] F is V11() non proper Element of bool the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is set
K29( the carrier of F,([#] F),{(0. F)}) is Element of bool the carrier of F
omf F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) M10( the carrier of F, 0. F)
[: the carrier of F, the carrier of F:] is set
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
revf F is V1() V4( NonZero F) V5( NonZero F) Function-like V18( NonZero F, NonZero F) Element of bool [:(),():]
[:(),():] is set
bool [:(),():] is set
a is Element of the carrier of F
b is Element of the carrier of F
(omf F) . (a,b) is Element of the carrier of F
[a,b] is set
(omf F) . [a,b] is set
c is Element of NonZero F
(revf F) . c is Element of NonZero F
(omf F) . (a,((revf F) . c)) is set
[a,((revf F) . c)] is set
(omf F) . [a,((revf F) . c)] is set
revfb is Element of NonZero F
(revf F) . revfb is Element of NonZero F
(omf F) . (b,((revf F) . revfb)) is set
[b,((revf F) . revfb)] is set
(omf F) . [b,((revf F) . revfb)] is set
(omf F) . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . revfb)))) is set
[((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . revfb)))] is set
(omf F) . [((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . revfb)))] is set
(omf F) . (c,revfb) is Element of the carrier of F
[c,revfb] is set
(omf F) . [c,revfb] is set
(revf F) . ((omf F) . (c,revfb)) is set
(omf F) . (((omf F) . (a,b)),((revf F) . ((omf F) . (c,revfb)))) is set
[((omf F) . (a,b)),((revf F) . ((omf F) . (c,revfb)))] is set
(omf F) . [((omf F) . (a,b)),((revf F) . ((omf F) . (c,revfb)))] is set
c * revfb is Element of the carrier of F
the multF of F . (c,revfb) is Element of the carrier of F
the multF of F . [c,revfb] is set
(revf F) . (c * revfb) is set
revfc is Element of NonZero F
a * revfc is Element of the carrier of F
the multF of F . (a,revfc) is Element of the carrier of F
[a,revfc] is set
the multF of F . [a,revfc] is set
revfc is Element of NonZero F
b * revfc is Element of the carrier of F
the multF of F . (b,revfc) is Element of the carrier of F
[b,revfc] is set
the multF of F . [b,revfc] is set
(a * revfc) * (b * revfc) is Element of the carrier of F
the multF of F . ((a * revfc),(b * revfc)) is Element of the carrier of F
[(a * revfc),(b * revfc)] is set
the multF of F . [(a * revfc),(b * revfc)] is set
revfc * (b * revfc) is Element of the carrier of F
the multF of F . (revfc,(b * revfc)) is Element of the carrier of F
[revfc,(b * revfc)] is set
the multF of F . [revfc,(b * revfc)] is set
a * (revfc * (b * revfc)) is Element of the carrier of F
the multF of F . (a,(revfc * (b * revfc))) is Element of the carrier of F
[a,(revfc * (b * revfc))] is set
the multF of F . [a,(revfc * (b * revfc))] is set
revfc * revfc is Element of the carrier of F
the multF of F . (revfc,revfc) is Element of the carrier of F
[revfc,revfc] is set
the multF of F . [revfc,revfc] is set
b * (revfc * revfc) is Element of the carrier of F
the multF of F . (b,(revfc * revfc)) is Element of the carrier of F
[b,(revfc * revfc)] is set
the multF of F . [b,(revfc * revfc)] is set
a * (b * (revfc * revfc)) is Element of the carrier of F
the multF of F . (a,(b * (revfc * revfc))) is Element of the carrier of F
[a,(b * (revfc * revfc))] is set
the multF of F . [a,(b * (revfc * revfc))] is set
(omf F) . (b,((revf F) . ((omf F) . (c,revfb)))) is set
[b,((revf F) . ((omf F) . (c,revfb)))] is set
(omf F) . [b,((revf F) . ((omf F) . (c,revfb)))] is set
(omf F) . (a,((omf F) . (b,((revf F) . ((omf F) . (c,revfb)))))) is set
[a,((omf F) . (b,((revf F) . ((omf F) . (c,revfb)))))] is set
(omf F) . [a,((omf F) . (b,((revf F) . ((omf F) . (c,revfb)))))] is set
revfd is Element of the carrier of F
b * revfd is Element of the carrier of F
the multF of F . (b,revfd) is Element of the carrier of F
[b,revfd] is set
the multF of F . [b,revfd] is set
a * (b * revfd) is Element of the carrier of F
the multF of F . (a,(b * revfd)) is Element of the carrier of F
[a,(b * revfd)] is set
the multF of F . [a,(b * revfd)] is set
a * b is Element of the carrier of F
the multF of F . (a,b) is Element of the carrier of F
the multF of F . [a,b] is set
(a * b) * revfd is Element of the carrier of F
the multF of F . ((a * b),revfd) is Element of the carrier of F
[(a * b),revfd] is set
the multF of F . [(a * b),revfd] is set

the carrier of F is V11() non trivial set
NonZero F is V11() Element of bool the carrier of F
bool the carrier of F is set
[#] F is V11() non proper Element of bool the carrier of F
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
{(0. F)} is set
K29( the carrier of F,([#] F),{(0. F)}) is Element of bool the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
omf F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) M10( the carrier of F, 0. F)
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
revf F is V1() V4( NonZero F) V5( NonZero F) Function-like V18( NonZero F, NonZero F) Element of bool [:(),():]
[:(),():] is set
bool [:(),():] is set
a is Element of the carrier of F
b is Element of the carrier of F
c is Element of NonZero F
(revf F) . c is Element of NonZero F
(omf F) . (a,((revf F) . c)) is set
[a,((revf F) . c)] is set
(omf F) . [a,((revf F) . c)] is set
revfb is Element of NonZero F
(revf F) . revfb is Element of NonZero F
(omf F) . (b,((revf F) . revfb)) is set
[b,((revf F) . revfb)] is set
(omf F) . [b,((revf F) . revfb)] is set
the addF of F . (((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . revfb)))) is set
[((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . revfb)))] is set
the addF of F . [((omf F) . (a,((revf F) . c))),((omf F) . (b,((revf F) . revfb)))] is set
(omf F) . (a,revfb) is Element of the carrier of F
[a,revfb] is set
(omf F) . [a,revfb] is set
(omf F) . (b,c) is Element of the carrier of F
[b,c] is set
(omf F) . [b,c] is set
the addF of F . (((omf F) . (a,revfb)),((omf F) . (b,c))) is Element of the carrier of F
[((omf F) . (a,revfb)),((omf F) . (b,c))] is set
the addF of F . [((omf F) . (a,revfb)),((omf F) . (b,c))] is set
(omf F) . (c,revfb) is Element of the carrier of F
[c,revfb] is set
(omf F) . [c,revfb] is set
(revf F) . ((omf F) . (c,revfb)) is set
(omf F) . (( the addF of F . (((omf F) . (a,revfb)),((omf F) . (b,c)))),((revf F) . ((omf F) . (c,revfb)))) is set
[( the addF of F . (((omf F) . (a,revfb)),((omf F) . (b,c)))),((revf F) . ((omf F) . (c,revfb)))] is set
(omf F) . [( the addF of F . (((omf F) . (a,revfb)),((omf F) . (b,c)))),((revf F) . ((omf F) . (c,revfb)))] is set
1. F is V51(F) Element of the carrier of F
the OneF of F is Element of the carrier of F
a * (1. F) is Element of the carrier of F
the multF of F . (a,(1. F)) is Element of the carrier of F
[a,(1. F)] is set
the multF of F . [a,(1. F)] is set
(omf F) . (a,(1. F)) is Element of the carrier of F
(omf F) . [a,(1. F)] is set
revfc is Element of the carrier of F
revfb * revfc is Element of the carrier of F
the multF of F . (revfb,revfc) is Element of the carrier of F
[revfb,revfc] is set
the multF of F . [revfb,revfc] is set
a * (revfb * revfc) is Element of the carrier of F
the multF of F . (a,(revfb * revfc)) is Element of the carrier of F
[a,(revfb * revfc)] is set
the multF of F . [a,(revfb * revfc)] is set
a * revfb is Element of the carrier of F
the multF of F . (a,revfb) is Element of the carrier of F
the multF of F . [a,revfb] is set
(a * revfb) * revfc is Element of the carrier of F
the multF of F . ((a * revfb),revfc) is Element of the carrier of F
[(a * revfb),revfc] is set
the multF of F . [(a * revfb),revfc] is set
c * revfb is Element of the carrier of F
the multF of F . (c,revfb) is Element of the carrier of F
the multF of F . [c,revfb] is set
(revf F) . (c * revfb) is set
b * (1. F) is Element of the carrier of F
the multF of F . (b,(1. F)) is Element of the carrier of F
[b,(1. F)] is set
the multF of F . [b,(1. F)] is set
(omf F) . (b,(1. F)) is Element of the carrier of F
(omf F) . [b,(1. F)] is set
revfc is Element of NonZero F
c * revfc is Element of the carrier of F
the multF of F . (c,revfc) is Element of the carrier of F
[c,revfc] is set
the multF of F . [c,revfc] is set
b * (c * revfc) is Element of the carrier of F
the multF of F . (b,(c * revfc)) is Element of the carrier of F
[b,(c * revfc)] is set
the multF of F . [b,(c * revfc)] is set
b * c is Element of the carrier of F
the multF of F . (b,c) is Element of the carrier of F
the multF of F . [b,c] is set
(b * c) * revfc is Element of the carrier of F
the multF of F . ((b * c),revfc) is Element of the carrier of F
[(b * c),revfc] is set
the multF of F . [(b * c),revfc] is set
revfd is Element of NonZero F
((b * c) * revfc) * revfd is Element of the carrier of F
the multF of F . (((b * c) * revfc),revfd) is Element of the carrier of F
[((b * c) * revfc),revfd] is set
the multF of F . [((b * c) * revfc),revfd] is set
revfc * revfd is Element of the carrier of F
the multF of F . (revfc,revfd) is Element of the carrier of F
[revfc,revfd] is set
the multF of F . [revfc,revfd] is set
(b * c) * (revfc * revfd) is Element of the carrier of F
the multF of F . ((b * c),(revfc * revfd)) is Element of the carrier of F
[(b * c),(revfc * revfd)] is set
the multF of F . [(b * c),(revfc * revfd)] is set
(omf F) . (((omf F) . (b,c)),((revf F) . ((omf F) . (c,revfb)))) is set
[((omf F) . (b,c)),((revf F) . ((omf F) . (c,revfb)))] is set
(omf F) . [((omf F) . (b,c)),((revf F) . ((omf F) . (c,revfb)))] is set
(a * revfb) * revfd is Element of the carrier of F
the multF of F . ((a * revfb),revfd) is Element of the carrier of F
[(a * revfb),revfd] is set
the multF of F . [(a * revfb),revfd] is set
((a * revfb) * revfd) * revfc is Element of the carrier of F
the multF of F . (((a * revfb) * revfd),revfc) is Element of the carrier of F
[((a * revfb) * revfd),revfc] is set
the multF of F . [((a * revfb) * revfd),revfc] is set
revfd * revfc is Element of the carrier of F
the multF of F . (revfd,revfc) is Element of the carrier of F
[revfd,revfc] is set
the multF of F . [revfd,revfc] is set
(a * revfb) * (revfd * revfc) is Element of the carrier of F
the multF of F . ((a * revfb),(revfd * revfc)) is Element of the carrier of F
[(a * revfb),(revfd * revfc)] is set
the multF of F . [(a * revfb),(revfd * revfc)] is set
(omf F) . (((omf F) . (a,revfb)),(revfc * revfd)) is Element of the carrier of F
[((omf F) . (a,revfb)),(revfc * revfd)] is set
(omf F) . [((omf F) . (a,revfb)),(revfc * revfd)] is set
(omf F) . (((omf F) . (a,revfb)),((revf F) . ((omf F) . (c,revfb)))) is set
[((omf F) . (a,revfb)),((revf F) . ((omf F) . (c,revfb)))] is set
(omf F) . [((omf F) . (a,revfb)),((revf F) . ((omf F) . (c,revfb)))] is set
revfcd is Element of the carrier of F
(a * revfb) * revfcd is Element of the carrier of F
the multF of F . ((a * revfb),revfcd) is Element of the carrier of F
[(a * revfb),revfcd] is set
the multF of F . [(a * revfb),revfcd] is set
(b * c) * revfcd is Element of the carrier of F
the multF of F . ((b * c),revfcd) is Element of the carrier of F
[(b * c),revfcd] is set
the multF of F . [(b * c),revfcd] is set
((a * revfb) * revfcd) + ((b * c) * revfcd) is Element of the carrier of F
the addF of F . (((a * revfb) * revfcd),((b * c) * revfcd)) is Element of the carrier of F
[((a * revfb) * revfcd),((b * c) * revfcd)] is set
the addF of F . [((a * revfb) * revfcd),((b * c) * revfcd)] is set
(a * revfb) + (b * c) is Element of the carrier of F
the addF of F . ((a * revfb),(b * c)) is Element of the carrier of F
[(a * revfb),(b * c)] is set
the addF of F . [(a * revfb),(b * c)] is set
((a * revfb) + (b * c)) * revfcd is Element of the carrier of F
the multF of F . (((a * revfb) + (b * c)),revfcd) is Element of the carrier of F
[((a * revfb) + (b * c)),revfcd] is set
the multF of F . [((a * revfb) + (b * c)),revfcd] is set

the carrier of F is V11() non trivial set
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
a is Element of the carrier of F
b is Element of the carrier of F
(comp F) . b is Element of the carrier of F
the addF of F . (a,((comp F) . b)) is Element of the carrier of F
[a,((comp F) . b)] is set
the addF of F . [a,((comp F) . b)] is set
a is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
a is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
b is Element of the carrier of F
c is Element of the carrier of F
a . (b,c) is Element of the carrier of F
[b,c] is set
a . [b,c] is set
(comp F) . c is Element of the carrier of F
the addF of F . (b,((comp F) . c)) is Element of the carrier of F
[b,((comp F) . c)] is set
the addF of F . [b,((comp F) . c)] is set
a is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
b is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
c is set
revfb is set
revfc is set
[revfb,revfc] is set
a . c is set
a . (revfb,revfc) is set
a . [revfb,revfc] is set
(comp F) . revfc is set
the addF of F . (revfb,((comp F) . revfc)) is set
[revfb,((comp F) . revfc)] is set
the addF of F . [revfb,((comp F) . revfc)] is set
b . (revfb,revfc) is set
b . [revfb,revfc] is set
b . c is set

the carrier of F is V11() non trivial set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
a is Element of the carrier of F
(F) . (a,a) is Element of the carrier of F
[a,a] is set
(F) . [a,a] is set
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
(comp F) . a is Element of the carrier of F
the addF of F . (a,((comp F) . a)) is Element of the carrier of F
[a,((comp F) . a)] is set
the addF of F . [a,((comp F) . a)] is set
a - a is Element of the carrier of F
- a is Element of the carrier of F
a + (- a) is Element of the carrier of F
the addF of F . (a,(- a)) is Element of the carrier of F
[a,(- a)] is set
the addF of F . [a,(- a)] is set

the carrier of F is V11() non trivial set
omf F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) M10( the carrier of F, 0. F)
[: the carrier of F, the carrier of F:] is set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
a is Element of the carrier of F
b is Element of the carrier of F
c is Element of the carrier of F
(F) . (b,c) is Element of the carrier of F
[b,c] is set
(F) . [b,c] is set
(omf F) . (a,((F) . (b,c))) is Element of the carrier of F
[a,((F) . (b,c))] is set
(omf F) . [a,((F) . (b,c))] is set
(omf F) . (a,b) is Element of the carrier of F
[a,b] is set
(omf F) . [a,b] is set
(omf F) . (a,c) is Element of the carrier of F
[a,c] is set
(omf F) . [a,c] is set
(F) . (((omf F) . (a,b)),((omf F) . (a,c))) is Element of the carrier of F
[((omf F) . (a,b)),((omf F) . (a,c))] is set
(F) . [((omf F) . (a,b)),((omf F) . (a,c))] is set
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
(comp F) . c is Element of the carrier of F
the addF of F . (b,((comp F) . c)) is Element of the carrier of F
[b,((comp F) . c)] is set
the addF of F . [b,((comp F) . c)] is set
(omf F) . (a,( the addF of F . (b,((comp F) . c)))) is Element of the carrier of F
[a,( the addF of F . (b,((comp F) . c)))] is set
(omf F) . [a,( the addF of F . (b,((comp F) . c)))] is set
b - c is Element of the carrier of F
- c is Element of the carrier of F
b + (- c) is Element of the carrier of F
the addF of F . (b,(- c)) is Element of the carrier of F
[b,(- c)] is set
the addF of F . [b,(- c)] is set
a * (b - c) is Element of the carrier of F
the multF of F . (a,(b - c)) is Element of the carrier of F
[a,(b - c)] is set
the multF of F . [a,(b - c)] is set
a * b is Element of the carrier of F
the multF of F . (a,b) is Element of the carrier of F
the multF of F . [a,b] is set
a * c is Element of the carrier of F
the multF of F . (a,c) is Element of the carrier of F
the multF of F . [a,c] is set
(a * b) - (a * c) is Element of the carrier of F
- (a * c) is Element of the carrier of F
(a * b) + (- (a * c)) is Element of the carrier of F
the addF of F . ((a * b),(- (a * c))) is Element of the carrier of F
[(a * b),(- (a * c))] is set
the addF of F . [(a * b),(- (a * c))] is set
(comp F) . (a * c) is Element of the carrier of F
the addF of F . (((omf F) . (a,b)),((comp F) . (a * c))) is Element of the carrier of F
[((omf F) . (a,b)),((comp F) . (a * c))] is set
the addF of F . [((omf F) . (a,b)),((comp F) . (a * c))] is set

the carrier of F is V11() non trivial set
omf F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) M10( the carrier of F, 0. F)
[: the carrier of F, the carrier of F:] is set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
the multF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
a is Element of the carrier of F
b is Element of the carrier of F
(F) . (a,b) is Element of the carrier of F
[a,b] is set
(F) . [a,b] is set
c is Element of the carrier of F
(omf F) . (((F) . (a,b)),c) is Element of the carrier of F
[((F) . (a,b)),c] is set
(omf F) . [((F) . (a,b)),c] is set
(omf F) . (a,c) is Element of the carrier of F
[a,c] is set
(omf F) . [a,c] is set
(omf F) . (b,c) is Element of the carrier of F
[b,c] is set
(omf F) . [b,c] is set
(F) . (((omf F) . (a,c)),((omf F) . (b,c))) is Element of the carrier of F
[((omf F) . (a,c)),((omf F) . (b,c))] is set
(F) . [((omf F) . (a,c)),((omf F) . (b,c))] is set
((F) . (a,b)) * c is Element of the carrier of F
the multF of F . (((F) . (a,b)),c) is Element of the carrier of F
the multF of F . [((F) . (a,b)),c] is set
c * ((F) . (a,b)) is Element of the carrier of F
the multF of F . (c,((F) . (a,b))) is Element of the carrier of F
[c,((F) . (a,b))] is set
the multF of F . [c,((F) . (a,b))] is set
(omf F) . (c,((F) . (a,b))) is Element of the carrier of F
(omf F) . [c,((F) . (a,b))] is set
c * a is Element of the carrier of F
the multF of F . (c,a) is Element of the carrier of F
[c,a] is set
the multF of F . [c,a] is set
c * b is Element of the carrier of F
the multF of F . (c,b) is Element of the carrier of F
[c,b] is set
the multF of F . [c,b] is set
(F) . ((c * a),(c * b)) is Element of the carrier of F
[(c * a),(c * b)] is set
(F) . [(c * a),(c * b)] is set
a * c is Element of the carrier of F
the multF of F . (a,c) is Element of the carrier of F
the multF of F . [a,c] is set
b * c is Element of the carrier of F
the multF of F . (b,c) is Element of the carrier of F
the multF of F . [b,c] is set
(F) . ((a * c),(b * c)) is Element of the carrier of F
[(a * c),(b * c)] is set
(F) . [(a * c),(b * c)] is set

the carrier of F is V11() non trivial set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
a is Element of the carrier of F
b is Element of the carrier of F
(F) . (a,b) is Element of the carrier of F
[a,b] is set
(F) . [a,b] is set
(F) . (b,a) is Element of the carrier of F
[b,a] is set
(F) . [b,a] is set
(comp F) . ((F) . (b,a)) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
(comp F) . b is Element of the carrier of F
the addF of F . (a,((comp F) . b)) is Element of the carrier of F
[a,((comp F) . b)] is set
the addF of F . [a,((comp F) . b)] is set
- b is Element of the carrier of F
a + (- b) is Element of the carrier of F
the addF of F . (a,(- b)) is Element of the carrier of F
[a,(- b)] is set
the addF of F . [a,(- b)] is set
b - a is Element of the carrier of F
- a is Element of the carrier of F
b + (- a) is Element of the carrier of F
the addF of F . (b,(- a)) is Element of the carrier of F
[b,(- a)] is set
the addF of F . [b,(- a)] is set
- (b - a) is Element of the carrier of F
b + (- a) is Element of the carrier of F
(comp F) . (b + (- a)) is Element of the carrier of F
(comp F) . a is Element of the carrier of F
the addF of F . (b,((comp F) . a)) is Element of the carrier of F
[b,((comp F) . a)] is set
the addF of F . [b,((comp F) . a)] is set
(comp F) . ( the addF of F . (b,((comp F) . a))) is Element of the carrier of F

the carrier of F is V11() non trivial set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
a is Element of the carrier of F
(comp F) . a is Element of the carrier of F
b is Element of the carrier of F
(F) . (((comp F) . a),b) is Element of the carrier of F
[((comp F) . a),b] is set
(F) . [((comp F) . a),b] is set
the addF of F . (a,b) is Element of the carrier of F
[a,b] is set
the addF of F . [a,b] is set
(comp F) . ( the addF of F . (a,b)) is Element of the carrier of F
(comp F) . b is Element of the carrier of F
the addF of F . (((comp F) . a),((comp F) . b)) is Element of the carrier of F
[((comp F) . a),((comp F) . b)] is set
the addF of F . [((comp F) . a),((comp F) . b)] is set
- a is Element of the carrier of F
the addF of F . ((- a),((comp F) . b)) is Element of the carrier of F
[(- a),((comp F) . b)] is set
the addF of F . [(- a),((comp F) . b)] is set
- b is Element of the carrier of F
(- a) + (- b) is Element of the carrier of F
the addF of F . ((- a),(- b)) is Element of the carrier of F
[(- a),(- b)] is set
the addF of F . [(- a),(- b)] is set
a + b is Element of the carrier of F
- (a + b) is Element of the carrier of F

the carrier of F is V11() non trivial set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
a is Element of the carrier of F
b is Element of the carrier of F
(F) . (a,b) is Element of the carrier of F
[a,b] is set
(F) . [a,b] is set
c is Element of the carrier of F
revfb is Element of the carrier of F
(F) . (c,revfb) is Element of the carrier of F
[c,revfb] is set
(F) . [c,revfb] is set
a + revfb is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the addF of F . (a,revfb) is Element of the carrier of F
[a,revfb] is set
the addF of F . [a,revfb] is set
b + c is Element of the carrier of F
the addF of F . (b,c) is Element of the carrier of F
[b,c] is set
the addF of F . [b,c] is set
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
(comp F) . revfb is Element of the carrier of F
the addF of F . (c,((comp F) . revfb)) is Element of the carrier of F
[c,((comp F) . revfb)] is set
the addF of F . [c,((comp F) . revfb)] is set
c - revfb is Element of the carrier of F
- revfb is Element of the carrier of F
c + (- revfb) is Element of the carrier of F
the addF of F . (c,(- revfb)) is Element of the carrier of F
[c,(- revfb)] is set
the addF of F . [c,(- revfb)] is set
(comp F) . b is Element of the carrier of F
the addF of F . (a,((comp F) . b)) is Element of the carrier of F
[a,((comp F) . b)] is set
the addF of F . [a,((comp F) . b)] is set
a - b is Element of the carrier of F
- b is Element of the carrier of F
a + (- b) is Element of the carrier of F
the addF of F . (a,(- b)) is Element of the carrier of F
[a,(- b)] is set
the addF of F . [a,(- b)] is set

the carrier of F is V11() non trivial set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
a is Element of the carrier of F
(F) . ((0. F),a) is Element of the carrier of F
[(0. F),a] is set
(F) . [(0. F),a] is set
(comp F) . a is Element of the carrier of F
(0. F) + ((comp F) . a) is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
the addF of F . ((0. F),((comp F) . a)) is Element of the carrier of F
[(0. F),((comp F) . a)] is set
the addF of F . [(0. F),((comp F) . a)] is set

the carrier of F is V11() non trivial set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
0. F is V51(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
a is Element of the carrier of F
(F) . (a,(0. F)) is Element of the carrier of F
[a,(0. F)] is set
(F) . [a,(0. F)] is set
the addF of F is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
comp F is V1() V4( the carrier of F) V5( the carrier of F) Function-like V18( the carrier of F, the carrier of F) Element of bool [: the carrier of F, the carrier of F:]
bool [: the carrier of F, the carrier of F:] is set
(comp F) . (0. F) is Element of the carrier of F
the addF of F . (a,((comp F) . (0. F))) is Element of the carrier of F
[a,((comp F) . (0. F))] is set
the addF of F . [a,((comp F) . (0. F))] is set
- (0. F) is Element of the carrier of F
the addF of F . (a,(- (0. F))) is Element of the carrier of F
[a,(- (0. F))] is set
the addF of F . [a,(- (0. F))] is set
a + (0. F) is Element of the carrier of F
the addF of F . (a,(0. F)) is Element of the carrier of F
the addF of F . [a,(0. F)] is set

the carrier of F is V11() non trivial set
(F) is V1() V4([: the carrier of F, the carrier of F:]) V5( the carrier of F) Function-like V18([: the carrier of F, the carrier of F:], the carrier of F) Element of bool [:[: the carrier of F, the carrier of F:], the carrier of F:]
[: the carrier of F, the carrier of F:] is set
[:[: the carrier of F, the carrier of F:], the carrier of F:] is set
bool [:[: the carrier of F, the carrier of F:], the carrier of F:] is set
a is Element of the carrier of F
b is Element of the carrier of F
a + b is Element of the carrier of F
the addF of F is V1() V4([: the carrier of F, the carrier of F