:: BILINEAR semantic presentation

K184() is Element of bool K180()
K180() is set
bool K180() is non empty set
K277() is strict doubleLoopStr
the carrier of K277() is set
K134() is set
bool K134() is non empty set
K177() is L6()
the carrier of K177() is set
bool K184() is non empty set
K181() is set
1 is non empty set
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
{} is set
the empty set is empty set
K is 1-sorted
K is non empty ZeroStr
the carrier of K is non empty set
V is VectSpStr over K
the carrier of V is set
f is VectSpStr over K
the carrier of f is set
[: the carrier of V, the carrier of f:] is set
0. K is V56(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
[: the carrier of V, the carrier of f:] --> (0. K) is Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
[:[: the carrier of V, the carrier of f:], the carrier of K:] is set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
K is non empty addLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
ww is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is Element of the carrier of V
A is Element of the carrier of f
w . (v,A) is Element of the carrier of K
[v,A] is set
{v,A} is set
{v} is set
{{v,A},{v}} is set
w . [v,A] is set
x . (v,A) is Element of the carrier of K
x . [v,A] is set
w . (v,A) is Element of the carrier of K
w . [v,A] is set
(x . (v,A)) + (w . (v,A)) is Element of the carrier of K
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
A is Element of the carrier of V
ww is Element of the carrier of f
v . (A,ww) is Element of the carrier of K
[A,ww] is set
{A,ww} is set
{A} is set
{{A,ww},{A}} is set
v . [A,ww] is set
x . (A,ww) is Element of the carrier of K
x . [A,ww] is set
w . (A,ww) is Element of the carrier of K
w . [A,ww] is set
(x . (A,ww)) + (w . (A,ww)) is Element of the carrier of K
B . (A,ww) is Element of the carrier of K
B . [A,ww] is set
K is non empty multMagma
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
w is Element of the carrier of K
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
ww is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is Element of the carrier of V
A is Element of the carrier of f
w . (v,A) is Element of the carrier of K
[v,A] is set
{v,A} is set
{v} is set
{{v,A},{v}} is set
w . [v,A] is set
x . (v,A) is Element of the carrier of K
x . [v,A] is set
w * (x . (v,A)) is Element of the carrier of K
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
A is Element of the carrier of V
ww is Element of the carrier of f
v . (A,ww) is Element of the carrier of K
[A,ww] is set
{A,ww} is set
{A} is set
{{A,ww},{A}} is set
v . [A,ww] is set
x . (A,ww) is Element of the carrier of K
x . [A,ww] is set
w * (x . (A,ww)) is Element of the carrier of K
B . (A,ww) is Element of the carrier of K
B . [A,ww] is set
K is non empty addLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
A is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
ww is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is Element of the carrier of V
v is Element of the carrier of f
ww . (w,v) is Element of the carrier of K
[w,v] is set
{w,v} is set
{w} is set
{{w,v},{w}} is set
ww . [w,v] is set
x . (w,v) is Element of the carrier of K
x . [w,v] is set
- (x . (w,v)) is Element of the carrier of K
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is Element of the carrier of V
A is Element of the carrier of f
w . (B,A) is Element of the carrier of K
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
w . [B,A] is set
x . (B,A) is Element of the carrier of K
x . [B,A] is set
- (x . (B,A)) is Element of the carrier of K
v . (B,A) is Element of the carrier of K
v . [B,A] is set
K is non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
- (1. K) is Element of the carrier of K
(K,V,f,x,(- (1. K))) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is Element of the carrier of V
B is Element of the carrier of f
w . (v,B) is Element of the carrier of K
[v,B] is set
{v,B} is set
{v} is set
{{v,B},{v}} is set
w . [v,B] is set
x . (v,B) is Element of the carrier of K
x . [v,B] is set
- (x . (v,B)) is Element of the carrier of K
(- (1. K)) * (x . (v,B)) is Element of the carrier of K
(K,V,f,x,(- (1. K))) . (v,B) is Element of the carrier of K
(K,V,f,x,(- (1. K))) . [v,B] is set
v is Element of the carrier of V
B is Element of the carrier of f
w . (v,B) is Element of the carrier of K
[v,B] is set
{v,B} is set
{v} is set
{{v,B},{v}} is set
w . [v,B] is set
x . (v,B) is Element of the carrier of K
x . [v,B] is set
(- (1. K)) * (x . (v,B)) is Element of the carrier of K
- (x . (v,B)) is Element of the carrier of K
(K,V,f,x) . (v,B) is Element of the carrier of K
(K,V,f,x) . [v,B] is set
K is non empty addLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,(K,V,f,w)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
K is non empty addLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,(K,V,f,w)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is Element of the carrier of V
A is Element of the carrier of f
v . (B,A) is Element of the carrier of K
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
v . [B,A] is set
x . (B,A) is Element of the carrier of K
x . [B,A] is set
w . (B,A) is Element of the carrier of K
w . [B,A] is set
(x . (B,A)) - (w . (B,A)) is Element of the carrier of K
(K,V,f,w) . (B,A) is Element of the carrier of K
(K,V,f,w) . [B,A] is set
(x . (B,A)) + ((K,V,f,w) . (B,A)) is Element of the carrier of K
- (w . (B,A)) is Element of the carrier of K
(x . (B,A)) + (- (w . (B,A))) is Element of the carrier of K
B is Element of the carrier of V
A is Element of the carrier of f
v . (B,A) is Element of the carrier of K
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
v . [B,A] is set
x . (B,A) is Element of the carrier of K
x . [B,A] is set
w . (B,A) is Element of the carrier of K
w . [B,A] is set
(x . (B,A)) - (w . (B,A)) is Element of the carrier of K
- (w . (B,A)) is Element of the carrier of K
(x . (B,A)) + (- (w . (B,A))) is Element of the carrier of K
(K,V,f,w) . (B,A) is Element of the carrier of K
(K,V,f,w) . [B,A] is set
(x . (B,A)) + ((K,V,f,w) . (B,A)) is Element of the carrier of K
(K,V,f,x,w) . (B,A) is Element of the carrier of K
(K,V,f,x,w) . [B,A] is set
K is non empty Abelian addLoopStr
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,v,B) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,B,v) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
A is Element of the carrier of V
ww is Element of the carrier of f
(K,V,f,v,B) . (A,ww) is Element of the carrier of K
[A,ww] is set
{A,ww} is set
{A} is set
{{A,ww},{A}} is set
(K,V,f,v,B) . [A,ww] is set
v . (A,ww) is Element of the carrier of K
v . [A,ww] is set
B . (A,ww) is Element of the carrier of K
B . [A,ww] is set
(v . (A,ww)) + (B . (A,ww)) is Element of the carrier of K
(K,V,f,B,v) . (A,ww) is Element of the carrier of K
(K,V,f,B,v) . [A,ww] is set
K is non empty right_zeroed addLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
(K,V,f) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
0. K is V56(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
[: the carrier of V, the carrier of f:] --> (0. K) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,(K,V,f)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is Element of the carrier of V
B is Element of the carrier of f
(K,V,f,x,(K,V,f)) . (v,B) is Element of the carrier of K
[v,B] is set
{v,B} is set
{v} is set
{{v,B},{v}} is set
(K,V,f,x,(K,V,f)) . [v,B] is set
x . (v,B) is Element of the carrier of K
x . [v,B] is set
(K,V,f) . (v,B) is Element of the carrier of K
(K,V,f) . [v,B] is set
(x . (v,B)) + ((K,V,f) . (v,B)) is Element of the carrier of K
(x . (v,B)) + (0. K) is Element of the carrier of K
K is non empty add-associative addLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,(K,V,f,x,w),v) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,w,v) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,(K,V,f,w,v)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is Element of the carrier of V
A is Element of the carrier of f
(K,V,f,(K,V,f,x,w),v) . (B,A) is Element of the carrier of K
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
(K,V,f,(K,V,f,x,w),v) . [B,A] is set
(K,V,f,x,w) . (B,A) is Element of the carrier of K
(K,V,f,x,w) . [B,A] is set
v . (B,A) is Element of the carrier of K
v . [B,A] is set
((K,V,f,x,w) . (B,A)) + (v . (B,A)) is Element of the carrier of K
x . (B,A) is Element of the carrier of K
x . [B,A] is set
w . (B,A) is Element of the carrier of K
w . [B,A] is set
(x . (B,A)) + (w . (B,A)) is Element of the carrier of K
((x . (B,A)) + (w . (B,A))) + (v . (B,A)) is Element of the carrier of K
(w . (B,A)) + (v . (B,A)) is Element of the carrier of K
(x . (B,A)) + ((w . (B,A)) + (v . (B,A))) is Element of the carrier of K
(K,V,f,w,v) . (B,A) is Element of the carrier of K
(K,V,f,w,v) . [B,A] is set
(x . (B,A)) + ((K,V,f,w,v) . (B,A)) is Element of the carrier of K
(K,V,f,x,(K,V,f,w,v)) . (B,A) is Element of the carrier of K
(K,V,f,x,(K,V,f,w,v)) . [B,A] is set
K is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
(K,V,f) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
0. K is V56(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
[: the carrier of V, the carrier of f:] --> (0. K) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,(K,V,f,x)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is Element of the carrier of V
v is Element of the carrier of f
(K,V,f,x,x) . (w,v) is Element of the carrier of K
[w,v] is set
{w,v} is set
{w} is set
{{w,v},{w}} is set
(K,V,f,x,x) . [w,v] is set
x . (w,v) is Element of the carrier of K
x . [w,v] is set
(x . (w,v)) - (x . (w,v)) is Element of the carrier of K
(K,V,f) . (w,v) is Element of the carrier of K
(K,V,f) . [w,v] is set
K is non empty right-distributive doubleLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is Element of the carrier of K
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,w,v) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,(K,V,f,w,v),x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,w,x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,v,x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,(K,V,f,w,x),(K,V,f,v,x)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is Element of the carrier of V
A is Element of the carrier of f
(K,V,f,(K,V,f,w,v),x) . (B,A) is Element of the carrier of K
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
(K,V,f,(K,V,f,w,v),x) . [B,A] is set
(K,V,f,w,v) . (B,A) is Element of the carrier of K
(K,V,f,w,v) . [B,A] is set
x * ((K,V,f,w,v) . (B,A)) is Element of the carrier of K
w . (B,A) is Element of the carrier of K
w . [B,A] is set
v . (B,A) is Element of the carrier of K
v . [B,A] is set
(w . (B,A)) + (v . (B,A)) is Element of the carrier of K
x * ((w . (B,A)) + (v . (B,A))) is Element of the carrier of K
x * (w . (B,A)) is Element of the carrier of K
x * (v . (B,A)) is Element of the carrier of K
(x * (w . (B,A))) + (x * (v . (B,A))) is Element of the carrier of K
(K,V,f,w,x) . (B,A) is Element of the carrier of K
(K,V,f,w,x) . [B,A] is set
((K,V,f,w,x) . (B,A)) + (x * (v . (B,A))) is Element of the carrier of K
(K,V,f,v,x) . (B,A) is Element of the carrier of K
(K,V,f,v,x) . [B,A] is set
((K,V,f,w,x) . (B,A)) + ((K,V,f,v,x) . (B,A)) is Element of the carrier of K
(K,V,f,(K,V,f,w,x),(K,V,f,v,x)) . (B,A) is Element of the carrier of K
(K,V,f,(K,V,f,w,x),(K,V,f,v,x)) . [B,A] is set
K is non empty left-distributive doubleLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is Element of the carrier of K
w is Element of the carrier of K
x + w is Element of the carrier of K
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,v,(x + w)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,v,x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,v,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,(K,V,f,v,x),(K,V,f,v,w)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is Element of the carrier of V
A is Element of the carrier of f
(K,V,f,v,(x + w)) . (B,A) is Element of the carrier of K
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
(K,V,f,v,(x + w)) . [B,A] is set
v . (B,A) is Element of the carrier of K
v . [B,A] is set
(x + w) * (v . (B,A)) is Element of the carrier of K
x * (v . (B,A)) is Element of the carrier of K
w * (v . (B,A)) is Element of the carrier of K
(x * (v . (B,A))) + (w * (v . (B,A))) is Element of the carrier of K
(K,V,f,v,x) . (B,A) is Element of the carrier of K
(K,V,f,v,x) . [B,A] is set
((K,V,f,v,x) . (B,A)) + (w * (v . (B,A))) is Element of the carrier of K
(K,V,f,v,w) . (B,A) is Element of the carrier of K
(K,V,f,v,w) . [B,A] is set
((K,V,f,v,x) . (B,A)) + ((K,V,f,v,w) . (B,A)) is Element of the carrier of K
(K,V,f,(K,V,f,v,x),(K,V,f,v,w)) . (B,A) is Element of the carrier of K
(K,V,f,(K,V,f,v,x),(K,V,f,v,w)) . [B,A] is set
K is non empty associative doubleLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is Element of the carrier of K
w is Element of the carrier of K
x * w is Element of the carrier of K
v is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,v,(x * w)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,v,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,(K,V,f,v,w),x) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
B is Element of the carrier of V
A is Element of the carrier of f
(K,V,f,v,(x * w)) . (B,A) is Element of the carrier of K
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
(K,V,f,v,(x * w)) . [B,A] is set
v . (B,A) is Element of the carrier of K
v . [B,A] is set
(x * w) * (v . (B,A)) is Element of the carrier of K
w * (v . (B,A)) is Element of the carrier of K
x * (w * (v . (B,A))) is Element of the carrier of K
(K,V,f,v,w) . (B,A) is Element of the carrier of K
(K,V,f,v,w) . [B,A] is set
x * ((K,V,f,v,w) . (B,A)) is Element of the carrier of K
(K,V,f,(K,V,f,v,w),x) . (B,A) is Element of the carrier of K
(K,V,f,(K,V,f,v,w),x) . [B,A] is set
K is non empty left_unital doubleLoopStr
the carrier of K is non empty set
1. K is Element of the carrier of K
the OneF of K is Element of the carrier of K
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,(1. K)) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is Element of the carrier of V
v is Element of the carrier of f
(K,V,f,x,(1. K)) . (w,v) is Element of the carrier of K
[w,v] is set
{w,v} is set
{w} is set
{{w,v},{w}} is set
(K,V,f,x,(1. K)) . [w,v] is set
x . (w,v) is Element of the carrier of K
x . [w,v] is set
(1. K) * (x . (w,v)) is Element of the carrier of K
K is non empty 1-sorted
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
K116( the carrier of f, the carrier of K) is non empty functional M5( the carrier of f, the carrier of K)
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
curry x is non empty Relation-like the carrier of V -defined K116( the carrier of f, the carrier of K) -valued Function-like V20( the carrier of V) V21( the carrier of V,K116( the carrier of f, the carrier of K)) Element of bool [: the carrier of V,K116( the carrier of f, the carrier of K):]
[: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
bool [: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
w is Element of the carrier of V
(curry x) . w is Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of K116( the carrier of f, the carrier of K)
[: the carrier of f, the carrier of K:] is non empty set
bool [: the carrier of f, the carrier of K:] is non empty set
K is non empty 1-sorted
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
the carrier of K is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
K116( the carrier of V, the carrier of K) is non empty functional M5( the carrier of V, the carrier of K)
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
curry' x is non empty Relation-like the carrier of f -defined K116( the carrier of V, the carrier of K) -valued Function-like V20( the carrier of f) V21( the carrier of f,K116( the carrier of V, the carrier of K)) Element of bool [: the carrier of f,K116( the carrier of V, the carrier of K):]
[: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
bool [: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
w is Element of the carrier of f
(curry' x) . w is Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of K116( the carrier of V, the carrier of K)
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
K is non empty 1-sorted
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is Element of the carrier of V
(K,V,f,x,w) is non empty Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of bool [: the carrier of f, the carrier of K:]
[: the carrier of f, the carrier of K:] is non empty set
bool [: the carrier of f, the carrier of K:] is non empty set
K116( the carrier of f, the carrier of K) is non empty functional M5( the carrier of f, the carrier of K)
curry x is non empty Relation-like the carrier of V -defined K116( the carrier of f, the carrier of K) -valued Function-like V20( the carrier of V) V21( the carrier of V,K116( the carrier of f, the carrier of K)) Element of bool [: the carrier of V,K116( the carrier of f, the carrier of K):]
[: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
bool [: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
(curry x) . w is Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of K116( the carrier of f, the carrier of K)
dom (K,V,f,x,w) is Element of bool the carrier of f
bool the carrier of f is non empty set
rng (K,V,f,x,w) is Element of bool the carrier of K
bool the carrier of K is non empty set
dom x is Relation-like the carrier of V -defined the carrier of f -valued Element of bool [: the carrier of V, the carrier of f:]
bool [: the carrier of V, the carrier of f:] is non empty set
rng x is Element of bool the carrier of K
B is Relation-like Function-like set
dom B is set
rng B is set
B is Element of the carrier of f
(K,V,f,x,w) . B is Element of the carrier of K
x . (w,B) is Element of the carrier of K
[w,B] is set
{w,B} is set
{w} is set
{{w,B},{w}} is set
x . [w,B] is set
A is Relation-like Function-like set
dom A is set
rng A is set
K is non empty 1-sorted
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is Element of the carrier of f
(K,V,f,x,w) is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of bool [: the carrier of V, the carrier of K:]
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
K116( the carrier of V, the carrier of K) is non empty functional M5( the carrier of V, the carrier of K)
curry' x is non empty Relation-like the carrier of f -defined K116( the carrier of V, the carrier of K) -valued Function-like V20( the carrier of f) V21( the carrier of f,K116( the carrier of V, the carrier of K)) Element of bool [: the carrier of f,K116( the carrier of V, the carrier of K):]
[: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
bool [: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
(curry' x) . w is Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of K116( the carrier of V, the carrier of K)
dom (K,V,f,x,w) is Element of bool the carrier of V
bool the carrier of V is non empty set
rng (K,V,f,x,w) is Element of bool the carrier of K
bool the carrier of K is non empty set
dom x is Relation-like the carrier of V -defined the carrier of f -valued Element of bool [: the carrier of V, the carrier of f:]
bool [: the carrier of V, the carrier of f:] is non empty set
rng x is Element of bool the carrier of K
B is Relation-like Function-like set
dom B is set
rng B is set
B is Element of the carrier of V
(K,V,f,x,w) . B is Element of the carrier of K
x . (B,w) is Element of the carrier of K
[B,w] is set
{B,w} is set
{B} is set
{{B,w},{B}} is set
x . [B,w] is set
A is Relation-like Function-like set
dom A is set
rng A is set
K is non empty ZeroStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
(K,V,f) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
0. K is V56(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
[: the carrier of V, the carrier of f:] --> (0. K) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
0Functional f is non empty Relation-like the carrier of f -defined the carrier of K -valued Function-like constant V20( the carrier of f) V21( the carrier of f, the carrier of K) 0-preserving Element of bool [: the carrier of f, the carrier of K:]
[: the carrier of f, the carrier of K:] is non empty set
bool [: the carrier of f, the carrier of K:] is non empty set
[#] f is non empty non proper Element of bool the carrier of f
bool the carrier of f is non empty set
([#] f) --> (0. K) is non empty Relation-like [#] f -defined the carrier of K -valued Function-like V20( [#] f) V21( [#] f, the carrier of K) Element of bool [:([#] f), the carrier of K:]
[:([#] f), the carrier of K:] is non empty set
bool [:([#] f), the carrier of K:] is non empty set
x is Element of the carrier of V
(K,V,f,(K,V,f),x) is non empty Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of bool [: the carrier of f, the carrier of K:]
K116( the carrier of f, the carrier of K) is non empty functional M5( the carrier of f, the carrier of K)
curry (K,V,f) is non empty Relation-like the carrier of V -defined K116( the carrier of f, the carrier of K) -valued Function-like V20( the carrier of V) V21( the carrier of V,K116( the carrier of f, the carrier of K)) Element of bool [: the carrier of V,K116( the carrier of f, the carrier of K):]
[: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
bool [: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
(curry (K,V,f)) . x is Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of K116( the carrier of f, the carrier of K)
v is Element of the carrier of f
(K,V,f,(K,V,f),x) . v is Element of the carrier of K
(K,V,f) . (x,v) is Element of the carrier of K
[x,v] is set
{x,v} is set
{x} is set
{{x,v},{x}} is set
(K,V,f) . [x,v] is set
(0Functional f) . v is Element of the carrier of K
K is non empty ZeroStr
the carrier of K is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
(K,V,f) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
0. K is V56(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
[: the carrier of V, the carrier of f:] --> (0. K) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
0Functional V is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like constant V20( the carrier of V) V21( the carrier of V, the carrier of K) 0-preserving Element of bool [: the carrier of V, the carrier of K:]
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
[#] V is non empty non proper Element of bool the carrier of V
bool the carrier of V is non empty set
([#] V) --> (0. K) is non empty Relation-like [#] V -defined the carrier of K -valued Function-like V20( [#] V) V21( [#] V, the carrier of K) Element of bool [:([#] V), the carrier of K:]
[:([#] V), the carrier of K:] is non empty set
bool [:([#] V), the carrier of K:] is non empty set
x is Element of the carrier of f
(K,V,f,(K,V,f),x) is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of bool [: the carrier of V, the carrier of K:]
K116( the carrier of V, the carrier of K) is non empty functional M5( the carrier of V, the carrier of K)
curry' (K,V,f) is non empty Relation-like the carrier of f -defined K116( the carrier of V, the carrier of K) -valued Function-like V20( the carrier of f) V21( the carrier of f,K116( the carrier of V, the carrier of K)) Element of bool [: the carrier of f,K116( the carrier of V, the carrier of K):]
[: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
bool [: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
(curry' (K,V,f)) . x is Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of K116( the carrier of V, the carrier of K)
v is Element of the carrier of V
(K,V,f,(K,V,f),x) . v is Element of the carrier of K
(K,V,f) . (v,x) is Element of the carrier of K
[v,x] is set
{v,x} is set
{v} is set
{{v,x},{v}} is set
(K,V,f) . [v,x] is set
(0Functional V) . v is Element of the carrier of K
K is non empty addLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is Element of the carrier of f
(K,V,f,(K,V,f,x,w),v) is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of bool [: the carrier of V, the carrier of K:]
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
K116( the carrier of V, the carrier of K) is non empty functional M5( the carrier of V, the carrier of K)
curry' (K,V,f,x,w) is non empty Relation-like the carrier of f -defined K116( the carrier of V, the carrier of K) -valued Function-like V20( the carrier of f) V21( the carrier of f,K116( the carrier of V, the carrier of K)) Element of bool [: the carrier of f,K116( the carrier of V, the carrier of K):]
[: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
bool [: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
(curry' (K,V,f,x,w)) . v is Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of K116( the carrier of V, the carrier of K)
(K,V,f,x,v) is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of bool [: the carrier of V, the carrier of K:]
curry' x is non empty Relation-like the carrier of f -defined K116( the carrier of V, the carrier of K) -valued Function-like V20( the carrier of f) V21( the carrier of f,K116( the carrier of V, the carrier of K)) Element of bool [: the carrier of f,K116( the carrier of V, the carrier of K):]
(curry' x) . v is Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of K116( the carrier of V, the carrier of K)
(K,V,f,w,v) is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of bool [: the carrier of V, the carrier of K:]
curry' w is non empty Relation-like the carrier of f -defined K116( the carrier of V, the carrier of K) -valued Function-like V20( the carrier of f) V21( the carrier of f,K116( the carrier of V, the carrier of K)) Element of bool [: the carrier of f,K116( the carrier of V, the carrier of K):]
(curry' w) . v is Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of K116( the carrier of V, the carrier of K)
(K,V,f,x,v) + (K,V,f,w,v) is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of bool [: the carrier of V, the carrier of K:]
B is Element of the carrier of V
(K,V,f,(K,V,f,x,w),v) . B is Element of the carrier of K
(K,V,f,x,w) . (B,v) is Element of the carrier of K
[B,v] is set
{B,v} is set
{B} is set
{{B,v},{B}} is set
(K,V,f,x,w) . [B,v] is set
x . (B,v) is Element of the carrier of K
x . [B,v] is set
w . (B,v) is Element of the carrier of K
w . [B,v] is set
(x . (B,v)) + (w . (B,v)) is Element of the carrier of K
(K,V,f,x,v) . B is Element of the carrier of K
((K,V,f,x,v) . B) + (w . (B,v)) is Element of the carrier of K
(K,V,f,w,v) . B is Element of the carrier of K
((K,V,f,x,v) . B) + ((K,V,f,w,v) . B) is Element of the carrier of K
((K,V,f,x,v) + (K,V,f,w,v)) . B is Element of the carrier of K
K is non empty addLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
(K,V,f,x,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is Element of the carrier of V
(K,V,f,(K,V,f,x,w),v) is non empty Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of bool [: the carrier of f, the carrier of K:]
[: the carrier of f, the carrier of K:] is non empty set
bool [: the carrier of f, the carrier of K:] is non empty set
K116( the carrier of f, the carrier of K) is non empty functional M5( the carrier of f, the carrier of K)
curry (K,V,f,x,w) is non empty Relation-like the carrier of V -defined K116( the carrier of f, the carrier of K) -valued Function-like V20( the carrier of V) V21( the carrier of V,K116( the carrier of f, the carrier of K)) Element of bool [: the carrier of V,K116( the carrier of f, the carrier of K):]
[: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
bool [: the carrier of V,K116( the carrier of f, the carrier of K):] is non empty set
(curry (K,V,f,x,w)) . v is Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of K116( the carrier of f, the carrier of K)
(K,V,f,x,v) is non empty Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of bool [: the carrier of f, the carrier of K:]
curry x is non empty Relation-like the carrier of V -defined K116( the carrier of f, the carrier of K) -valued Function-like V20( the carrier of V) V21( the carrier of V,K116( the carrier of f, the carrier of K)) Element of bool [: the carrier of V,K116( the carrier of f, the carrier of K):]
(curry x) . v is Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of K116( the carrier of f, the carrier of K)
(K,V,f,w,v) is non empty Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of bool [: the carrier of f, the carrier of K:]
curry w is non empty Relation-like the carrier of V -defined K116( the carrier of f, the carrier of K) -valued Function-like V20( the carrier of V) V21( the carrier of V,K116( the carrier of f, the carrier of K)) Element of bool [: the carrier of V,K116( the carrier of f, the carrier of K):]
(curry w) . v is Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of K116( the carrier of f, the carrier of K)
(K,V,f,x,v) + (K,V,f,w,v) is non empty Relation-like the carrier of f -defined the carrier of K -valued Function-like V20( the carrier of f) V21( the carrier of f, the carrier of K) Element of bool [: the carrier of f, the carrier of K:]
B is Element of the carrier of f
(K,V,f,(K,V,f,x,w),v) . B is Element of the carrier of K
(K,V,f,x,w) . (v,B) is Element of the carrier of K
[v,B] is set
{v,B} is set
{v} is set
{{v,B},{v}} is set
(K,V,f,x,w) . [v,B] is set
x . (v,B) is Element of the carrier of K
x . [v,B] is set
w . (v,B) is Element of the carrier of K
w . [v,B] is set
(x . (v,B)) + (w . (v,B)) is Element of the carrier of K
(K,V,f,x,v) . B is Element of the carrier of K
((K,V,f,x,v) . B) + (w . (v,B)) is Element of the carrier of K
(K,V,f,w,v) . B is Element of the carrier of K
((K,V,f,x,v) . B) + ((K,V,f,w,v) . B) is Element of the carrier of K
((K,V,f,x,v) + (K,V,f,w,v)) . B is Element of the carrier of K
K is non empty doubleLoopStr
the carrier of K is non empty set
V is non empty VectSpStr over K
the carrier of V is non empty set
f is non empty VectSpStr over K
the carrier of f is non empty set
[: the carrier of V, the carrier of f:] is non empty set
[:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
bool [:[: the carrier of V, the carrier of f:], the carrier of K:] is non empty set
x is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
w is Element of the carrier of K
(K,V,f,x,w) is non empty Relation-like [: the carrier of V, the carrier of f:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of f:]) V21([: the carrier of V, the carrier of f:], the carrier of K) Element of bool [:[: the carrier of V, the carrier of f:], the carrier of K:]
v is Element of the carrier of f
(K,V,f,(K,V,f,x,w),v) is non empty Relation-like the carrier of V -defined the carrier of K -valued Function-like V20( the carrier of V) V21( the carrier of V, the carrier of K) Element of bool [: the carrier of V, the carrier of K:]
[: the carrier of V, the carrier of K:] is non empty set
bool [: the carrier of V, the carrier of K:] is non empty set
K116( the carrier of V, the carrier of K) is non empty functional M5( the carrier of V, the carrier of K)
curry' (K,V,f,x,w) is non empty Relation-like the carrier of f -defined K116( the carrier of V, the carrier of K) -valued Function-like V20( the carrier of f) V21( the carrier of f,K116( the carrier of V, the carrier of K)) Element of bool [: the carrier of f,K116( the carrier of V, the carrier of K):]
[: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
bool [: the carrier of f,K116( the carrier of V, the carrier of K):] is non empty set
(curry' (K,V,f,x,w)) . v is Relation-like the carrier of V -defined the carrier of K -valued