:: RANKNULL semantic presentation

REAL is set

NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal Element of K6(REAL)

K6(REAL) is non empty set

NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal set

K6(NAT) is non empty V2() non finite set

K6(NAT) is non empty V2() non finite set

0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of NAT

{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() set

the empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() set is empty V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() set

1 is non empty V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT

2 is non empty V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT

K223(0,1,2) is non empty finite set

K7(K223(0,1,2),K223(0,1,2)) is non empty Relation-like finite set

K7(K7(K223(0,1,2),K223(0,1,2)),K223(0,1,2)) is non empty Relation-like finite set

K6(K7(K7(K223(0,1,2),K223(0,1,2)),K223(0,1,2))) is non empty finite V38() set

K6(K7(K223(0,1,2),K223(0,1,2))) is non empty finite V38() set

COMPLEX is set

RAT is set

INT is set

K7(NAT,REAL) is Relation-like set

K6(K7(NAT,REAL)) is non empty set

3 is non empty V4() V5() V6() V10() V11() ext-real finite cardinal V46() Element of NAT

V is Relation-like Function-like set

F is Relation-like Function-like set

rng V is set

F | (rng V) is Relation-like Function-like set

dom F is set

V (#) F is Relation-like Function-like set

dom (V (#) F) is set

dom V is set

T is set

T is set

V . T is set

T is set

A is set

(V (#) F) . T is set

(V (#) F) . A is set

V . T is set

F . (V . T) is set

V . A is set

F . (V . A) is set

dom (F | (rng V)) is set

(F | (rng V)) . (V . T) is set

(F | (rng V)) . (V . A) is set

F is Relation-like Function-like set

V is set

W is set

F | W is Relation-like Function-like set

F | V is Relation-like Function-like set

(F | W) | V is Relation-like Function-like set

F is 1-sorted

the carrier of F is set

K6( the carrier of F) is non empty set

V is Element of K6( the carrier of F)

W is Element of K6( the carrier of F)

T is set

A is Element of the carrier of F

T is Element of the carrier of F

A is Element of the carrier of F

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is finite Element of K6( the carrier of V)

T is Basis of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of V, the carrier of W) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of W)) is non empty set

[#] V is non empty non proper Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

FuncZero (([#] V),W) is Relation-like [#] V -defined the carrier of W -valued Function-like quasi_total Element of Funcs (([#] V), the carrier of W)

Funcs (([#] V), the carrier of W) is non empty FUNCTION_DOMAIN of [#] V, the carrier of W

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

([#] V) --> (0. W) is non empty Relation-like [#] V -defined the carrier of W -valued Function-like constant total quasi_total Element of K6(K7(([#] V), the carrier of W))

K7(([#] V), the carrier of W) is non empty Relation-like set

K6(K7(([#] V), the carrier of W)) is non empty set

{(0. W)} is non empty V2() finite 1 -element set

K7(([#] V),{(0. W)}) is non empty Relation-like set

A is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total Element of K6(K7( the carrier of V, the carrier of W))

A9 is Element of the carrier of V

B is Element of the carrier of V

A9 + B is Element of the carrier of V

A . (A9 + B) is Element of the carrier of W

A . A9 is Element of the carrier of W

A . B is Element of the carrier of W

(A . A9) + (A . B) is Element of the carrier of W

the carrier of F is non empty V2() set

A9 is Element of the carrier of F

B is Element of the carrier of V

A9 * B is Element of the carrier of V

A . (A9 * B) is Element of the carrier of W

A . B is Element of the carrier of W

A9 * (A . B) is Element of the carrier of W

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

[#] V is non empty non proper Element of K6( the carrier of V)

the carrier of V is non empty set

K6( the carrier of V) is non empty set

the Basis of V is Basis of V

T is finite Element of K6( the carrier of V)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F

[#] V is non empty non proper Element of K6( the carrier of V)

the carrier of V is non empty set

K6( the carrier of V) is non empty set

card ([#] V) is non empty V4() V5() V6() cardinal set

dim V is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set

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

the ZeroF of V is Element of the carrier of V

{(0. V)} is non empty V2() finite 1 -element Element of K6( the carrier of V)

W is set

{W} is non empty V2() finite 1 -element set

(Omega). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V

the U5 of V is Relation-like K7( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of V, the carrier of V), the carrier of V))

K7( the carrier of V, the carrier of V) is non empty Relation-like set

K7(K7( the carrier of V, the carrier of V), the carrier of V) is non empty Relation-like set

K6(K7(K7( the carrier of V, the carrier of V), the carrier of V)) is non empty set

the lmult of V is Relation-like K7( the carrier of F, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of V), the carrier of V))

the carrier of F is non empty V2() set

K7( the carrier of F, the carrier of V) is non empty Relation-like set

K7(K7( the carrier of F, the carrier of V), the carrier of V) is non empty Relation-like set

K6(K7(K7( the carrier of F, the carrier of V), the carrier of V)) is non empty set

VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is strict VectSpStr over F

(0). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

[#] V is non empty non proper Element of K6( the carrier of V)

the carrier of V is non empty set

K6( the carrier of V) is non empty set

card ([#] V) is non empty V4() V5() V6() cardinal set

dim V is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set

T is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F

the carrier of T is non empty set

0. T is V55(T) Element of the carrier of T

the ZeroF of T is Element of the carrier of T

(Omega). T is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T

the U5 of T is Relation-like K7( the carrier of T, the carrier of T) -defined the carrier of T -valued Function-like quasi_total Element of K6(K7(K7( the carrier of T, the carrier of T), the carrier of T))

K7( the carrier of T, the carrier of T) is non empty Relation-like set

K7(K7( the carrier of T, the carrier of T), the carrier of T) is non empty Relation-like set

K6(K7(K7( the carrier of T, the carrier of T), the carrier of T)) is non empty set

the lmult of T is Relation-like K7( the carrier of F, the carrier of T) -defined the carrier of T -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of T), the carrier of T))

the carrier of F is non empty V2() set

K7( the carrier of F, the carrier of T) is non empty Relation-like set

K7(K7( the carrier of F, the carrier of T), the carrier of T) is non empty Relation-like set

K6(K7(K7( the carrier of F, the carrier of T), the carrier of T)) is non empty set

VectSpStr(# the carrier of T, the U5 of T, the ZeroF of T, the lmult of T #) is strict VectSpStr over F

[#] T is non empty non proper Element of K6( the carrier of T)

K6( the carrier of T) is non empty set

A is set

A9 is set

{A,A9} is non empty finite set

B is Element of the carrier of T

{B} is non empty V2() finite 1 -element Element of K6( the carrier of T)

Lin {B} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T

X is Element of the carrier of T

0. (Lin {B}) is V55( Lin {B}) Element of the carrier of (Lin {B})

the carrier of (Lin {B}) is non empty set

the ZeroF of (Lin {B}) is Element of the carrier of (Lin {B})

B is Element of the carrier of T

B is Element of the carrier of T

B is Element of the carrier of T

{B} is non empty V2() finite 1 -element Element of K6( the carrier of T)

Lin {B} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T

X is Element of the carrier of T

0. (Lin {B}) is V55( Lin {B}) Element of the carrier of (Lin {B})

the carrier of (Lin {B}) is non empty set

the ZeroF of (Lin {B}) is Element of the carrier of (Lin {B})

B is Element of the carrier of T

B is Element of the carrier of T

A is Element of the carrier of T

{A} is non empty V2() finite 1 -element Element of K6( the carrier of T)

K6( the carrier of T) is non empty set

Lin {A} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of T

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

F is non empty 1-sorted

the carrier of F is non empty set

V is non empty 1-sorted

the carrier of V is non empty set

K7( the carrier of F, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of F, the carrier of V)) is non empty set

[#] F is non empty non proper Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

[#] V is non empty non proper Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

W is Relation-like the carrier of F -defined the carrier of V -valued Function-like quasi_total Element of K6(K7( the carrier of F, the carrier of V))

dom W is Element of K6( the carrier of F)

rng W is set

Funcs (([#] F),([#] V)) is non empty FUNCTION_DOMAIN of [#] F, [#] V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

A is Element of the carrier of W

T . A is Element of the carrier of V

A9 is Element of the carrier of W

T . A9 is Element of the carrier of V

(T . A) - (T . A9) is Element of the carrier of V

- (T . A9) is Element of the carrier of V

K176(V,(T . A),(- (T . A9))) is Element of the carrier of V

A - A9 is Element of the carrier of W

- A9 is Element of the carrier of W

K176(W,A,(- A9)) is Element of the carrier of W

T . (A - A9) is Element of the carrier of V

1. F is V55(F) Element of the carrier of F

the carrier of F is non empty V2() set

the OneF of F is Element of the carrier of F

- (1. F) is Element of the carrier of F

(- (1. F)) * A9 is Element of the carrier of W

T . ((- (1. F)) * A9) is Element of the carrier of V

(- (1. F)) * (T . A9) is Element of the carrier of V

T . (- A9) is Element of the carrier of V

(T . A) + (T . (- A9)) is Element of the carrier of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

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

the ZeroF of V is Element of the carrier of V

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of V, the carrier of W) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of W)) is non empty set

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))

T . (0. V) is Element of the carrier of W

0. F is V55(F) Element of the carrier of F

the carrier of F is non empty V2() set

the ZeroF of F is Element of the carrier of F

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

(0. F) * (T . (0. V)) is Element of the carrier of W

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of V, the carrier of W) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of W)) is non empty set

T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

{ b

[#] V is non empty non proper Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

A9 is set

B is Element of the carrier of V

T . B is Element of the carrier of W

A9 is Element of K6( the carrier of V)

B is Element of the carrier of V

T . B is Element of the carrier of W

B is Element of the carrier of V

T . B is Element of the carrier of W

the carrier of F is non empty V2() set

B is Element of the carrier of V

T . B is Element of the carrier of W

B is Element of the carrier of F

B * B is Element of the carrier of V

T . (B * B) is Element of the carrier of W

B * (0. W) is Element of the carrier of W

B is Element of the carrier of V

B is Element of the carrier of F

B * B is Element of the carrier of V

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

the ZeroF of V is Element of the carrier of V

T . (0. V) is Element of the carrier of W

B is Element of the carrier of V

B is Element of the carrier of V

T . B is Element of the carrier of W

T . B is Element of the carrier of W

B + B is Element of the carrier of V

T . (B + B) is Element of the carrier of W

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

B is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

the carrier of B is non empty set

[#] B is non empty non proper Element of K6( the carrier of B)

K6( the carrier of B) is non empty set

A is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

[#] A is non empty non proper Element of K6( the carrier of A)

the carrier of A is non empty set

K6( the carrier of A) is non empty set

A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

[#] A9 is non empty non proper Element of K6( the carrier of A9)

the carrier of A9 is non empty set

K6( the carrier of A9) is non empty set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of V, the carrier of W) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of W)) is non empty set

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))

(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

A is Element of the carrier of V

T . A is Element of the carrier of W

[#] (F,V,W,T) is non empty non proper Element of K6( the carrier of (F,V,W,T))

the carrier of (F,V,W,T) is non empty set

K6( the carrier of (F,V,W,T)) is non empty set

{ b

A9 is Element of the carrier of V

T . A9 is Element of the carrier of W

{ b

[#] (F,V,W,T) is non empty non proper Element of K6( the carrier of (F,V,W,T))

the carrier of (F,V,W,T) is non empty set

K6( the carrier of (F,V,W,T)) is non empty set

F is non empty 1-sorted

the carrier of F is non empty set

V is non empty 1-sorted

the carrier of V is non empty set

K7( the carrier of F, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of F, the carrier of V)) is non empty set

K6( the carrier of F) is non empty set

W is Relation-like the carrier of F -defined the carrier of V -valued Function-like quasi_total Element of K6(K7( the carrier of F, the carrier of V))

T is Element of K6( the carrier of F)

W .: T is set

K6( the carrier of V) is non empty set

rng W is set

[#] V is non empty non proper Element of K6( the carrier of V)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of V, the carrier of W) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of W)) is non empty set

T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))

[#] V is non empty non proper Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

(V,W,T,([#] V)) is Element of K6( the carrier of W)

K6( the carrier of W) is non empty set

A is Element of K6( the carrier of W)

A9 is Element of the carrier of W

dom T is Element of K6( the carrier of V)

B is set

T . B is set

B is Element of the carrier of V

T . B is Element of the carrier of W

B is Element of the carrier of V

T . B is Element of the carrier of W

dom T is Element of K6( the carrier of V)

A9 is Element of the carrier of W

B is Element of the carrier of W

B is Element of the carrier of V

T . B is Element of the carrier of W

X is Element of the carrier of V

T . X is Element of the carrier of W

A9 + B is Element of the carrier of W

B + X is Element of the carrier of V

T . (B + X) is Element of the carrier of W

the carrier of F is non empty V2() set

B is Element of the carrier of W

B is Element of the carrier of V

T . B is Element of the carrier of W

A9 is Element of the carrier of F

A9 * B is Element of the carrier of V

T . (A9 * B) is Element of the carrier of W

A9 * B is Element of the carrier of W

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

the ZeroF of V is Element of the carrier of V

T . (0. V) is Element of the carrier of W

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

the carrier of A9 is non empty set

[#] A9 is non empty non proper Element of K6( the carrier of A9)

K6( the carrier of A9) is non empty set

A is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

[#] A is non empty non proper Element of K6( the carrier of A)

the carrier of A is non empty set

K6( the carrier of A) is non empty set

A9 is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

[#] A9 is non empty non proper Element of K6( the carrier of A9)

the carrier of A9 is non empty set

K6( the carrier of A9) is non empty set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

0. F is V55(F) Element of the carrier of F

the carrier of F is non empty V2() set

the ZeroF of F is Element of the carrier of F

(0. F) * (0. W) is Element of the carrier of W

T . (0. W) is Element of the carrier of V

(0. F) * (T . (0. W)) is Element of the carrier of V

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

the ZeroF of V is Element of the carrier of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

K6( the carrier of W) is non empty set

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

the carrier of (F,W,V,T) is non empty set

K6( the carrier of (F,W,V,T)) is non empty set

A is Element of K6( the carrier of W)

(W,V,T,A) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

[#] (F,W,V,T) is non empty non proper Element of K6( the carrier of (F,W,V,T))

[#] W is non empty non proper Element of K6( the carrier of W)

(W,V,T,([#] W)) is Element of K6( the carrier of V)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

A is Element of the carrier of V

the carrier of (F,W,V,T) is non empty set

[#] (F,W,V,T) is non empty non proper Element of K6( the carrier of (F,W,V,T))

K6( the carrier of (F,W,V,T)) is non empty set

[#] W is non empty non proper Element of K6( the carrier of W)

K6( the carrier of W) is non empty set

(W,V,T,([#] W)) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

dom T is Element of K6( the carrier of W)

A9 is Element of the carrier of (F,W,V,T)

B is set

T . B is set

B is Element of the carrier of W

T . B is Element of the carrier of V

dom T is Element of K6( the carrier of W)

K6( the carrier of W) is non empty set

[#] W is non empty non proper Element of K6( the carrier of W)

(W,V,T,([#] W)) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

A9 is Element of the carrier of W

T . A9 is Element of the carrier of V

[#] (F,W,V,T) is non empty non proper Element of K6( the carrier of (F,W,V,T))

the carrier of (F,W,V,T) is non empty set

K6( the carrier of (F,W,V,T)) is non empty set

A9 is Element of the carrier of W

T . A9 is Element of the carrier of V

B is Element of the carrier of W

T . B is Element of the carrier of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of V, the carrier of W) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of W)) is non empty set

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

T is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))

(F,V,W,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

the carrier of (F,V,W,T) is non empty set

A is Element of the carrier of (F,V,W,T)

T . A is set

A9 is Element of the carrier of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

(0). W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

the carrier of (F,W,V,T) is non empty set

A is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) Subspace of (F,W,V,T)

A9 is Element of the carrier of (F,W,V,T)

0. W is V55(W) Element of the carrier of W

the ZeroF of W is Element of the carrier of W

T . (0. W) is Element of the carrier of V

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

the ZeroF of V is Element of the carrier of V

dom T is Element of K6( the carrier of W)

K6( the carrier of W) is non empty set

[#] W is non empty non proper Element of K6( the carrier of W)

B is Element of the carrier of W

T . B is Element of the carrier of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) finite-dimensional VectSpStr over F

(0). V is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of V

dim ((0). V) is V4() V5() V6() V10() V11() ext-real finite cardinal V46() set

(Omega). ((0). V) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (0). V

the carrier of ((0). V) is non empty set

the U5 of ((0). V) is Relation-like K7( the carrier of ((0). V), the carrier of ((0). V)) -defined the carrier of ((0). V) -valued Function-like quasi_total Element of K6(K7(K7( the carrier of ((0). V), the carrier of ((0). V)), the carrier of ((0). V)))

K7( the carrier of ((0). V), the carrier of ((0). V)) is non empty Relation-like set

K7(K7( the carrier of ((0). V), the carrier of ((0). V)), the carrier of ((0). V)) is non empty Relation-like set

K6(K7(K7( the carrier of ((0). V), the carrier of ((0). V)), the carrier of ((0). V))) is non empty set

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

the lmult of ((0). V) is Relation-like K7( the carrier of F, the carrier of ((0). V)) -defined the carrier of ((0). V) -valued Function-like quasi_total Element of K6(K7(K7( the carrier of F, the carrier of ((0). V)), the carrier of ((0). V)))

the carrier of F is non empty V2() set

K7( the carrier of F, the carrier of ((0). V)) is non empty Relation-like set

K7(K7( the carrier of F, the carrier of ((0). V)), the carrier of ((0). V)) is non empty Relation-like set

K6(K7(K7( the carrier of F, the carrier of ((0). V)), the carrier of ((0). V))) is non empty set

VectSpStr(# the carrier of ((0). V), the U5 of ((0). V), the ZeroF of ((0). V), the lmult of ((0). V) #) is strict VectSpStr over F

(0). ((0). V) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) finite-dimensional Subspace of (0). V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

A is Element of the carrier of W

T . A is Element of the carrier of V

A9 is Element of the carrier of W

T . A9 is Element of the carrier of V

A - A9 is Element of the carrier of W

- A9 is Element of the carrier of W

K176(W,A,(- A9)) is Element of the carrier of W

T . (A - A9) is Element of the carrier of V

(T . A) - (T . A9) is Element of the carrier of V

- (T . A9) is Element of the carrier of V

K176(V,(T . A),(- (T . A9))) is Element of the carrier of V

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

the ZeroF of V is Element of the carrier of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Element of K6( the carrier of V)

Lin W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

T is Element of the carrier of V

A is Element of the carrier of V

T - A is Element of the carrier of V

- A is Element of the carrier of V

K176(V,T,(- A)) is Element of the carrier of V

{A} is non empty V2() finite 1 -element Element of K6( the carrier of V)

W \/ {A} is non empty Element of K6( the carrier of V)

Lin (W \/ {A}) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

Lin {A} is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

(Lin W) + (Lin {A}) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

(T - A) + A is Element of the carrier of V

A - A is Element of the carrier of V

K176(V,A,(- A)) is Element of the carrier of V

T - (A - A) is Element of the carrier of V

- (A - A) is Element of the carrier of V

K176(V,T,(- (A - A))) is Element of the carrier of V

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

the ZeroF of V is Element of the carrier of V

T - (0. V) is Element of the carrier of V

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

K176(V,T,(- (0. V))) is Element of the carrier of V

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K6( the carrier of W) is non empty set

T is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

[#] W is non empty non proper Element of K6( the carrier of W)

A is set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Element of K6( the carrier of V)

Lin W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

[#] (Lin W) is non empty non proper Element of K6( the carrier of (Lin W))

the carrier of (Lin W) is non empty set

K6( the carrier of (Lin W)) is non empty set

T is set

A is Element of the carrier of V

T is Element of K6( the carrier of (Lin W))

Lin T is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of Lin W

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Element of K6( the carrier of V)

Lin W is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of V

T is Element of the carrier of V

{T} is non empty V2() finite 1 -element Element of K6( the carrier of V)

W \/ {T} is non empty Element of K6( the carrier of V)

[#] (Lin W) is non empty non proper Element of K6( the carrier of (Lin W))

the carrier of (Lin W) is non empty set

K6( the carrier of (Lin W)) is non empty set

A9 is Basis of Lin W

A is Element of K6( the carrier of (Lin W))

A9 \/ A is Element of K6( the carrier of (Lin W))

B is set

B is Element of K6( the carrier of (Lin W))

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

K6( the carrier of W) is non empty set

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

(F,W,V,T) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

A is Element of K6( the carrier of W)

A9 is Basis of W

A9 \ A is Element of K6( the carrier of W)

T | (A9 \ A) is Relation-like the carrier of W -defined A9 \ A -defined the carrier of W -defined the carrier of V -valued Function-like Element of K6(K7( the carrier of W, the carrier of V))

X is set

dom (T | (A9 \ A)) is set

X is set

(T | (A9 \ A)) . X is set

(T | (A9 \ A)) . X is set

dom (T | (A9 \ A)) is Element of K6((A9 \ A))

K6((A9 \ A)) is non empty set

dom T is Element of K6( the carrier of W)

A is Element of the carrier of W

B is Element of K6( the carrier of W)

B is Element of the carrier of W

{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)

B \/ {B} is non empty Element of K6( the carrier of W)

(T | (A9 \ A)) . B is set

T . B is Element of the carrier of V

C is Basis of (F,W,V,T)

Lin C is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of (F,W,V,T)

(T | (A9 \ A)) . A is set

T . A is Element of the carrier of V

A - B is Element of the carrier of W

- B is Element of the carrier of W

K176(W,A,(- B)) is Element of the carrier of W

Lin B is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

Lin (B \/ {B}) is non empty V74() V99() V100() V101() strict V128(F) V129(F) V130(F) V131(F) Subspace of W

{A} is non empty V2() finite 1 -element Element of K6( the carrier of W)

{B} \/ {A} is non empty finite Element of K6( the carrier of W)

{A,B} is non empty finite Element of K6( the carrier of W)

(B \/ {B}) \/ {A} is non empty Element of K6( the carrier of W)

B \/ {A,B} is non empty Element of K6( the carrier of W)

C is set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Element of K6( the carrier of V)

T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W

A is Element of the carrier of V

{A} is non empty V2() finite 1 -element Element of K6( the carrier of V)

W \/ {A} is non empty Element of K6( the carrier of V)

A9 is Element of the carrier of F

T +* (A,A9) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Element of K6(K7( the carrier of V, the carrier of F))

K7( the carrier of V, the carrier of F) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of F)) is non empty set

dom (T +* (A,A9)) is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

rng (T +* (A,A9)) is set

[#] F is non empty non proper Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

B is set

X is set

(T +* (A,A9)) . X is set

dom T is Element of K6( the carrier of V)

T . X is set

rng T is set

Funcs (([#] V),([#] F)) is non empty FUNCTION_DOMAIN of [#] V, [#] F

Carrier T is finite Element of K6( the carrier of V)

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

{ b

(Carrier T) \/ {A} is non empty finite Element of K6( the carrier of V)

B is Relation-like [#] V -defined [#] F -valued Function-like quasi_total Element of Funcs (([#] V),([#] F))

X is Element of the carrier of V

B . X is set

T . X is Element of the carrier of F

X is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

Carrier X is finite Element of K6( the carrier of V)

{ b

B is set

A is Element of the carrier of V

X . A is Element of the carrier of F

T . A is Element of the carrier of F

F is 1-sorted

the carrier of F is set

K6( the carrier of F) is non empty set

[#] F is non proper Element of K6( the carrier of F)

V is Element of K6( the carrier of F)

([#] F) \ V is Element of K6( the carrier of F)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

the carrier of F is non empty V2() set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

T is Element of K6( the carrier of V)

W .: T is set

K6( the carrier of F) is non empty set

(V,F,W,T) is Element of K6( the carrier of F)

[#] F is non empty non proper Element of K6( the carrier of F)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

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

the ZeroF of V is Element of the carrier of V

{(0. V)} is non empty V2() finite 1 -element Element of K6( the carrier of V)

W is Element of K6( the carrier of V)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

the carrier of F is non empty V2() set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

T is Element of K6( the carrier of V)

W | T is Relation-like the carrier of V -defined T -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))

K7( the carrier of V, the carrier of F) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of F)) is non empty set

(V,T) is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

([#] V) \ T is Element of K6( the carrier of V)

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

(V,T) --> (0. F) is Relation-like (V,T) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,T), the carrier of F))

K7((V,T), the carrier of F) is Relation-like set

K6(K7((V,T), the carrier of F)) is non empty set

{(0. F)} is non empty V2() finite 1 -element set

K7((V,T),{(0. F)}) is Relation-like set

(W | T) +* ((V,T) --> (0. F)) is Relation-like Function-like set

dom ((W | T) +* ((V,T) --> (0. F))) is set

dom (W | T) is Element of K6(T)

K6(T) is non empty set

dom ((V,T) --> (0. F)) is Element of K6((V,T))

K6((V,T)) is non empty set

(dom (W | T)) \/ (dom ((V,T) --> (0. F))) is set

dom W is Element of K6( the carrier of V)

T \/ (([#] V) \ T) is Element of K6( the carrier of V)

rng ((W | T) +* ((V,T) --> (0. F))) is set

[#] F is non empty non proper Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

A9 is set

B is set

((W | T) +* ((V,T) --> (0. F))) . B is set

B is Element of the carrier of V

((W | T) +* ((V,T) --> (0. F))) . B is set

(W | T) . B is set

W . B is Element of the carrier of F

B is Element of the carrier of V

((W | T) +* ((V,T) --> (0. F))) . B is set

((V,T) --> (0. F)) . B is set

B is Element of the carrier of V

Funcs (([#] V),([#] F)) is non empty FUNCTION_DOMAIN of [#] V, [#] F

A9 is Relation-like [#] V -defined [#] F -valued Function-like quasi_total Element of Funcs (([#] V),([#] F))

{ b

B is set

X is Element of the carrier of V

A9 . X is set

Carrier W is finite Element of K6( the carrier of V)

{ b

B is Element of K6( the carrier of V)

X is set

B is Element of the carrier of V

A9 . B is set

((V,T) --> (0. F)) . B is set

(W | T) . B is set

W . B is Element of the carrier of F

X is finite Element of K6( the carrier of V)

B is Element of the carrier of V

A9 . B is set

B is finite Element of K6( the carrier of V)

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

Carrier B is finite Element of K6( the carrier of V)

{ b

B is set

X is Element of the carrier of V

B . X is Element of the carrier of F

((V,T) --> (0. F)) . X is set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

Carrier W is finite Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

{ b

(F,V,W,(Carrier W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of Carrier W

W | (Carrier W) is Relation-like the carrier of V -defined Carrier W -defined the carrier of V -defined the carrier of F -valued Function-like finite Element of K6(K7( the carrier of V, the carrier of F))

K7( the carrier of V, the carrier of F) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of F)) is non empty set

(V,(Carrier W)) is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

([#] V) \ (Carrier W) is Element of K6( the carrier of V)

(V,(Carrier W)) --> (0. F) is Relation-like (V,(Carrier W)) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,(Carrier W)), the carrier of F))

K7((V,(Carrier W)), the carrier of F) is Relation-like set

K6(K7((V,(Carrier W)), the carrier of F)) is non empty set

{(0. F)} is non empty V2() finite 1 -element set

K7((V,(Carrier W)),{(0. F)}) is Relation-like set

(W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F)) is Relation-like Function-like set

dom ((V,(Carrier W)) --> (0. F)) is Element of K6((V,(Carrier W)))

K6((V,(Carrier W))) is non empty set

dom W is Element of K6( the carrier of V)

dom (W | (Carrier W)) is finite Element of K6((Carrier W))

K6((Carrier W)) is non empty finite V38() set

(dom (W | (Carrier W))) \/ (dom ((V,(Carrier W)) --> (0. F))) is set

B is set

W . B is set

((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) . B is set

B is Element of the carrier of V

((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) . B is set

(W | (Carrier W)) . B is set

B is Element of the carrier of V

((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) . B is set

((V,(Carrier W)) --> (0. F)) . B is set

B is Element of the carrier of V

dom ((W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F))) is set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

T is Element of K6( the carrier of V)

(F,V,W,T) is Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

Carrier W is finite Element of K6( the carrier of V)

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

{ b

(F,V,W,(Carrier W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of Carrier W

W | (Carrier W) is Relation-like the carrier of V -defined Carrier W -defined the carrier of V -defined the carrier of F -valued Function-like finite Element of K6(K7( the carrier of V, the carrier of F))

K7( the carrier of V, the carrier of F) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of F)) is non empty set

(V,(Carrier W)) is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

([#] V) \ (Carrier W) is Element of K6( the carrier of V)

(V,(Carrier W)) --> (0. F) is Relation-like (V,(Carrier W)) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,(Carrier W)), the carrier of F))

K7((V,(Carrier W)), the carrier of F) is Relation-like set

K6(K7((V,(Carrier W)), the carrier of F)) is non empty set

{(0. F)} is non empty V2() finite 1 -element set

K7((V,(Carrier W)),{(0. F)}) is Relation-like set

(W | (Carrier W)) +* ((V,(Carrier W)) --> (0. F)) is Relation-like Function-like set

rng (W | (Carrier W)) is finite set

rng ((V,(Carrier W)) --> (0. F)) is V2() finite set

(rng (W | (Carrier W))) \/ (rng ((V,(Carrier W)) --> (0. F))) is finite set

rng W is set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

T is Element of K6( the carrier of V)

(F,V,W,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T

W | T is Relation-like the carrier of V -defined T -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))

K7( the carrier of V, the carrier of F) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of F)) is non empty set

(V,T) is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

([#] V) \ T is Element of K6( the carrier of V)

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

(V,T) --> (0. F) is Relation-like (V,T) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,T), the carrier of F))

K7((V,T), the carrier of F) is Relation-like set

K6(K7((V,T), the carrier of F)) is non empty set

{(0. F)} is non empty V2() finite 1 -element set

K7((V,T),{(0. F)}) is Relation-like set

(W | T) +* ((V,T) --> (0. F)) is Relation-like Function-like set

A is Element of the carrier of V

(F,V,W,T) . A is Element of the carrier of F

W . A is Element of the carrier of F

dom (F,V,W,T) is Element of K6( the carrier of V)

dom (W | T) is Element of K6(T)

K6(T) is non empty set

dom ((V,T) --> (0. F)) is Element of K6((V,T))

K6((V,T)) is non empty set

(dom (W | T)) \/ (dom ((V,T) --> (0. F))) is set

(W | T) . A is set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

T is Element of K6( the carrier of V)

(F,V,W,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T

W | T is Relation-like the carrier of V -defined T -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))

K7( the carrier of V, the carrier of F) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of F)) is non empty set

(V,T) is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

([#] V) \ T is Element of K6( the carrier of V)

(V,T) --> (0. F) is Relation-like (V,T) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,T), the carrier of F))

K7((V,T), the carrier of F) is Relation-like set

K6(K7((V,T), the carrier of F)) is non empty set

{(0. F)} is non empty V2() finite 1 -element set

K7((V,T),{(0. F)}) is Relation-like set

(W | T) +* ((V,T) --> (0. F)) is Relation-like Function-like set

A is Element of the carrier of V

(F,V,W,T) . A is Element of the carrier of F

dom (F,V,W,T) is Element of K6( the carrier of V)

dom ((V,T) --> (0. F)) is Element of K6((V,T))

K6((V,T)) is non empty set

dom (W | T) is Element of K6(T)

K6(T) is non empty set

(dom (W | T)) \/ (dom ((V,T) --> (0. F))) is set

((V,T) --> (0. F)) . A is set

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

T is Element of K6( the carrier of V)

W is Element of K6( the carrier of V)

T \ W is Element of K6( the carrier of V)

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

(F,V,A,W) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W

A | W is Relation-like the carrier of V -defined W -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))

K7( the carrier of V, the carrier of F) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of F)) is non empty set

(V,W) is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

([#] V) \ W is Element of K6( the carrier of V)

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

(V,W) --> (0. F) is Relation-like (V,W) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,W), the carrier of F))

K7((V,W), the carrier of F) is Relation-like set

K6(K7((V,W), the carrier of F)) is non empty set

{(0. F)} is non empty V2() finite 1 -element set

K7((V,W),{(0. F)}) is Relation-like set

(A | W) +* ((V,W) --> (0. F)) is Relation-like Function-like set

(F,V,A,(T \ W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of T \ W

A | (T \ W) is Relation-like the carrier of V -defined T \ W -defined the carrier of V -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of V, the carrier of F))

(V,(T \ W)) is Element of K6( the carrier of V)

([#] V) \ (T \ W) is Element of K6( the carrier of V)

(V,(T \ W)) --> (0. F) is Relation-like (V,(T \ W)) -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7((V,(T \ W)), the carrier of F))

K7((V,(T \ W)), the carrier of F) is Relation-like set

K6(K7((V,(T \ W)), the carrier of F)) is non empty set

K7((V,(T \ W)),{(0. F)}) is Relation-like set

(A | (T \ W)) +* ((V,(T \ W)) --> (0. F)) is Relation-like Function-like set

(F,V,A,W) + (F,V,A,(T \ W)) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

B is Element of the carrier of V

A . B is set

((F,V,A,W) + (F,V,A,(T \ W))) . B is set

W \/ (T \ W) is Element of K6( the carrier of V)

(F,V,A,(T \ W)) . B is Element of the carrier of F

(F,V,A,W) . B is Element of the carrier of F

A . B is Element of the carrier of F

((F,V,A,W) + (F,V,A,(T \ W))) . B is Element of the carrier of F

(A . B) + (0. F) is Element of the carrier of F

(F,V,A,W) . B is Element of the carrier of F

(F,V,A,(T \ W)) . B is Element of the carrier of F

A . B is Element of the carrier of F

((F,V,A,W) + (F,V,A,(T \ W))) . B is Element of the carrier of F

(0. F) + (A . B) is Element of the carrier of F

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

{ b

(F,V,A,(T \ W)) . B is Element of the carrier of F

(F,V,A,W) . B is Element of the carrier of F

((F,V,A,W) + (F,V,A,(T \ W))) . B is Element of the carrier of F

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

A . B is Element of the carrier of F

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

the carrier of F is non empty V2() set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

T is Element of K6( the carrier of V)

(F,V,W,T) is Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

F is non empty 1-sorted

the carrier of F is non empty set

V is non empty 1-sorted

the carrier of V is non empty set

K7( the carrier of F, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of F, the carrier of V)) is non empty set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of F -defined the carrier of V -valued Function-like quasi_total Element of K6(K7( the carrier of F, the carrier of V))

T is Element of K6( the carrier of V)

W " T is set

K6( the carrier of F) is non empty set

dom W is Element of K6( the carrier of F)

[#] F is non empty non proper Element of K6( the carrier of F)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

K6( the carrier of V) is non empty set

W is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

Carrier W is finite Element of K6( the carrier of V)

{ b

T is Element of K6( the carrier of V)

(F,V,W,T) is finite Element of K6( the carrier of F)

A9 is set

dom W is Element of K6( the carrier of V)

B is set

W . B is set

B is Element of the carrier of V

W . B is Element of the carrier of F

(Carrier W) /\ T is finite Element of K6( the carrier of V)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

the carrier of F is non empty V2() set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of V, the carrier of W) is non empty Relation-like set

K6(K7( the carrier of V, the carrier of W)) is non empty set

T is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

A is Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of V, the carrier of W))

[#] W is non empty non proper Element of K6( the carrier of W)

K6( the carrier of W) is non empty set

A9 is set

B is Element of the carrier of W

{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{B}) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

(F,V,T,(V,W,A,{B})) is finite Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

Sum (F,V,T,(V,W,A,{B})) is Element of the carrier of F

A9 is Relation-like Function-like set

dom A9 is set

rng A9 is set

[#] F is non empty non proper Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

B is set

B is set

A9 . B is set

X is Element of the carrier of W

{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{X}) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)

Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F

B is Element of the carrier of W

A9 . B is set

{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{B}) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

(F,V,T,(V,W,A,{B})) is finite Element of K6( the carrier of F)

Sum (F,V,T,(V,W,A,{B})) is Element of the carrier of F

B is Element of the carrier of W

{B} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{B}) is Element of K6( the carrier of V)

(F,V,T,(V,W,A,{B})) is finite Element of K6( the carrier of F)

Sum (F,V,T,(V,W,A,{B})) is Element of the carrier of F

Funcs (([#] W),([#] F)) is non empty FUNCTION_DOMAIN of [#] W, [#] F

B is Relation-like [#] W -defined [#] F -valued Function-like quasi_total Element of Funcs (([#] W),([#] F))

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

{ b

X is set

X is Element of the carrier of W

B . X is set

Carrier T is finite Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

{ b

(V,W,A,(Carrier T)) is finite Element of K6( the carrier of W)

X is Element of K6( the carrier of W)

B is Element of K6( the carrier of W)

A is set

C is Element of the carrier of W

B . C is set

{C} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{C}) is Element of K6( the carrier of V)

(F,V,T,(V,W,A,{C})) is finite Element of K6( the carrier of F)

{(0. F)} is non empty V2() finite 1 -element Element of K6( the carrier of F)

Sum (F,V,T,(V,W,A,{C})) is Element of the carrier of F

{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)

{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)

C is set

L is set

{} F is empty proper V4() V5() V6() V8() V9() V10() V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() Element of K6( the carrier of F)

C is set

dom A is Element of K6( the carrier of V)

[#] V is non empty non proper Element of K6( the carrier of V)

L is Element of the carrier of V

A . L is Element of the carrier of W

A is finite Element of K6( the carrier of W)

C is Element of the carrier of W

B . C is set

X is finite Element of K6( the carrier of W)

B is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W

X is Element of the carrier of W

B . X is Element of the carrier of F

{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{X}) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)

Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F

X is Element of the carrier of W

{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{X}) is Element of K6( the carrier of V)

(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)

Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F

X is Element of the carrier of W

B . X is Element of the carrier of F

{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{X}) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)

Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F

A9 is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W

B is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W

dom A9 is Element of K6( the carrier of W)

K6( the carrier of W) is non empty set

B is set

A9 . B is set

B . B is set

X is Element of the carrier of W

A9 . X is Element of the carrier of F

{X} is non empty V2() finite 1 -element Element of K6( the carrier of W)

(V,W,A,{X}) is Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

(F,V,T,(V,W,A,{X})) is finite Element of K6( the carrier of F)

K6( the carrier of F) is non empty set

Sum (F,V,T,(V,W,A,{X})) is Element of the carrier of F

[#] W is non empty non proper Element of K6( the carrier of W)

dom B is Element of K6( the carrier of W)

F is non empty non degenerated V53() V74() V94() V99() V100() V101() V117() V119() well-unital V125() L11()

the carrier of F is non empty V2() set

V is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of V is non empty set

W is non empty V74() V99() V100() V101() V128(F) V129(F) V130(F) V131(F) VectSpStr over F

the carrier of W is non empty set

K7( the carrier of W, the carrier of V) is non empty Relation-like set

K6(K7( the carrier of W, the carrier of V)) is non empty set

T is Relation-like the carrier of W -defined the carrier of V -valued Function-like quasi_total additive homogeneous Element of K6(K7( the carrier of W, the carrier of V))

A is Relation-like the carrier of W -defined the carrier of F -valued Function-like quasi_total Linear_Combination of W

(F,W,V,A,T) is Relation-like the carrier of V -defined the carrier of F -valued Function-like quasi_total Linear_Combination of V

Carrier A is finite Element of K6( the carrier of W)

K6( the carrier of W) is non empty set

0. F is V55(F) Element of the carrier of F

the ZeroF of F is Element of the carrier of F

{ b

(W,V,T,(Carrier A)) is finite Element of K6( the carrier of V)

K6( the carrier of V) is non empty set

Carrier (F,W,V,A,T) is finite Element of K6( the carrier of V)

{ b

A9 is set

B is Element of the carrier of V

(F,W,V,A,T) . B is Element of the carrier of F

{B} is non empty V2() finite 1 -element Element of K6( the carrier of V)

(W