:: RUSUB_4 semantic presentation

REAL is set
NAT is non empty V5() V7() V8() V9() non finite cardinal limit_cardinal Element of K11(REAL)
K11(REAL) is non empty set
NAT is non empty V5() V7() V8() V9() non finite cardinal limit_cardinal set
K11(NAT) is non empty V5() non finite set
K11(NAT) is non empty V5() non finite set

RAT is set
INT is set
{} is set

2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
K12(NAT,REAL) is set
K11(K12(NAT,REAL)) is non empty set
1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
3 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
0 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card {} is V7() V8() V9() cardinal set
0 " is ext-real non negative V14() V15() set

the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
N is finite Element of K11( the carrier of V)
M \/ N is finite Element of K11( the carrier of V)

x is Element of the carrier of V
{x} is non empty V5() finite 1 -element Element of K11( the carrier of V)
y is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of M \/ N
Sum y is Element of the carrier of V

a is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of {x}
Sum a is Element of the carrier of V
Carrier y is finite Element of K11( the carrier of V)
u1 is set
v1 is Element of the carrier of V
y . v1 is ext-real V14() V15() Element of REAL
u1 is Element of the carrier of V
y . u1 is ext-real V14() V15() Element of REAL
u1 is Element of the carrier of V
y . u1 is ext-real V14() V15() Element of REAL
v1 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v1 is finite set
y (#) v1 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (y (#) v1) is Element of the carrier of V

u2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng u2 is finite set
v2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v2 is finite set
u2 ^ v2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng (u2 ^ v2) is finite set
(rng (u2 ^ v2)) /\ () is finite Element of K11( the carrier of V)
y (#) (u2 ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
Carrier A is finite Element of K11( the carrier of V)
A (#) (u2 ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
{u1} is non empty V5() finite 1 -element Element of K11( the carrier of V)

() \ {u1} is finite Element of K11( the carrier of V)
(M \/ N) \ {u1} is finite Element of K11( the carrier of V)
((M \/ N) \ {u1}) \/ {x} is finite Element of K11( the carrier of V)

(y . u1) " is ext-real V14() V15() Element of REAL
<*u1*> is non empty V5() V16() V19( NAT ) V20( the carrier of V) Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(v1 -| u1) ^ <*u1*> is non empty V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
((v1 -| u1) ^ <*u1*>) ^ (v1 |-- u1) is non empty V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
<*u1*> ^ v2 is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
u2 ^ (<*u1*> ^ v2) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) u2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) (<*u1*> ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ (y (#) (<*u1*> ^ v2)) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) <*u1*> is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) v2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) <*u1*>) ^ (y (#) v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ ((y (#) <*u1*>) ^ (y (#) v2)) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ (y (#) <*u1*>) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
((y (#) u2) ^ (y (#) <*u1*>)) ^ (y (#) v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y . u1) * u1 is Element of the carrier of V
<*((y . u1) * u1)*> is non empty V5() V16() V19( NAT ) V20( the carrier of V) Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ <*((y . u1) * u1)*> is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
((y (#) u2) ^ <*((y . u1) * u1)*>) ^ (y (#) v2) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*((y . u1) * u1)*> ^ (y (#) v2) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ (<*((y . u1) * u1)*> ^ (y (#) v2)) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((y (#) u2) ^ (<*((y . u1) * u1)*> ^ (y (#) v2))) is Element of the carrier of V
Sum (y (#) u2) is Element of the carrier of V
Sum (<*((y . u1) * u1)*> ^ (y (#) v2)) is Element of the carrier of V
(Sum (y (#) u2)) + (Sum (<*((y . u1) * u1)*> ^ (y (#) v2))) is Element of the carrier of V
Sum <*((y . u1) * u1)*> is Element of the carrier of V
Sum (y (#) v2) is Element of the carrier of V
(Sum <*((y . u1) * u1)*>) + (Sum (y (#) v2)) is Element of the carrier of V
(Sum (y (#) u2)) + ((Sum <*((y . u1) * u1)*>) + (Sum (y (#) v2))) is Element of the carrier of V
(Sum (y (#) v2)) + ((y . u1) * u1) is Element of the carrier of V
(Sum (y (#) u2)) + ((Sum (y (#) v2)) + ((y . u1) * u1)) is Element of the carrier of V
(Sum (y (#) u2)) + (Sum (y (#) v2)) is Element of the carrier of V
((Sum (y (#) u2)) + (Sum (y (#) v2))) + ((y . u1) * u1) is Element of the carrier of V
(y (#) u2) ^ (y (#) v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((y (#) u2) ^ (y (#) v2)) is Element of the carrier of V
(Sum ((y (#) u2) ^ (y (#) v2))) + ((y . u1) * u1) is Element of the carrier of V
Sum (y (#) (u2 ^ v2)) is Element of the carrier of V
(Sum (y (#) (u2 ^ v2))) + ((y . u1) * u1) is Element of the carrier of V
A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of (M \/ N) \ {u1}
- A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
(- A9) + a is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
Carrier ((- A9) + a) is finite Element of K11( the carrier of V)
Carrier (- A9) is finite Element of K11( the carrier of V)
Carrier a is finite Element of K11( the carrier of V)
(Carrier (- A9)) \/ () is finite Element of K11( the carrier of V)
Carrier A9 is finite Element of K11( the carrier of V)
(Carrier A9) \/ () is finite Element of K11( the carrier of V)
((y . u1) ") * ((- A9) + a) is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
Carrier (((y . u1) ") * ((- A9) + a)) is finite Element of K11( the carrier of V)
A9 (#) (u2 ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (A9 (#) (u2 ^ v2)) is Element of the carrier of V
Sum A9 is Element of the carrier of V
((y . u1) ") * x is Element of the carrier of V
((y . u1) ") * (Sum A9) is Element of the carrier of V
((y . u1) ") * ((y . u1) * u1) is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + (((y . u1) ") * ((y . u1) * u1)) is Element of the carrier of V
((y . u1) ") * (y . u1) is ext-real V14() V15() Element of REAL
(((y . u1) ") * (y . u1)) * u1 is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + ((((y . u1) ") * (y . u1)) * u1) is Element of the carrier of V
1 * u1 is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + (1 * u1) is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + u1 is Element of the carrier of V
(((y . u1) ") * x) - (((y . u1) ") * (Sum A9)) is Element of the carrier of V
x - (Sum A9) is Element of the carrier of V
((y . u1) ") * (x - (Sum A9)) is Element of the carrier of V
- (Sum A9) is Element of the carrier of V
(- (Sum A9)) + x is Element of the carrier of V
((y . u1) ") * ((- (Sum A9)) + x) is Element of the carrier of V
Sum (- A9) is Element of the carrier of V
(Sum (- A9)) + (Sum a) is Element of the carrier of V
((y . u1) ") * ((Sum (- A9)) + (Sum a)) is Element of the carrier of V
Sum ((- A9) + a) is Element of the carrier of V
((y . u1) ") * (Sum ((- A9) + a)) is Element of the carrier of V
Sum (((y . u1) ") * ((- A9) + a)) is Element of the carrier of V
V is set
M is set
{M} is non empty V5() finite 1 -element set
V \ {M} is Element of K11(V)
K11(V) is non empty set
(V \ {M}) \/ {M} is set
{M} \/ (V \ {M}) is set
{M} \/ V is set
V is set
M is set
{M} is non empty V5() finite 1 -element set
V \ {M} is Element of K11(V)
K11(V) is non empty set
V /\ {M} is finite set
N is set

the carrier of V is non empty set
K11( the carrier of V) is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N - (M + 1) is ext-real V14() V15() set
x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is finite Element of K11( the carrier of V)
card y is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

a is set
u1 is Element of the carrier of V
{u1} is non empty V5() finite 1 -element Element of K11( the carrier of V)
y \ {u1} is finite Element of K11( the carrier of V)
K11(y) is non empty finite V37() set
card (y \ {u1}) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card {u1} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card y) - (card {u1}) is ext-real V14() V15() set
(M + 1) - 1 is ext-real V14() V15() Element of REAL
N - M is ext-real V14() V15() set
u2 is finite Element of K11( the carrier of V)
card u2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(y \ {u1}) \/ u2 is finite Element of K11( the carrier of V)

M - M is ext-real V14() V15() set
v2 is finite Element of K11( the carrier of V)
card v2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(y \ {u1}) \/ v2 is finite Element of K11( the carrier of V)

u2 \/ (y \ {u1}) is finite Element of K11( the carrier of V)
v2 is Element of the carrier of V
{v2} is non empty V5() finite 1 -element Element of K11( the carrier of V)
(u2 \/ (y \ {u1})) \ {v2} is finite Element of K11( the carrier of V)
((u2 \/ (y \ {u1})) \ {v2}) \/ {u1} is finite Element of K11( the carrier of V)

u2 \ {v2} is finite Element of K11( the carrier of V)
(y \ {u1}) \ {v2} is finite Element of K11( the carrier of V)
((y \ {u1}) \ {v2}) \/ {u1} is finite Element of K11( the carrier of V)
(y \ {u1}) \/ {u1} is finite Element of K11( the carrier of V)
(u2 \ {v2}) \/ (((y \ {u1}) \ {v2}) \/ {u1}) is finite Element of K11( the carrier of V)
(u2 \ {v2}) \/ ((y \ {u1}) \/ {u1}) is finite Element of K11( the carrier of V)
y \/ (u2 \ {v2}) is finite Element of K11( the carrier of V)
K11(u2) is non empty finite V37() set
card (u2 \ {v2}) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card {v2} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card u2) - (card {v2}) is ext-real V14() V15() set
(N - M) - 1 is ext-real V14() V15() Element of REAL
N - (M + 1) is ext-real V14() V15() Element of REAL
(u2 \ {v2}) \/ ((y \ {u1}) \ {v2}) is finite Element of K11( the carrier of V)
((u2 \ {v2}) \/ ((y \ {u1}) \ {v2})) \/ {u1} is finite Element of K11( the carrier of V)

(u2 \ {v2}) \/ {v2} is finite Element of K11( the carrier of V)
A is set
the carrier of (Lin (y \/ (u2 \ {v2}))) is non empty set
the carrier of (Lin ((y \ {u1}) \/ u2)) is non empty set
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M - 0 is ext-real V14() V15() set
N is finite Element of K11( the carrier of V)
card N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

x \/ N is finite Element of K11( the carrier of V)
M is finite Element of K11( the carrier of V)

N is finite Element of K11( the carrier of V)
card N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card M) - (card N) is ext-real V14() V15() set

the carrier of () is non empty set
K11( the carrier of ()) is non empty set
{} the carrier of () is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of ())
M is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of ())

the ZeroF of () is Element of the carrier of ()
the addF of () is V16() V19(K12( the carrier of (), the carrier of ())) V20( the carrier of ()) Function-like quasi_total Element of K11(K12(K12( the carrier of (), the carrier of ()), the carrier of ()))
K12( the carrier of (), the carrier of ()) is non empty set
K12(K12( the carrier of (), the carrier of ()), the carrier of ()) is non empty set
K11(K12(K12( the carrier of (), the carrier of ()), the carrier of ())) is non empty set
the Mult of () is V16() V19(K12(REAL, the carrier of ())) V20( the carrier of ()) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of ()), the carrier of ()))
K12(REAL, the carrier of ()) is set
K12(K12(REAL, the carrier of ()), the carrier of ()) is set
K11(K12(K12(REAL, the carrier of ()), the carrier of ())) is non empty set
the scalar of () is V16() V19(K12( the carrier of (), the carrier of ())) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of (), the carrier of ()),REAL))
K12(K12( the carrier of (), the carrier of ()),REAL) is set
K11(K12(K12( the carrier of (), the carrier of ()),REAL)) is non empty set
UNITSTR(# the carrier of (), the ZeroF of (), the addF of (), the Mult of (), the scalar of () #) is strict UNITSTR

the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
N is Basis of V

rng x is finite set
y is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom y is finite Element of K11(NAT)
{ (Carrier b1) where b1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N : ex b2 being ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT st
( b2 in dom y & Sum b1 = y . b2 )
}
is set

union { (Carrier b1) where b1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N : ex b2 being ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT st
( b2 in dom y & Sum b1 = y . b2 )
}
is set

v1 is set
u2 is set
v2 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier v2 is finite Element of K11( the carrier of V)
I1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Sum v2 is Element of the carrier of V
y . I1 is set

v1 is Element of K11( the carrier of V)

u2 is Element of the carrier of V
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR

v2 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of M
Sum v2 is Element of the carrier of V
Carrier v2 is finite Element of K11( the carrier of V)
the carrier of (Lin v1) is non empty set
I1 is set

A is Element of the carrier of V
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Sum A is Element of the carrier of V
Carrier A is finite Element of K11( the carrier of V)
A9 is set
y . A9 is set
A9 is set
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of v1
Sum I1 is Element of the carrier of V
the carrier of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is set
the carrier of () is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
N \ v1 is Element of K11( the carrier of V)
I1 is set
I1 is Element of K11( the carrier of V)
I1 \ v1 is Element of K11( the carrier of V)
v1 \/ (I1 \ v1) is Element of K11( the carrier of V)
v1 \/ I1 is Element of K11( the carrier of V)
v2 is non empty Element of K11( the carrier of V)
v1 \/ v2 is Element of K11( the carrier of V)
len y is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Seg (len y) is finite len y -element Element of K11(NAT)
u2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal set
y . u2 is set

v2 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Sum v2 is Element of the carrier of V
Carrier v2 is finite Element of K11( the carrier of V)
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier I1 is finite Element of K11( the carrier of V)
Sum I1 is Element of the carrier of V

dom u2 is finite Element of K11(NAT)

dom u2 is finite Element of K11(NAT)
v2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal set
y . v2 is set
I1 is set
A is set
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A is finite Element of K11( the carrier of V)
Sum A is Element of the carrier of V
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A is finite Element of K11( the carrier of V)
Sum A is Element of the carrier of V
A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A9 is finite Element of K11( the carrier of V)
Sum A9 is Element of the carrier of V
A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A9 is finite Element of K11( the carrier of V)
Sum A9 is Element of the carrier of V
v2 is set
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier I1 is finite Element of K11( the carrier of V)
Sum I1 is Element of the carrier of V
A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y . A is set
A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y . A is set
u2 . A is set
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A is finite Element of K11( the carrier of V)
Sum A is Element of the carrier of V
rng u2 is finite set
v2 is set
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier I1 is finite Element of K11( the carrier of V)
A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Sum I1 is Element of the carrier of V
y . A is set

the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is Element of K11( the carrier of V)
N is Basis of V

M is Basis of V
card M is V7() V8() V9() cardinal set
N is Basis of V
card N is V7() V8() V9() cardinal set
the carrier of V is non empty set
K11( the carrier of V) is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR

x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is finite Element of K11( the carrier of V)
card y is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

the carrier of M is non empty set
K11( the carrier of M) is non empty set
{} the carrier of M is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of M)
the carrier of V is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty V5() finite 1 -element Element of K11( the carrier of V)
K11( the carrier of V) is non empty set
0. M is V64(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
{(0. M)} is non empty V5() finite 1 -element Element of K11( the carrier of M)

the carrier of ((0). M) is non empty set
N is finite Element of K11( the carrier of M)

the Basis of M is Basis of M
x is Basis of V

the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is Basis of V
card x is V7() V8() V9() cardinal set
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
K11( the carrier of V) is non empty set
x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the Basis of M is Basis of M
the carrier of M is non empty set
K11( the carrier of M) is non empty set
x is Element of K11( the carrier of M)
the carrier of V is non empty set
K11( the carrier of V) is non empty set
y is linearly-independent Element of K11( the carrier of V)

the Basis of u1 is Basis of u1

the carrier of u1 is non empty set
the ZeroF of u1 is Element of the carrier of u1
the addF of u1 is V16() V19(K12( the carrier of u1, the carrier of u1)) V20( the carrier of u1) Function-like quasi_total Element of K11(K12(K12( the carrier of u1, the carrier of u1), the carrier of u1))
K12( the carrier of u1, the carrier of u1) is non empty set
K12(K12( the carrier of u1, the carrier of u1), the carrier of u1) is non empty set
K11(K12(K12( the carrier of u1, the carrier of u1), the carrier of u1)) is non empty set
the Mult of u1 is V16() V19(K12(REAL, the carrier of u1)) V20( the carrier of u1) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of u1), the carrier of u1))
K12(REAL, the carrier of u1) is set
K12(K12(REAL, the carrier of u1), the carrier of u1) is set
K11(K12(K12(REAL, the carrier of u1), the carrier of u1)) is non empty set
the scalar of u1 is V16() V19(K12( the carrier of u1, the carrier of u1)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of u1, the carrier of u1),REAL))
K12(K12( the carrier of u1, the carrier of u1),REAL) is set
K11(K12(K12( the carrier of u1, the carrier of u1),REAL)) is non empty set
UNITSTR(# the carrier of u1, the ZeroF of u1, the addF of u1, the Mult of u1, the scalar of u1 #) is strict UNITSTR
u2 is finite Element of K11( the carrier of V)
card u2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
a is finite Element of K11( the carrier of V)
card a is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is Element of K11( the carrier of V)
card M is V7() V8() V9() cardinal set

((Lin M)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is set
the carrier of (Lin M) is non empty set
K11( the carrier of (Lin M)) is non empty set
x is linearly-independent Element of K11( the carrier of (Lin M))

y is Basis of Lin M
card y is V7() V8() V9() cardinal set

(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

(()) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR

card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

the carrier of V is non empty set
K11( the carrier of V) is non empty set
N is finite Element of K11( the carrier of V)
the Basis of M is Basis of M
y is Basis of V
the carrier of M is non empty set
card the Basis of M is V7() V8() V9() cardinal set
card y is V7() V8() V9() cardinal set
u1 is finite Element of K11( the carrier of V)
card u1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
a is finite Element of K11( the carrier of V)
card a is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
K11( the carrier of M) is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
v1 is Element of K11( the carrier of V)

u2 is Element of K11( the carrier of M)

the ZeroF of M is Element of the carrier of M
the addF of M is V16() V19(K12( the carrier of M, the carrier of M)) V20( the carrier of M) Function-like quasi_total Element of K11(K12(K12( the carrier of M, the carrier of M), the carrier of M))
K12( the carrier of M, the carrier of M) is non empty set
K12(K12( the carrier of M, the carrier of M), the carrier of M) is non empty set
K11(K12(K12( the carrier of M, the carrier of M), the carrier of M)) is non empty set
the Mult of M is V16() V19(K12(REAL, the carrier of M)) V20( the carrier of M) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of M), the carrier of M))
K12(REAL, the carrier of M) is set
K12(K12(REAL, the carrier of M), the carrier of M) is set
K11(K12(K12(REAL, the carrier of M), the carrier of M)) is non empty set
the scalar of M is V16() V19(K12( the carrier of M, the carrier of M)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of M, the carrier of M),REAL))
K12(K12( the carrier of M, the carrier of M),REAL) is set
K11(K12(K12( the carrier of M, the carrier of M),REAL)) is non empty set
UNITSTR(# the carrier of M, the ZeroF of M, the addF of M, the Mult of M, the scalar of M #) is strict UNITSTR
x is finite Element of K11( the carrier of M)

a is Element of K11( the carrier of V)
card a is V7() V8() V9() cardinal set
y is Element of K11( the carrier of M)

((Lin y)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card y is V7() V8() V9() cardinal set

(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
N is finite Element of K11( the carrier of V)
card N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
{} the carrier of V is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of V)
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR

0. V is V64(V) Element of the carrier of V
{(0. V)} is non empty V5() finite 1 -element Element of K11( the carrier of V)

(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V

K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is set
{N} is non empty V5() finite 1 -element set
x is Element of the carrier of V
{x} is non empty V5() finite 1 -element Element of K11( the carrier of V)

the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
M is Element of the carrier of V
{M} is non empty V5() finite 1 -element Element of K11( the carrier of V)

card {M} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set

K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is set
x is Element of the carrier of V
{x} is non empty V5() finite 1 -element Element of K11( the carrier of V)
card {x} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is set
a is Element of the carrier of V
{x,a} is finite Element of K11( the carrier of V)
u1 is set
{x,a,u1} is non empty finite set
v1 is set
card {x,a,u1} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
u1 is set

the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
M is Element of the carrier of V
N is Element of the carrier of V
{M,N} is finite Element of K11( the carrier of V)

card {M,N} is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

((M + N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

((M /\ N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((M + N)) + ((M /\ N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(M) + (N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT

the carrier of (y /\ a) is non empty set
K11( the carrier of (y /\ a)) is non empty set
u1 is finite Element of K11( the carrier of (y /\ a))
v1 is Basis of a
u2 is Basis of y
the carrier of a is non empty set
K11( the carrier of a) is non empty set
the carrier of y is non empty set
K11( the carrier of y) is non empty set
I1 is finite Element of K11( the carrier of y)
the carrier of x is non empty set
K11( the carrier of x) is non empty set
v2 is finite Element of K11( the carrier of a)
I1 /\ v2 is finite Element of K11( the carrier of a)
A9 is set

the ZeroF of y is Element of the carrier of y
the addF of y is V16() V19(K12( the carrier of y, the carrier of y)) V20( the carrier of y) Function-like quasi_total Element of K11(K12(K12( the carrier of y, the carrier of y), the carrier of y))
K12( the carrier of y, the carrier of y) is non empty set
K12(K12( the carrier of y, the carrier of y), the carrier of y) is non empty set
K11(K12(K12( the carrier of y, the carrier of y), the carrier of y)) is non empty set
the Mult of y is V16() V19(K12(REAL, the carrier of y)) V20( the carrier of y) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of y), the carrier of y))
K12(REAL, the carrier of y) is set
K12(K12(REAL, the carrier of y), the carrier of y) is set
K11(K12(K12(REAL, the carrier of y), the carrier of y)) is non empty set
the scalar of y is V16() V19(K12( the carrier of y, the carrier of y)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of y, the carrier of y),REAL))
K12(K12( the carrier of y, the carrier of y),REAL) is set
K11(K12(K12( the carrier of y, the carrier of y),REAL)) is non empty set
UNITSTR(# the carrier of y, the ZeroF of y, the addF of y, the Mult of y, the scalar of y #) is strict UNITSTR
w1 is set
{A9} is non empty V5() finite 1 -element set
u1 \/ {A9} is finite set
w2 is set
A is linearly-independent Element of K11( the carrier of x)
w1 is Element of K11( the carrier of x)
x is Element of the carrier of x

the ZeroF of a is Element of the carrier of a
the addF of a is V16() V19(K12( the carrier of a, the carrier of a)) V20( the carrier of a) Function-like quasi_total Element of K11(K12(K12( the carrier of a, the carrier of a), the carrier of a))
K12( the carrier of a, the carrier of a) is non empty set
K12(K12( the carrier of a, the carrier of a), the carrier of a) is non empty set
K11(K12(K12( the carrier of a, the carrier of a), the carrier of a)) is non empty set
the Mult of a is V16() V19(K12(REAL, the carrier of a)) V20( the carrier of a) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of a), the carrier of a))
K12(REAL, the carrier of a) is set
K12(K12(REAL, the carrier of a), the carrier of a) is set
K11(K12(K12(REAL, the carrier of a), the carrier of a)) is non empty set
the scalar of a is V16() V19(K12( the carrier of a, the carrier of a)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of a, the carrier of a),REAL))
K12(K12( the carrier of a, the carrier of a),REAL) is set
K11(K12(K12( the carrier of a, the carrier of a),REAL)) is non empty set
UNITSTR(# the carrier of a, the ZeroF of a, the addF of a, the Mult of a, the scalar of a #) is strict UNITSTR
the carrier of y /\ the carrier of a is set
the ZeroF of (y /\ a) is Element of the carrier of (y /\ a)
the addF of (y /\ a) is V16() V19(K12( the carrier of (y /\ a), the carrier of (y /\ a))) V20( the carrier of (y /\ a)) Function-like quasi_total Element of K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)), the carrier of (y /\ a)))
K12( the carrier of (y /\ a), the carrier of (y /\ a)) is non empty set
K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)), the carrier of (y /\ a)) is non empty set
K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)), the carrier of (y /\ a))) is non empty set
the Mult of (y /\ a) is V16() V19(K12(REAL, the carrier of (y /\ a))) V20( the carrier of (y /\ a)) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of (y /\ a)), the carrier of (y /\ a)))
K12(REAL, the carrier of (y /\ a)) is set
K12(K12(REAL, the carrier of (y /\ a)), the carrier of (y /\ a)) is set
K11(K12(K12(REAL, the carrier of (y /\ a)), the carrier of (y /\ a))) is non empty set
the scalar of (y /\ a) is V16() V19(K12( the carrier of (y /\ a), the carrier of (y /\ a))) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)),REAL))
K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)),REAL) is set
K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)),REAL)) is non empty set
UNITSTR(# the carrier of (y /\ a), the ZeroF of (y /\ a), the addF of (y /\ a), the Mult of (y /\ a), the scalar of (y /\ a) #) is strict UNITSTR

w1 \ {A9} is Element of K11( the carrier of x)
u1 \ {A9} is finite Element of K11( the carrier of (y /\ a))
A is Element of K11( the carrier of x)

I1 \/ v2 is finite set
A is set
A9 is Element of the carrier of x

the carrier of (y + a) is non empty set
K11( the carrier of (y + a)) is non empty set
A is finite Element of K11( the carrier of (y + a))
card A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card I1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card v2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card I1) + (card v2) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card u1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((card I1) + (card v2)) - (card u1) is ext-real V14() V15() Element of REAL