:: LMOD_5 semantic presentation

NAT is non empty V18() V19() V20() Element of K19(REAL)

REAL is set

K19(REAL) is non empty set

NAT is non empty V18() V19() V20() set

K19(NAT) is non empty set

K19(NAT) is non empty set

{} is Function-like functional empty V18() V19() V20() V22() V23() V24() finite V29() set

the Function-like functional empty V18() V19() V20() V22() V23() V24() finite V29() set is Function-like functional empty V18() V19() V20() V22() V23() V24() finite V29() set

1 is non empty set

R is non empty doubleLoopStr

V is non empty VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

R is non empty doubleLoopStr

V is non empty VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

A is Element of K19( the carrier of V)

B is Element of K19( the carrier of V)

the carrier of R is non empty set

v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum v is Element of the carrier of V

0. V is V49(V) Element of the carrier of V

Carrier v is finite Element of K19( the carrier of V)

0. R is V49(R) Element of the carrier of R

{ b

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B

Carrier l is finite Element of K19( the carrier of V)

{ b

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr

0. R is V49(R) Element of the carrier of R

the carrier of R is non empty set

1. R is Element of the carrier of R

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

0. V is V49(V) Element of the carrier of V

A is Element of K19( the carrier of V)

K20( the carrier of V, the carrier of R) is non empty set

K19(K20( the carrier of V, the carrier of R)) is non empty set

B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))

B . (0. V) is Element of the carrier of R

Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R

v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

{(0. V)} is non empty finite Element of K19( the carrier of V)

l is non empty finite Element of K19( the carrier of V)

D is Element of the carrier of V

v . D is Element of the carrier of R

D is finite Element of K19( the carrier of V)

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier l is finite Element of K19( the carrier of V)

