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