{ b

{(0. V)} is non empty finite Element of K19( the carrier of V)

D is set

C is Element of the carrier of V

l . C is Element of the carrier of R

D is set

D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum D is Element of the carrier of V

D . (0. V) is Element of the carrier of R

(D . (0. V)) * (0. V) is Element of the carrier of V

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

{} the carrier of V is Function-like functional empty proper V18() V19() V20() V22() V23() V24() finite V29() Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

the carrier of R is non empty set

A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {} the carrier of V

Sum A is Element of the carrier of V

0. V is V49(V) Element of the carrier of V

Carrier A is finite Element of K19( the carrier of V)

0. R is V49(R) Element of the carrier of R

{ b

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr

0. R is V49(R) Element of the carrier of R

the carrier of R is non empty set

1. R is Element of the carrier of R

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

0. V is V49(V) Element of the carrier of V

A is Element of the carrier of V

B is Element of the carrier of V

{A,B} is non empty finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

R is non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

0. R is V49(R) Element of the carrier of R

the carrier of R is non empty set

1. R is Element of the carrier of R

A is Element of the carrier of V

0. V is V49(V) Element of the carrier of V

{A,(0. V)} is non empty finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{(0. V),A} is non empty finite Element of K19( the carrier of V)

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

the carrier of R is non empty V12() set

0. R is V49(R) Element of the carrier of R

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier A is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{ b

B is Element of the carrier of R

B * A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier (B * A) is finite Element of K19( the carrier of V)

{ b

D is set

C is Element of the carrier of V

(B * A) . C is Element of the carrier of R

A . C is Element of the carrier of R

B * (A . C) is Element of the carrier of R

D is set

C is Element of the carrier of V

A . C is Element of the carrier of R

(B * A) . C is Element of the carrier of R

B * (A . C) is Element of the carrier of R

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

the carrier of R is non empty V12() set

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Sum A is Element of the carrier of V

B is Element of the carrier of R

B * A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Sum (B * A) is Element of the carrier of V

B * (Sum A) is Element of the carrier of V

0. R is V49(R) Element of the carrier of R

Carrier (B * A) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{ b

Carrier A is finite Element of K19( the carrier of V)

{ b

l is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng l is set

A (#) l is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (A (#) l) is Element of the carrier of V

C is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng C is set

(B * A) (#) C is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum ((B * A) (#) C) is Element of the carrier of V

len l is V18() V19() V20() V24() Element of NAT

len C is V18() V19() V20() V24() Element of NAT

f is Relation-like Function-like FinSequence-like set

len f is V18() V19() V20() V24() Element of NAT

dom f is Element of K19(NAT)

Seg (len C) is Element of K19(NAT)

dom C is Element of K19(NAT)

f is set

dom l is Element of K19(NAT)

f is V18() V19() V20() V24() Element of NAT

l . f is set

f . f is set

C . (f . f) is set

C <- (l . f) is set

C . (C <- (l . f)) is set

l . f is set

f . f is set

C . (f . f) is set

rng f is set

f is set

f is set

f . f is set

g is V18() V19() V20() V24() Element of NAT

l . g is set

f . g is set

C <- (l . g) is set

f is set

f . f is set

f (#) C is Relation-like Function-like set

C " is Relation-like Function-like set

l (#) (C ") is Relation-like Function-like set

f is set

dom (C ") is set

rng (l (#) (C ")) is set

rng (C ") is set

C (#) (C ") is Relation-like Function-like set

f (#) (C (#) (C ")) is Relation-like Function-like set

id (dom C) is Relation-like dom C -defined dom C -valued Function-like one-to-one total Element of K19(K20((dom C),(dom C)))

K20((dom C),(dom C)) is set

K19(K20((dom C),(dom C))) is non empty set

f (#) (id (dom C)) is Relation-like Function-like set

K20((dom C),(dom C)) is set

K19(K20((dom C),(dom C))) is non empty set

len ((B * A) (#) C) is V18() V19() V20() V24() Element of NAT

dom ((B * A) (#) C) is Element of K19(NAT)

K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C))) is set

K19(K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C)))) is non empty set

f is Relation-like dom C -defined dom C -valued Function-like quasi_total Element of K19(K20((dom C),(dom C)))

f is Relation-like dom ((B * A) (#) C) -defined dom ((B * A) (#) C) -valued Function-like quasi_total Element of K19(K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C))))

((B * A) (#) C) * f is Relation-like dom ((B * A) (#) C) -defined the carrier of V -valued Function-like Element of K19(K20((dom ((B * A) (#) C)), the carrier of V))

K20((dom ((B * A) (#) C)), the carrier of V) is set

K19(K20((dom ((B * A) (#) C)), the carrier of V)) is non empty set

g is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

g is Relation-like dom ((B * A) (#) C) -defined dom ((B * A) (#) C) -valued Function-like quasi_total bijective Element of K19(K20((dom ((B * A) (#) C)),(dom ((B * A) (#) C))))

((B * A) (#) C) * g is Relation-like dom ((B * A) (#) C) -defined the carrier of V -valued Function-like Element of K19(K20((dom ((B * A) (#) C)), the carrier of V))

len g is V18() V19() V20() V24() Element of NAT

len (A (#) l) is V18() V19() V20() V24() Element of NAT

g is V18() V19() V20() V24() Element of NAT

dom g is Element of K19(NAT)

g is Element of the carrier of V

(A (#) l) . g is set

Seg (len (A (#) l)) is Element of K19(NAT)

dom g is set

l . g is set

C <- (l . g) is set

l /. g is Element of the carrier of V

g . g is set

C . (g . g) is set

v is V18() V19() V20() V24() Element of NAT

C . v is set

C /. v is Element of the carrier of V

dom (A (#) l) is Element of K19(NAT)

Seg (len ((B * A) (#) C)) is Element of K19(NAT)

g . g is set

((B * A) (#) C) . (g . g) is set

((B * A) (#) C) . (C <- (l . g)) is set

(B * A) . (C /. v) is Element of the carrier of R

((B * A) . (C /. v)) * (C /. v) is Element of the carrier of V

A . (C /. v) is Element of the carrier of R

B * (A . (C /. v)) is Element of the carrier of R

(B * (A . (C /. v))) * (C /. v) is Element of the carrier of V

(A . (C /. v)) * (C /. v) is Element of the carrier of V

B * ((A . (C /. v)) * (C /. v)) is Element of the carrier of V

B * g is Element of the carrier of V

Sum g is Element of the carrier of V

0. R is V49(R) Element of the carrier of R

ZeroLC V is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Sum (ZeroLC V) is Element of the carrier of V

0. V is V49(V) Element of the carrier of V

0. R is V49(R) Element of the carrier of R

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

the carrier of R is non empty V12() set

A is Element of K19( the carrier of V)

{ (Sum b

v is set

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum l is Element of the carrier of V

ZeroLC V is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

v is Element of K19( the carrier of V)

D is Element of the carrier of V

C is Element of the carrier of V

D + C is Element of the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

f + f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

D is Element of the carrier of R

C is Element of the carrier of V

D * C is Element of the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

D * f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum f is Element of the carrier of V

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum l is Element of the carrier of V

0. V is V49(V) Element of the carrier of V

B is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

the carrier of B is non empty set

v is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

the carrier of v is non empty set

R is set

V is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

the carrier of V is non empty V12() set

A is non empty right_complementable V105(V) V106(V) V107(V) V108(V) V112() V113() V114() VectSpStr over V

the carrier of A is non empty set

K19( the carrier of A) is non empty set

B is Element of K19( the carrier of A)

(V,A,B) is non empty right_complementable strict V105(V) V106(V) V107(V) V108(V) V112() V113() V114() Subspace of A

the carrier of (V,A,B) is non empty set

{ (Sum b

v is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B

Sum v is Element of the carrier of A

{ (Sum b

the carrier of (V,A,B) is non empty set

R is set

V is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

A is non empty right_complementable V105(V) V106(V) V107(V) V108(V) V112() V113() V114() VectSpStr over V

the carrier of A is non empty set

K19( the carrier of A) is non empty set

B is Element of K19( the carrier of A)

(V,A,B) is non empty right_complementable strict V105(V) V106(V) V107(V) V108(V) V112() V113() V114() Subspace of A

0. V is V49(V) Element of the carrier of V

the carrier of V is non empty V12() set

K20( the carrier of A, the carrier of V) is non empty set

K19(K20( the carrier of A, the carrier of V)) is non empty set

v is Element of the carrier of A

1. V is V49(V) Element of the carrier of V

l is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of K19(K20( the carrier of A, the carrier of V))

l . v is Element of the carrier of V

Funcs ( the carrier of A, the carrier of V) is non empty FUNCTION_DOMAIN of the carrier of A, the carrier of V

D is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of Funcs ( the carrier of A, the carrier of V)

{v} is non empty finite Element of K19( the carrier of A)

C is non empty finite Element of K19( the carrier of A)

f is Element of the carrier of A

D . f is Element of the carrier of V

f is finite Element of K19( the carrier of A)

C is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of A

Carrier C is finite Element of K19( the carrier of A)

{ b

{v} is non empty finite Element of K19( the carrier of A)

f is set

f is Element of the carrier of A

C . f is Element of the carrier of V

f is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of {v}

Sum f is Element of the carrier of A

(1. V) * v is Element of the carrier of A

Carrier f is finite Element of K19( the carrier of A)

{ b

f is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B

Sum f is Element of the carrier of A

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

{} the carrier of V is Function-like functional empty proper V18() V19() V20() V22() V23() V24() finite V29() Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

(R,V,({} the carrier of V)) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

(0). V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

B is Element of the carrier of V

the carrier of (R,V,({} the carrier of V)) is non empty set

the carrier of R is non empty V12() set

{ (Sum b

0. V is V49(V) Element of the carrier of V

v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of {} the carrier of V

Sum v is Element of the carrier of V

0. V is V49(V) Element of the carrier of V

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

(0). V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

0. V is V49(V) Element of the carrier of V

{(0. V)} is non empty finite Element of K19( the carrier of V)

A is Element of K19( the carrier of V)

(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

B is set

the Element of A is Element of A

v is set

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

0. R is V49(R) Element of the carrier of R

the carrier of R is non empty V12() set

1. R is V49(R) Element of the carrier of R

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

A is Element of K19( the carrier of V)

(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

B is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

the carrier of B is non empty set

v is Element of the carrier of V

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum l is Element of the carrier of V

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

0. R is V49(R) Element of the carrier of R

the carrier of R is non empty V12() set

1. R is V49(R) Element of the carrier of R

V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

A is Element of K19( the carrier of V)

(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

(Omega). V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

the addF of V is Relation-like K20( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K19(K20(K20( the carrier of V, the carrier of V), the carrier of V))

K20( the carrier of V, the carrier of V) is non empty set

K20(K20( the carrier of V, the carrier of V), the carrier of V) is non empty set

K19(K20(K20( the carrier of V, the carrier of V), the carrier of V)) is non empty set

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like K20( the carrier of R, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K19(K20(K20( the carrier of R, the carrier of V), the carrier of V))

K20( the carrier of R, the carrier of V) is non empty set

K20(K20( the carrier of R, the carrier of V), the carrier of V) is non empty set

K19(K20(K20( the carrier of R, the carrier of V), the carrier of V)) is non empty set

VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over R

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

A is Element of K19( the carrier of V)

(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

B is Element of K19( the carrier of V)

(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

v is Element of the carrier of V

the carrier of R is non empty V12() set

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

Sum l is Element of the carrier of V

D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B

Sum D is Element of the carrier of V

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

V is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

A is Element of K19( the carrier of V)

(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

B is Element of K19( the carrier of V)

(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

A is Element of K19( the carrier of V)

(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

B is Element of K19( the carrier of V)

A \/ B is Element of K19( the carrier of V)

(R,V,(A \/ B)) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

(R,V,A) + (R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

0. R is V49(R) Element of the carrier of R

the carrier of R is non empty V12() set

v is Element of the carrier of V

l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A \/ B

Sum l is Element of the carrier of V

Carrier l is finite Element of K19( the carrier of V)

{ b

(Carrier l) \ A is finite Element of K19( the carrier of V)

(Carrier l) /\ A is finite Element of K19( the carrier of V)

f is set

K20( the carrier of V, the carrier of R) is non empty set

K19(K20( the carrier of V, the carrier of R)) is non empty set

f is Element of the carrier of V

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))

f . f is Element of the carrier of R

l . f is set

f is set

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))

Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

f is Element of the carrier of V

f . f is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier f is finite Element of K19( the carrier of V)

{ b

f is set

g is Element of the carrier of V

f . g is Element of the carrier of R

g is set

g is Element of the carrier of V

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))

g . g is Element of the carrier of R

l . g is set

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)

g is Element of the carrier of V

g . g is Element of the carrier of R

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

Carrier g is finite Element of K19( the carrier of V)

{ b

g is set

v is Element of the carrier of V

g . v is Element of the carrier of R

f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of A

g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of B

f + g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Linear_Combination of V

v is Element of the carrier of V

l . v is Element of the carrier of R

(f + g) . v is Element of the carrier of R

f . v is Element of the carrier of R

g . v is Element of the carrier of R

(f . v) + (g . v) is Element of the carrier of R

(l . v) + (g . v) is Element of the carrier of R

(l . v) + (0. R) is Element of the carrier of R

f . v is Element of the carrier of R

g . v is Element of the carrier of R

(f . v) + (g . v) is Element of the carrier of R

(0. R) + (g . v) is Element of the carrier of R

f . v is Element of the carrier of R

g . v is Element of the carrier of R

(f . v) + (g . v) is Element of the carrier of R

(0. R) + (g . v) is Element of the carrier of R

(0. R) + (0. R) is Element of the carrier of R

Sum f is Element of the carrier of V

Sum g is Element of the carrier of V

(Sum f) + (Sum g) is Element of the carrier of V

R is non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like doubleLoopStr

V is non empty right_complementable V105(R) V106(R) V107(R) V108(R) V112() V113() V114() VectSpStr over R

the carrier of V is non empty set

K19( the carrier of V) is non empty set

A is Element of K19( the carrier of V)

(R,V,A) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

B is Element of K19( the carrier of V)

A /\ B is Element of K19( the carrier of V)

(R,V,(A /\ B)) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

(R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V

(R,V,A) /\ (R,V,B) is non empty right_complementable strict V105(R) V106(R) V107(R) V108(R) V112() V113() V114() Subspace of V