REAL is non empty non trivial non finite V120() V121() V122() V126() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() Element of bool REAL
bool REAL is non empty non trivial non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V120() V121() V122() V123() V124() V125() V126() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V120() V126() set
RAT is non empty non trivial non finite V120() V121() V122() V123() V126() set
INT is non empty non trivial non finite V120() V121() V122() V123() V124() V126() set
{} is set
the functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() set is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() set
2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
[:NAT,REAL:] is non empty non trivial non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
Seg 1 is non empty trivial finite 1 -element V120() V121() V122() V123() V124() V125() Element of bool NAT
0 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
- 1 is ext-real V25() V26() Element of REAL
K64(0) is V25() set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 : verum } is set
v is set
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum x is Element of the carrier of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
v is Element of bool the carrier of V
u is Element of the carrier of V
r2 is Element of the carrier of V
u + r2 is Element of the carrier of V
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum r3 is Element of the carrier of V
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum r4 is Element of the carrier of V
r3 + r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum t is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
r2 is Element of the carrier of V
u * r2 is Element of the carrier of V
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum r3 is Element of the carrier of V
u * r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum r4 is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum x is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of W2 is non empty set
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of v is non empty set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is set
the carrier of (V,W1) is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 : verum } is set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum v is Element of the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 : verum } is set
the carrier of (V,W1) is non empty set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is set
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
v is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
x . v is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
{v} is non empty trivial finite 1 -element Element of bool the carrier of V
r2 is non empty trivial finite 1 -element Element of bool the carrier of V
r3 is Element of the carrier of V
u . r3 is ext-real V25() V26() Element of REAL
r3 is finite Element of bool the carrier of V
r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
{v} is non empty trivial finite 1 -element Element of bool the carrier of V
r3 is set
r4 is Element of the carrier of V
r2 . r4 is ext-real V25() V26() Element of REAL
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {v}
Sum r3 is Element of the carrier of V
1 * v is Element of the carrier of V
Carrier r3 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0 } is set
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum r4 is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
(0). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
0. V is V55(V) Element of the carrier of V
the carrier of V is non empty set
W1 is set
the carrier of ((0). V) is non empty set
{(0. V)} is non empty trivial finite 1 -element Element of bool the carrier of V
bool the carrier of V is non empty set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
{} the carrier of V is functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() Element of bool the carrier of V
bool the carrier of V is non empty set
(V,({} the carrier of V)) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(0). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is Element of the carrier of V
the carrier of (V,({} the carrier of V)) is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {} the carrier of V : verum } is set
0. V is V55(V) Element of the carrier of V
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {} the carrier of V
Sum v is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
(0). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
0. V is V55(V) Element of the carrier of V
{(0. V)} is non empty trivial finite 1 -element Element of bool the carrier of V
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is set
the Element of W1 is Element of W1
v is set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum x is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(Omega). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of ((Omega). V) is non empty set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W1 /\ W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 /\ v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of V is non empty set
x is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 + v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W1 + W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of V is non empty set
x is Element of the carrier of V
u is Element of the carrier of V
r2 is Element of the carrier of V
u + r2 is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum x is Element of the carrier of V
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum u is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V
W1 \/ W2 is Element of bool the carrier of V
(V,(W1 \/ W2)) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,W1) + (V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 \/ W2
Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
(Carrier x) \ W1 is finite Element of bool the carrier of V
(Carrier x) /\ W1 is finite Element of bool the carrier of V
r3 is set
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r4 is Element of the carrier of V
t is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
t . r4 is ext-real V25() V26() Element of REAL
x . r3 is set
r3 is set
x . r3 is set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
r4 is finite Element of bool the carrier of V
t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
a4 is Element of the carrier of V
t . a4 is ext-real V25() V26() Element of REAL
a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier a4 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not a4 . b1 = 0 } is set
a3 is set
a2 is Element of the carrier of V
a4 . a2 is ext-real V25() V26() Element of REAL
a2 is set
a1 is Element of the carrier of V
a is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a . a1 is ext-real V25() V26() Element of REAL
x . a2 is set
a2 is set
x . a2 is set
a2 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a1 is finite Element of bool the carrier of V
a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
b is Element of the carrier of V
a . b is ext-real V25() V26() Element of REAL
r6 is set
b is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier b is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not b . b1 = 0 } is set
r6 is set
v is Element of the carrier of V
b . v is ext-real V25() V26() Element of REAL
a3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
r6 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
a3 + r6 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
v is Element of the carrier of V
x . v is ext-real V25() V26() Element of REAL
(a3 + r6) . v is ext-real V25() V26() Element of REAL
a3 . v is ext-real V25() V26() Element of REAL
r6 . v is ext-real V25() V26() Element of REAL
(a3 . v) + (r6 . v) is ext-real V25() V26() Element of REAL
(x . v) + (r6 . v) is ext-real V25() V26() Element of REAL
(x . v) + 0 is ext-real V25() V26() Element of REAL
a3 . v is ext-real V25() V26() Element of REAL
r6 . v is ext-real V25() V26() Element of REAL
(a3 . v) + (r6 . v) is ext-real V25() V26() Element of REAL
0 + (r6 . v) is ext-real V25() V26() Element of REAL
a3 . v is ext-real V25() V26() Element of REAL
r6 . v is ext-real V25() V26() Element of REAL
(a3 . v) + (r6 . v) is ext-real V25() V26() Element of REAL
0 + (r6 . v) is ext-real V25() V26() Element of REAL
0 + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
Sum a3 is Element of the carrier of V
Sum r6 is Element of the carrier of V
(Sum a3) + (Sum r6) is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V
W1 /\ W2 is Element of bool the carrier of V
(V,(W1 /\ W2)) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,W1) /\ (V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR
W1 is Element of bool the carrier of V
W2 is set
v is set
the Element of v is Element of v
union v is set
r2 is set
r3 is set
r2 is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of r2
Sum r3 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r3 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0 } is set
r4 is Relation-like Function-like set
dom r4 is set
rng r4 is set
t is non empty set
union t is set
the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t is Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t
rng the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t is set
a2 is set
r4 . a2 is set
a1 is set
a is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a2 in b1 & b1 in v ) } is set
dom the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t is set
a2 is set
a1 is set
the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t . a1 is set
a is set
r4 . a is set
{ b1 where b1 is Element of bool the carrier of V : ( a in b1 & b1 in v ) } is set
b is Element of bool the carrier of V
a2 is set
a1 is set
union (rng the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t) is set
a2 is Element of bool the carrier of V
a1 is set
r4 . a1 is set
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set
the Relation-like t -defined union t -valued Function-like quasi_total Choice_Function of t . (r4 . a1) is set
b is Element of bool the carrier of V
r3 is Element of bool the carrier of V
(Omega). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is set
x is Element of bool the carrier of V
(V,x) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
u is Element of the carrier of V
{u} is non empty trivial finite 1 -element Element of bool the carrier of V
x \/ {u} is Element of bool the carrier of V
r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x \/ {u}
Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
r2 . u is ext-real V25() V26() Element of REAL
- (r2 . u) is ext-real V25() V26() Element of REAL
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r3 . u is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
t is Element of the carrier of V
(Carrier r2) \ {u} is finite Element of bool the carrier of V
r2 . t is ext-real V25() V26() Element of REAL
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
r4 . t is ext-real V25() V26() Element of REAL
t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier t is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not t . b1 = 0 } is set
a4 is set
a3 is Element of the carrier of V
t . a3 is ext-real V25() V26() Element of REAL
r2 . a3 is ext-real V25() V26() Element of REAL
a3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a3 . u is ext-real V25() V26() Element of REAL
a1 is Element of the carrier of V
a2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
a2 . a1 is ext-real V25() V26() Element of REAL
a1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier a1 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not a1 . b1 = 0 } is set
a is set
b is Element of the carrier of V
a1 . b is ext-real V25() V26() Element of REAL
a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {u}
Sum a is Element of the carrier of V
(- (r2 . u)) * u is Element of the carrier of V
a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x
a4 - a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
- a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
(- 1) * a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
a4 + (- a) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
b is Element of the carrier of V
(a4 - a) . b is ext-real V25() V26() Element of REAL
r2 . b is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - 0 is ext-real V25() V26() Element of REAL
Sum a4 is Element of the carrier of V
(Sum a4) - (Sum a) is Element of the carrier of V
- (Sum a) is Element of the carrier of V
K194(V,(Sum a4),(- (Sum a))) is Element of the carrier of V
(0. V) + (Sum a) is Element of the carrier of V
(- (r2 . u)) " is ext-real V25() V26() Element of REAL
((- (r2 . u)) ") * ((- (r2 . u)) * u) is Element of the carrier of V
((- (r2 . u)) ") * (- (r2 . u)) is ext-real V25() V26() Element of REAL
(((- (r2 . u)) ") * (- (r2 . u))) * u is Element of the carrier of V
1 * u is Element of the carrier of V
r3 is set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is set
v is set
union v is set
u is set
r2 is set
u is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set
r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of u
Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
r3 is Relation-like Function-like set
dom r3 is set
rng r3 is set
r4 is non empty set
union r4 is set
the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 is Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4
rng the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 is set
a3 is set
r3 . a3 is set
a2 is set
a1 is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( a3 in b1 & b1 in v ) } is set
dom the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 is set
a3 is set
a2 is set
the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 . a2 is set
a1 is set
r3 . a1 is set
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in v ) } is set
a is Element of bool the carrier of V
a3 is set
a2 is set
union (rng the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4) is set
a3 is Element of bool the carrier of V
a2 is set
r3 . a2 is set
{ b1 where b1 is Element of bool the carrier of V : ( a2 in b1 & b1 in v ) } is set
the Relation-like r4 -defined union r4 -valued Function-like quasi_total Choice_Function of r4 . (r3 . a2) is set
a is Element of bool the carrier of V
r2 is set
r3 is set
r4 is Element of bool the carrier of V
{} the carrier of V is functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() Element of bool the carrier of V
v is set
x is Element of bool the carrier of V
(V,x) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of (V,x) is non empty set
r2 is Element of the carrier of V
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Sum r3 is Element of the carrier of V
Carrier r3 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0 } is set
r4 is set
t is Element of the carrier of V
u is Element of bool the carrier of V
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of u
Sum r4 is Element of the carrier of V
(V,u) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
u is Element of the carrier of V
u is Element of the carrier of V
{u} is non empty trivial finite 1 -element Element of bool the carrier of V
x \/ {u} is Element of bool the carrier of V
r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x \/ {u}
Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
r2 . u is ext-real V25() V26() Element of REAL
- (r2 . u) is ext-real V25() V26() Element of REAL
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r3 . u is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
t is Element of the carrier of V
(Carrier r2) \ {u} is finite Element of bool the carrier of V
r2 . t is ext-real V25() V26() Element of REAL
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
r4 . t is ext-real V25() V26() Element of REAL
t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier t is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not t . b1 = 0 } is set
a4 is set
a3 is Element of the carrier of V
t . a3 is ext-real V25() V26() Element of REAL
r2 . a3 is ext-real V25() V26() Element of REAL
a3 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
a3 . u is ext-real V25() V26() Element of REAL
a1 is Element of the carrier of V
a2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
a2 . a1 is ext-real V25() V26() Element of REAL
a1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier a1 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not a1 . b1 = 0 } is set
a is set
b is Element of the carrier of V
a1 . b is ext-real V25() V26() Element of REAL
a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {u}
Sum a is Element of the carrier of V
(- (r2 . u)) * u is Element of the carrier of V
a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of x
a4 - a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
- a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
(- 1) * a is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
a4 + (- a) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
b is Element of the carrier of V
(a4 - a) . b is ext-real V25() V26() Element of REAL
r2 . b is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
a4 . b is ext-real V25() V26() Element of REAL
a . b is ext-real V25() V26() Element of REAL
(a4 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - (a . b) is ext-real V25() V26() Element of REAL
(r2 . b) - 0 is ext-real V25() V26() Element of REAL
Sum a4 is Element of the carrier of V
(Sum a4) - (Sum a) is Element of the carrier of V
- (Sum a) is Element of the carrier of V
K194(V,(Sum a4),(- (Sum a))) is Element of the carrier of V
(0. V) + (Sum a) is Element of the carrier of V
(- (r2 . u)) " is ext-real V25() V26() Element of REAL
((- (r2 . u)) ") * ((- (r2 . u)) * u) is Element of the carrier of V
((- (r2 . u)) ") * (- (r2 . u)) is ext-real V25() V26() Element of REAL
(((- (r2 . u)) ") * (- (r2 . u))) * u is Element of the carrier of V
1 * u is Element of the carrier of V
r3 is set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR
{} the carrier of V is functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V40() cardinal {} -element FinSequence-membered V120() V121() V122() V123() V124() V125() V126() Element of bool the carrier of V
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is (V)
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is (V)
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is (V)
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of (V,W2) is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v is finite set
W1 (#) v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (W1 (#) v) is Element of the carrier of V
len v is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
x + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
u is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng u is finite set
len u is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
W1 (#) u is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (W1 (#) u) is Element of the carrier of V
r2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
r3 is set
<*r3*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
r2 ^ <*r3*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
r4 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
r4 ^ <*r3*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
rng (r4 ^ <*r3*>) is finite set
rng r4 is finite set
rng <*r3*> is finite set
(rng r4) \/ (rng <*r3*>) is finite set
{r3} is non empty trivial finite 1 -element set
(rng r4) \/ {r3} is finite set
a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum a4 is Element of the carrier of V
a3 is Element of the carrier of V
<*a3*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
r4 ^ <*a3*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (r4 ^ <*a3*>) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
len r4 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
len <*a3*> is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
(len r4) + (len <*a3*>) is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
(len r4) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
W1 (#) r4 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (W1 (#) r4) is Element of the carrier of V
a2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum a2 is Element of the carrier of V
W1 . a3 is ext-real V25() V26() Element of REAL
(W1 . a3) * a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
a2 + ((W1 . a3) * a4) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
t is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
W1 (#) t is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(W1 (#) r4) ^ (W1 (#) t) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((W1 (#) r4) ^ (W1 (#) t)) is Element of the carrier of V
Sum (W1 (#) t) is Element of the carrier of V
(Sum a2) + (Sum (W1 (#) t)) is Element of the carrier of V
(W1 . a3) * a3 is Element of the carrier of V
<*((W1 . a3) * a3)*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum <*((W1 . a3) * a3)*> is Element of the carrier of V
(Sum a2) + (Sum <*((W1 . a3) * a3)*>) is Element of the carrier of V
(W1 . a3) * (Sum a4) is Element of the carrier of V
(Sum a2) + ((W1 . a3) * (Sum a4)) is Element of the carrier of V
Sum ((W1 . a3) * a4) is Element of the carrier of V
(Sum a2) + (Sum ((W1 . a3) * a4)) is Element of the carrier of V
Sum (a2 + ((W1 . a3) * a4)) is Element of the carrier of V
x is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng x is finite set
len x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
W1 (#) x is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (W1 (#) x) is Element of the carrier of V
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V120() V121() V122() V123() V124() V125() V126() FinSequence of the carrier of V
[:NAT, the carrier of V:] is non empty non trivial non finite set
0. V is V55(V) Element of the carrier of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Sum (ZeroLC V) is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier W1 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not W1 . b1 = 0 } is set
Sum W1 is Element of the carrier of V
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
the carrier of (V,W2) is non empty set
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v is finite set
W1 (#) v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (W1 (#) v) is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum x is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
W2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier W2 is finite Element of bool the carrier of V
bool the carrier of V is non empty set
{ b1 where b1 is Element of the carrier of V : not W2 . b1 = 0 } is set
W2 | the carrier of W1 is Relation-like the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
Sum W2 is Element of the carrier of V
v is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Carrier v is finite Element of bool the carrier of W1
bool the carrier of W1 is non empty set
{ b1 where b1 is Element of the carrier of W1 : not v . b1 = 0 } is set
Sum v is Element of the carrier of W1
dom v is set
x is set
u is Element of the carrier of W1
v . u is ext-real V25() V26() Element of REAL
W2 . u is set
x is Relation-like NAT -defined the carrier of W1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W1
rng x is finite set
v (#) x is Relation-like NAT -defined the carrier of W1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W1
Sum (v (#) x) is Element of the carrier of W1
u is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng u is finite set
W2 (#) u is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (W2 (#) u) is Element of the carrier of V
r2 is set
r3 is Element of the carrier of V
W2 . r3 is ext-real V25() V26() Element of REAL
v . r3 is set
dom x is finite set
[:(dom x),(dom x):] is finite set
bool [:(dom x),(dom x):] is non empty finite V40() set
r2 is Relation-like dom x -defined dom x -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(dom x),(dom x):]
x * r2 is Relation-like dom x -defined the carrier of W1 -valued Function-like finite Element of bool [:(dom x), the carrier of W1:]
[:(dom x), the carrier of W1:] is set
bool [:(dom x), the carrier of W1:] is non empty set
len (v (#) x) is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
len x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
dom (v (#) x) is finite set
(v (#) x) * r2 is Relation-like dom x -defined the carrier of W1 -valued Function-like finite Element of bool [:(dom x), the carrier of W1:]
r3 is Relation-like NAT -defined the carrier of W1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of W1
len r3 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
dom r3 is finite set
rng r3 is finite set
[:NAT, the carrier of W1:] is non empty non trivial non finite set
bool [:NAT, the carrier of W1:] is non empty non trivial non finite set
Sum r3 is Element of the carrier of W1
0. W1 is V55(W1) Element of the carrier of W1
a4 is Relation-like NAT -defined the carrier of W1 -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of W1:]
a4 . (len r3) is Element of the carrier of W1
a4 . 0 is Element of the carrier of W1
dom a4 is set
rng a4 is set
[:NAT, the carrier of V:] is non empty non trivial non finite set
bool [:NAT, the carrier of V:] is non empty non trivial non finite set
t is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len t is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
a3 is Relation-like NAT -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of V:]
a2 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
a2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
t . (a2 + 1) is set
a3 . (a2 + 1) is Element of the carrier of V
a3 . a2 is Element of the carrier of V
a1 is Element of the carrier of V
(a3 . a2) + a1 is Element of the carrier of V
a4 . (a2 + 1) is Element of the carrier of W1
a4 . a2 is Element of the carrier of W1
a is Element of the carrier of W1
(a4 . a2) + a is Element of the carrier of W1
len u is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
dom u is finite set
len (W2 (#) u) is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
dom (W2 (#) u) is finite set
a2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal set
u /. a2 is Element of the carrier of V
r2 . a2 is set
u . a2 is set
dom r2 is finite set
rng r2 is finite set
card x is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
Seg (card x) is finite card x -element V120() V121() V122() V123() V124() V125() Element of bool NAT
r6 is ext-real epsilon-transitive epsilon-connected ordinal natural V25() V26() finite cardinal V108() V109() V120() V121() V122() V123() V124() V125() Element of NAT
x /. r6 is Element of the carrier of W1
x . (r2 . a2) is set
r3 . a2 is set
(v (#) x) . r6 is set
b is Element of the carrier of W1
v . b is ext-real V25() V26() Element of REAL
(v . b) * b is Element of the carrier of W1
W2 . (u /. a2) is ext-real V25() V26() Element of REAL
(W2 . (u /. a2)) * b is Element of the carrier of W1
(W2 . (u /. a2)) * (u /. a2) is Element of the carrier of V
(W2 (#) u) . a2 is set
[:(dom (v (#) x)),(dom (v (#) x)):] is finite set
bool [:(dom (v (#) x)),(dom (v (#) x)):] is non empty finite V40() set
a2 is Relation-like dom (v (#) x) -defined dom (v (#) x) -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(dom (v (#) x)),(dom (v (#) x)):]
(v (#) x) * a2 is Relation-like dom (v (#) x) -defined the carrier of W1 -valued Function-like finite Element of bool [:(dom (v (#) x)), the carrier of W1:]
[:(dom (v (#) x)), the carrier of W1:] is set
bool [:(dom (v (#) x)), the carrier of W1:] is non empty set
a3 . (len t) is Element of the carrier of V
a3 . 0 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
W2 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Carrier W2 is finite Element of bool the carrier of W1
bool the carrier of W1 is non empty set
{ b1 where b1 is Element of the carrier of W1 : not W2 . b1 = 0 } is set
Sum W2 is Element of the carrier of W1
[: the carrier of W1,REAL:] is non empty non trivial non finite set
bool [: the carrier of W1,REAL:] is non empty non trivial non finite set
bool the carrier of V is non empty set
u is set
W2 . u is set
r2 is Element of the carrier of V
r3 is Element of the carrier of W1
W2 . r3 is ext-real V25() V26() Element of REAL
W2 . r3 is set
r2 is Element of the carrier of V
r2 is Element of the carrier of V
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
u is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
u is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r2 is Element of the carrier of V
x is finite Element of bool the carrier of V
W2 . r2 is set
u . r2 is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
r2 | the carrier of W1 is Relation-like the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
Sum r2 is Element of the carrier of V
r4 is set
t is Element of the carrier of V
r2 . t is ext-real V25() V26() Element of REAL
r4 is set
r2 . r4 is set
W2 . r4 is set
v is Relation-like the carrier of W1 -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of W1,REAL:]
v . r4 is set
r3 is Relation-like the carrier of W1 -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of W1,REAL:]
r3 . r4 is set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
W2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier W2 is finite Element of bool the carrier of V
bool the carrier of V is non empty set
{ b1 where b1 is Element of the carrier of V : not W2 . b1 = 0 } is set
Sum W2 is Element of the carrier of V
bool the carrier of W1 is non empty set
[: the carrier of W1,REAL:] is non empty non trivial non finite set
bool [: the carrier of W1,REAL:] is non empty non trivial non finite set
W2 | the carrier of W1 is Relation-like the carrier of V -defined REAL -valued Function-like Element of bool [: the carrier of V,REAL:]
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
x is Relation-like the carrier of W1 -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of W1,REAL:]
Funcs ( the carrier of W1,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of W1, REAL
dom x is set
u is Element of the carrier of W1
v is finite Element of bool the carrier of W1
W2 . u is set
x . u is ext-real V25() V26() Element of REAL
u is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Carrier u is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not u . b1 = 0 } is set
Sum u is Element of the carrier of W1
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is (V)
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is Element of the carrier of V
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like non empty total quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty non trivial non finite set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty non trivial non finite set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty non trivial non finite set
UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
bool the carrier of W1 is non empty set
W2 is Element of bool the carrier of W1
v is Element of bool the carrier of V
0. V is V55(V) Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of v
Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
u is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Carrier u is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not u . b1 = 0 } is set
Sum u is Element of the carrier of W1
r2 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum r2 is Element of the carrier of W1
0. W1 is V55(W1) Element of the carrier of W1
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
bool the carrier of W1 is non empty set
W2 is Element of bool the carrier of V
v is Element of bool the carrier of W1
0. W1 is V55(W1) Element of the carrier of W1
x is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of v
Sum x is Element of the carrier of W1
Carrier x is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not x . b1 = 0 } is set
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier u is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not u . b1 = 0 } is set
Sum u is Element of the carrier of V
r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum r2 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is (W1)
the carrier of V is non empty set
bool the carrier of V is non empty set
v is linearly-independent Element of bool the carrier of V
x is (V)
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is Element of bool the carrier of V
W2 is Element of the carrier of V
{W2} is non empty trivial finite 1 -element Element of bool the carrier of V
W1 \ {W2} is Element of bool the carrier of V
bool W1 is non empty set
v is Element of bool the carrier of V
(V,v) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v \/ {W2} is Element of bool the carrier of V
W1 \/ W1 is Element of bool the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of v
Sum x is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
(V,{W2}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W2}
Sum u is Element of the carrier of V
Carrier u is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not u . b1 = 0 } is set
(Carrier x) \/ (Carrier u) is finite Element of bool the carrier of V
x - u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
- u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
(- 1) * u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
x + (- u) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier (x - u) is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not (x - u) . b1 = 0 } is set
r2 is Element of the carrier of V
u . r2 is ext-real V25() V26() Element of REAL
r2 is set
r3 is Element of the carrier of V
x . r3 is ext-real V25() V26() Element of REAL
(x - u) . r3 is ext-real V25() V26() Element of REAL
u . r3 is ext-real V25() V26() Element of REAL
(x . r3) - (u . r3) is ext-real V25() V26() Element of REAL
(x . r3) - 0 is ext-real V25() V26() Element of REAL
- (Sum u) is Element of the carrier of V
(Sum x) + (- (Sum u)) is Element of the carrier of V
Sum (- u) is Element of the carrier of V
(Sum x) + (Sum (- u)) is Element of the carrier of V
Sum (x - u) is Element of the carrier of V
r2 is set
V is set
W1 is set
{W1} is non empty trivial finite 1 -element set
V \ {W1} is Element of bool V
bool V is non empty set
V /\ {W1} is finite set
W2 is set
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is (V)
W2 is non empty Element of bool the carrier of V
W1 \/ W2 is Element of bool the carrier of V
v is set
x is Element of bool the carrier of V
u is Element of the carrier of V
{u} is non empty trivial finite 1 -element Element of bool the carrier of V
x \ {u} is Element of bool the carrier of V
W1 \ {u} is Element of bool the carrier of V
r2 is Element of bool the carrier of V
(V,W1) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,r2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is set
the carrier of (V,W2) is non empty set
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
u is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Carrier u is finite Element of bool the carrier of W1
bool the carrier of W1 is non empty set
{ b1 where b1 is Element of the carrier of W1 : not u . b1 = 0 } is set
Sum u is Element of the carrier of W1
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
the carrier of W1 is non empty set
bool the carrier of W1 is non empty set
W2 is Element of bool the carrier of V
(V,W2) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is Element of bool the carrier of W1
(W1,v) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of W1
x is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
u is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
r2 is set
the carrier of (V,W2) is non empty set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum r3 is Element of the carrier of V
Carrier r3 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r3 . b1 = 0 } is set
r4 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Carrier r4 is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not r4 . b1 = 0 } is set
Sum r4 is Element of the carrier of W1
t is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of v
Sum t is Element of the carrier of W1
the carrier of (W1,v) is non empty set
r2 is set
r3 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of v
Sum r3 is Element of the carrier of W1
Carrier r3 is finite Element of bool the carrier of W1
{ b1 where b1 is Element of the carrier of W1 : not r3 . b1 = 0 } is set
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier r4 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r4 . b1 = 0 } is set
Sum r4 is Element of the carrier of V
t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W2
Sum t is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
{W1} is non empty trivial finite 1 -element Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W1}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W2 is set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W1}
Sum v is Element of the carrier of V
v . W1 is ext-real V25() V26() Element of REAL
(v . W1) * W1 is Element of the carrier of V
v is ext-real V25() V26() Element of REAL
v * W1 is Element of the carrier of V
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
x is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
x . W1 is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
r2 is Element of the carrier of V
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
u . r2 is ext-real V25() V26() Element of REAL
r2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier r2 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r2 . b1 = 0 } is set
r3 is set
r2 . r3 is set
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W1}
Sum r3 is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
{W1} is non empty trivial finite 1 -element Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W1}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
{W2} is non empty trivial finite 1 -element Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W2}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W1 + (V,{W2}) is Element of bool the carrier of V
v is set
x is Element of the carrier of V
W1 + x is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W2 is Element of the carrier of V
x is ext-real V25() V26() Element of REAL
x * W2 is Element of the carrier of V
W1 + (x * W2) is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
{W1,W2} is finite Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W1,W2}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is set
{W1} is non empty trivial finite 1 -element Element of bool the carrier of V
x is ext-real V25() V26() Element of REAL
x * W1 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
(x * W1) + (0. V) is Element of the carrier of V
0 * W2 is Element of the carrier of V
(x * W1) + (0 * W2) is Element of the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W1,W2}
Sum x is Element of the carrier of V
x . W1 is ext-real V25() V26() Element of REAL
(x . W1) * W1 is Element of the carrier of V
x . W2 is ext-real V25() V26() Element of REAL
(x . W2) * W2 is Element of the carrier of V
((x . W1) * W1) + ((x . W2) * W2) is Element of the carrier of V
x is ext-real V25() V26() Element of REAL
x * W1 is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W2 is Element of the carrier of V
(x * W1) + (u * W2) is Element of the carrier of V
x is ext-real V25() V26() Element of REAL
x * W1 is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W2 is Element of the carrier of V
(x * W1) + (u * W2) is Element of the carrier of V
x + u is ext-real V25() V26() Element of REAL
(x + u) * W1 is Element of the carrier of V
{W1} is non empty trivial finite 1 -element Element of bool the carrier of V
(V,{W1}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r2 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r2 . W1 is ext-real V25() V26() Element of REAL
r2 . W2 is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
r4 is Element of the carrier of V
r3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
r3 . r4 is ext-real V25() V26() Element of REAL
r4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier r4 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not r4 . b1 = 0 } is set
t is set
r4 . t is set
t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W1,W2}
Sum t is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
{W1,W2} is finite Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W1,W2}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
v is Element of the carrier of V
{W2,v} is finite Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W2,v}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W1 + (V,{W2,v}) is Element of bool the carrier of V
x is set
u is Element of the carrier of V
W1 + u is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * W2 is Element of the carrier of V
r3 is ext-real V25() V26() Element of REAL
r3 * v is Element of the carrier of V
(r2 * W2) + (r3 * v) is Element of the carrier of V
W1 + (r2 * W2) is Element of the carrier of V
(W1 + (r2 * W2)) + (r3 * v) is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W2 is Element of the carrier of V
W1 + (u * W2) is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * v is Element of the carrier of V
(W1 + (u * W2)) + (r2 * v) is Element of the carrier of V
(u * W2) + (r2 * v) is Element of the carrier of V
W1 + ((u * W2) + (r2 * v)) is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
v is Element of the carrier of V
{W1,W2,v} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W1,W2,v}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
x is set
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W1,W2,v}
Sum u is Element of the carrier of V
u . W1 is ext-real V25() V26() Element of REAL
(u . W1) * W1 is Element of the carrier of V
u . W2 is ext-real V25() V26() Element of REAL
(u . W2) * W2 is Element of the carrier of V
((u . W1) * W1) + ((u . W2) * W2) is Element of the carrier of V
u . v is ext-real V25() V26() Element of REAL
(u . v) * v is Element of the carrier of V
(((u . W1) * W1) + ((u . W2) * W2)) + ((u . v) * v) is Element of the carrier of V
{W1,v} is finite Element of bool the carrier of V
{W1,W1,W2} is non empty finite Element of bool the carrier of V
{v,v,W1} is non empty finite Element of bool the carrier of V
{W1,W2} is finite Element of bool the carrier of V
u is ext-real V25() V26() Element of REAL
u * W1 is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * W2 is Element of the carrier of V
(u * W1) + (r2 * W2) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
((u * W1) + (r2 * W2)) + (0. V) is Element of the carrier of V
0 * v is Element of the carrier of V
((u * W1) + (r2 * W2)) + (0 * v) is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W1 is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * v is Element of the carrier of V
(u * W1) + (r2 * v) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
(u * W1) + (0. V) is Element of the carrier of V
((u * W1) + (0. V)) + (r2 * v) is Element of the carrier of V
0 * W2 is Element of the carrier of V
(u * W1) + (0 * W2) is Element of the carrier of V
((u * W1) + (0 * W2)) + (r2 * v) is Element of the carrier of V
{W1,W2} is finite Element of bool the carrier of V
u is ext-real V25() V26() Element of REAL
u * W1 is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * W2 is Element of the carrier of V
(u * W1) + (r2 * W2) is Element of the carrier of V
r3 is ext-real V25() V26() Element of REAL
r3 * v is Element of the carrier of V
((u * W1) + (r2 * W2)) + (r3 * v) is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W1 is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * W2 is Element of the carrier of V
(u * W1) + (r2 * W2) is Element of the carrier of V
r3 is ext-real V25() V26() Element of REAL
r3 * v is Element of the carrier of V
((u * W1) + (r2 * W2)) + (r3 * v) is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W1 is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * W2 is Element of the carrier of V
(u * W1) + (r2 * W2) is Element of the carrier of V
r3 is ext-real V25() V26() Element of REAL
r3 * v is Element of the carrier of V
((u * W1) + (r2 * W2)) + (r3 * v) is Element of the carrier of V
{W1,v} is finite Element of bool the carrier of V
u + r2 is ext-real V25() V26() Element of REAL
(u + r2) * W1 is Element of the carrier of V
((u + r2) * W1) + (r3 * v) is Element of the carrier of V
{W1,W1,W2} is non empty finite Element of bool the carrier of V
{W2,W1} is finite Element of bool the carrier of V
r3 * W1 is Element of the carrier of V
(u * W1) + (r3 * W1) is Element of the carrier of V
(r2 * W2) + ((u * W1) + (r3 * W1)) is Element of the carrier of V
u + r3 is ext-real V25() V26() Element of REAL
(u + r3) * W1 is Element of the carrier of V
(r2 * W2) + ((u + r3) * W1) is Element of the carrier of V
{W2,W2,W1} is non empty finite Element of bool the carrier of V
{W1,W2} is finite Element of bool the carrier of V
r3 * W2 is Element of the carrier of V
(r2 * W2) + (r3 * W2) is Element of the carrier of V
(u * W1) + ((r2 * W2) + (r3 * W2)) is Element of the carrier of V
r2 + r3 is ext-real V25() V26() Element of REAL
(r2 + r3) * W2 is Element of the carrier of V
(u * W1) + ((r2 + r3) * W2) is Element of the carrier of V
[: the carrier of V,REAL:] is non empty non trivial non finite set
bool [: the carrier of V,REAL:] is non empty non trivial non finite set
r4 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of bool [: the carrier of V,REAL:]
r4 . W1 is ext-real V25() V26() Element of REAL
r4 . W2 is ext-real V25() V26() Element of REAL
r4 . v is ext-real V25() V26() Element of REAL
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
a4 is Element of the carrier of V
t is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of V,REAL)
t . a4 is ext-real V25() V26() Element of REAL
a4 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier a4 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not a4 . b1 = 0 } is set
a3 is set
a4 . a3 is set
a3 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of {W1,W2,v}
Sum a3 is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
v is Element of the carrier of V
{W1,W2,v} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W1,W2,v}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
v is Element of the carrier of V
x is Element of the carrier of V
{W2,v,x} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W2,v,x}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W1 + (V,{W2,v,x}) is Element of bool the carrier of V
u is set
r2 is Element of the carrier of V
W1 + r2 is Element of the carrier of V
r3 is ext-real V25() V26() Element of REAL
r3 * W2 is Element of the carrier of V
r4 is ext-real V25() V26() Element of REAL
r4 * v is Element of the carrier of V
(r3 * W2) + (r4 * v) is Element of the carrier of V
t is ext-real V25() V26() Element of REAL
t * x is Element of the carrier of V
((r3 * W2) + (r4 * v)) + (t * x) is Element of the carrier of V
W1 + (r3 * W2) is Element of the carrier of V
(W1 + (r3 * W2)) + (r4 * v) is Element of the carrier of V
((W1 + (r3 * W2)) + (r4 * v)) + (t * x) is Element of the carrier of V
W1 + ((r3 * W2) + (r4 * v)) is Element of the carrier of V
(W1 + ((r3 * W2) + (r4 * v))) + (t * x) is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * W2 is Element of the carrier of V
W1 + (r2 * W2) is Element of the carrier of V
r3 is ext-real V25() V26() Element of REAL
r3 * v is Element of the carrier of V
(W1 + (r2 * W2)) + (r3 * v) is Element of the carrier of V
r4 is ext-real V25() V26() Element of REAL
r4 * x is Element of the carrier of V
((W1 + (r2 * W2)) + (r3 * v)) + (r4 * x) is Element of the carrier of V
(r2 * W2) + (r3 * v) is Element of the carrier of V
((r2 * W2) + (r3 * v)) + (r4 * x) is Element of the carrier of V
W1 + (((r2 * W2) + (r3 * v)) + (r4 * x)) is Element of the carrier of V
W1 + ((r2 * W2) + (r3 * v)) is Element of the carrier of V
(W1 + ((r2 * W2) + (r3 * v))) + (r4 * x) is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
W2 is Element of the carrier of V
{W2} is non empty trivial finite 1 -element Element of bool the carrier of V
bool the carrier of V is non empty set
(V,{W2}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W1 is Element of the carrier of V
{W1} is non empty trivial finite 1 -element Element of bool the carrier of V
(V,{W1}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
v is ext-real V25() V26() Element of REAL
v * W2 is Element of the carrier of V
x is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W1 is Element of the carrier of V
u * v is ext-real V25() V26() Element of REAL
(u * v) * W2 is Element of the carrier of V
u is ext-real V25() V26() Element of REAL
u * W2 is Element of the carrier of V
v " is ext-real V25() V26() Element of REAL
(v ") * W1 is Element of the carrier of V
(v ") * v is ext-real V25() V26() Element of REAL
((v ") * v) * W2 is Element of the carrier of V
1 * W2 is Element of the carrier of V
u * (v ") is ext-real V25() V26() Element of REAL
(u * (v ")) * W1 is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
{W1,W2} is finite Element of bool the carrier of V
bool the carrier of V is non empty set
v is Element of the carrier of V
x is Element of the carrier of V
{v,x} is finite Element of bool the carrier of V
(V,{v,x}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
(V,{W1,W2}) is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
u is ext-real V25() V26() Element of REAL
u * v is Element of the carrier of V
r2 is ext-real V25() V26() Element of REAL
r2 * x is Element of the carrier of V
(u * v) + (r2 * x) is Element of the carrier of V
r3 is ext-real V25() V26() Element of REAL
r3 * v is Element of the carrier of V
r4 is ext-real V25() V26() Element of REAL
r4 * x is Element of the carrier of V
(r3 * v) + (r4 * x) is Element of the carrier of V
u * r4 is ext-real V25() V26() Element of REAL
r2 * r3 is ext-real V25() V26() Element of REAL
(u * r4) - (r2 * r3) is ext-real V25() V26() Element of REAL
0. V is V55(V) Element of the carrier of V
0 * x is Element of the carrier of V
(0. V) + (0 * x) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
u " is ext-real V25() V26() Element of REAL
(u ") * u is ext-real V25() V26() Element of REAL
((u ") * u) * r4 is ext-real V25() V26() Element of REAL
(u ") * (r2 * r3) is ext-real V25() V26() Element of REAL
1 * r4 is ext-real V25() V26() Element of REAL
(u ") * r2 is ext-real V25() V26() Element of REAL
r3 * ((u ") * r2) is ext-real V25() V26() Element of REAL
(r3 * ((u ") * r2)) * x is Element of the carrier of V
(r3 * v) + ((r3 * ((u ") * r2)) * x) is Element of the carrier of V
((u ") * r2) * x is Element of the carrier of V
r3 * (((u ") * r2) * x) is Element of the carrier of V
(r3 * v) + (r3 * (((u ") * r2) * x)) is Element of the carrier of V
v + (((u ") * r2) * x) is Element of the carrier of V
r3 * 1 is ext-real V25() V26() Element of REAL
(r3 * 1) * (v + (((u ") * r2) * x)) is Element of the carrier of V
r3 * ((u ") * u) is ext-real V25() V26() Element of REAL
(r3 * ((u ") * u)) * (v + (((u ") * r2) * x)) is Element of the carrier of V
r3 * (u ") is ext-real V25() V26() Element of REAL
(r3 * (u ")) * u is ext-real V25() V26() Element of REAL
((r3 * (u ")) * u) * (v + (((u ") * r2) * x)) is Element of the carrier of V
u * (v + (((u ") * r2) * x)) is Element of the carrier of V
(r3 * (u ")) * (u * (v + (((u ") * r2) * x))) is Element of the carrier of V
u * (((u ") * r2) * x) is Element of the carrier of V
(u * v) + (u * (((u ") * r2) * x)) is Element of the carrier of V
(r3 * (u ")) * ((u * v) + (u * (((u ") * r2) * x))) is Element of the carrier of V
u * ((u ") * r2) is ext-real V25() V26() Element of REAL
(u * ((u ") * r2)) * x is Element of the carrier of V
(u * v) + ((u * ((u ") * r2)) * x) is Element of the carrier of V
(r3 * (u ")) * ((u * v) + ((u * ((u ") * r2)) * x)) is Element of the carrier of V
u * (u ") is ext-real V25() V26() Element of REAL
(u * (u ")) * r2 is ext-real V25() V26() Element of REAL
((u * (u ")) * r2) * x is Element of the carrier of V
(u * v) + (((u * (u ")) * r2) * x) is Element of the carrier of V
(r3 * (u ")) * ((u * v) + (((u * (u ")) * r2) * x)) is Element of the carrier of V
1 * r2 is ext-real V25() V26() Element of REAL
(1 * r2) * x is Element of the carrier of V
(u * v) + ((1 * r2) * x) is Element of the carrier of V
(r3 * (u ")) * ((u * v) + ((1 * r2) * x)) is Element of the carrier of V
(r3 * (u ")) * ((u * v) + (r2 * x)) is Element of the carrier of V
r2 " is ext-real V25() V26() Element of REAL
(r2 ") * (u * r4) is ext-real V25() V26() Element of REAL
(r2 ") * (r2 * r3) is ext-real V25() V26() Element of REAL
(r2 ") * r2 is ext-real V25() V26() Element of REAL
((r2 ") * r2) * r3 is ext-real V25() V26() Element of REAL
1 * r3 is ext-real V25() V26() Element of REAL
(r2 ") * u is ext-real V25() V26() Element of REAL
r4 * ((r2 ") * u) is ext-real V25() V26() Element of REAL
(r4 * ((r2 ") * u)) * v is Element of the carrier of V
((r4 * ((r2 ") * u)) * v) + (r4 * x) is Element of the carrier of V
((r2 ") * u) * v is Element of the carrier of V
r4 * (((r2 ") * u) * v) is Element of the carrier of V
(r4 * (((r2 ") * u) * v)) + (r4 * x) is Element of the carrier of V
(((r2 ") * u) * v) + x is Element of the carrier of V
r4 * 1 is ext-real V25() V26() Element of REAL
(r4 * 1) * ((((r2 ") * u) * v) + x) is Element of the carrier of V
r4 * ((r2 ") * r2) is ext-real V25() V26() Element of REAL
(r4 * ((r2 ") * r2)) * ((((r2 ") * u) * v) + x) is Element of the carrier of V
r4 * (r2 ") is ext-real V25() V26() Element of REAL
(r4 * (r2 ")) * r2 is ext-real V25() V26() Element of REAL
((r4 * (r2 ")) * r2) * ((((r2 ") * u) * v) + x) is Element of the carrier of V
r2 * ((((r2 ") * u) * v) + x) is Element of the carrier of V
(r4 * (r2 ")) * (r2 * ((((r2 ") * u) * v) + x)) is Element of the carrier of V
r2 * (((r2 ") * u) * v) is Element of the carrier of V
(r2 * (((r2 ") * u) * v)) + (r2 * x) is Element of the carrier of V
(r4 * (r2 ")) * ((r2 * (((r2 ") * u) * v)) + (r2 * x)) is Element of the carrier of V
r2 * ((r2 ") * u) is ext-real V25() V26() Element of REAL
(r2 * ((r2 ") * u)) * v is Element of the carrier of V
((r2 * ((r2 ") * u)) * v) + (r2 * x) is Element of the carrier of V
(r4 * (r2 ")) * (((r2 * ((r2 ") * u)) * v) + (r2 * x)) is Element of the carrier of V
r2 * (r2 ") is ext-real V25() V26() Element of REAL
(r2 * (r2 ")) * u is ext-real V25() V26() Element of REAL
((r2 * (r2 ")) * u) * v is Element of the carrier of V
(((r2 * (r2 ")) * u) * v) + (r2 * x) is Element of the carrier of V
(r4 * (r2 ")) * ((((r2 * (r2 ")) * u) * v) + (r2 * x)) is Element of the carrier of V
1 * u is ext-real V25() V26() Element of REAL
(1 * u) * v is Element of the carrier of V
((1 * u) * v) + (r2 * x) is Element of the carrier of V
(r4 * (r2 ")) * (((1 * u) * v) + (r2 * x)) is Element of the carrier of V
(r4 * (r2 ")) * ((u * v) + (r2 * x)) is Element of the carrier of V
r2 " is ext-real V25() V26() Element of REAL
(r2 ") * W1 is Element of the carrier of V
(r2 ") * (u * v) is Element of the carrier of V
(r2 ") * (r2 * x) is Element of the carrier of V
((r2 ") * (u * v)) + ((r2 ") * (r2 * x)) is Element of the carrier of V
(r2 ") * u is ext-real V25() V26() Element of REAL
((r2 ") * u) * v is Element of the carrier of V
(((r2 ") * u) * v) + ((r2 ") * (r2 * x)) is Element of the carrier of V
(r2 ") * r2 is ext-real V25() V26() Element of REAL
((r2 ") * r2) * x is Element of the carrier of V
(((r2 ") * u) * v) + (((r2 ") * r2) * x) is Element of the carrier of V
1 * x is Element of the carrier of V
(((r2 ") * u) * v) + (1 * x) is Element of the carrier of V
(((r2 ") * u) * v) + x is Element of the carrier of V
((r2 ") * W1) - (((r2 ") * u) * v) is Element of the carrier of V
- (((r2 ") * u) * v) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (((r2 ") * u) * v))) is Element of the carrier of V
((r2 ") * W1) - ((r2 ") * (u * v)) is Element of the carrier of V
- ((r2 ") * (u * v)) is Element of the carrier of V
K194(V,((r2 ") * W1),(- ((r2 ") * (u * v)))) is Element of the carrier of V
W1 - (u * v) is Element of the carrier of V
- (u * v) is Element of the carrier of V
K194(V,W1,(- (u * v))) is Element of the carrier of V
(r2 ") * (W1 - (u * v)) is Element of the carrier of V
r4 * ((r2 ") * (W1 - (u * v))) is Element of the carrier of V
(r3 * v) + (r4 * ((r2 ") * (W1 - (u * v)))) is Element of the carrier of V
r4 * (r2 ") is ext-real V25() V26() Element of REAL
(r4 * (r2 ")) * (W1 - (u * v)) is Element of the carrier of V
(r3 * v) + ((r4 * (r2 ")) * (W1 - (u * v))) is Element of the carrier of V
(r4 * (r2 ")) * W1 is Element of the carrier of V
(r4 * (r2 ")) * (u * v) is Element of the carrier of V
((r4 * (r2 ")) * W1) - ((r4 * (r2 ")) * (u * v)) is Element of the carrier of V
- ((r4 * (r2 ")) * (u * v)) is Element of the carrier of V
K194(V,((r4 * (r2 ")) * W1),(- ((r4 * (r2 ")) * (u * v)))) is Element of the carrier of V
(r3 * v) + (((r4 * (r2 ")) * W1) - ((r4 * (r2 ")) * (u * v))) is Element of the carrier of V
(r3 * v) + ((r4 * (r2 ")) * W1) is Element of the carrier of V
((r3 * v) + ((r4 * (r2 ")) * W1)) - ((r4 * (r2 ")) * (u * v)) is Element of the carrier of V
K194(V,((r3 * v) + ((r4 * (r2 ")) * W1)),(- ((r4 * (r2 ")) * (u * v)))) is Element of the carrier of V
((r4 * (r2 ")) * W1) + (r3 * v) is Element of the carrier of V
(r4 * (r2 ")) * u is ext-real V25() V26() Element of REAL
((r4 * (r2 ")) * u) * v is Element of the carrier of V
(((r4 * (r2 ")) * W1) + (r3 * v)) - (((r4 * (r2 ")) * u) * v) is Element of the carrier of V
- (((r4 * (r2 ")) * u) * v) is Element of the carrier of V
K194(V,(((r4 * (r2 ")) * W1) + (r3 * v)),(- (((r4 * (r2 ")) * u) * v))) is Element of the carrier of V
(r3 * v) - (((r4 * (r2 ")) * u) * v) is Element of the carrier of V
K194(V,(r3 * v),(- (((r4 * (r2 ")) * u) * v))) is Element of the carrier of V
((r4 * (r2 ")) * W1) + ((r3 * v) - (((r4 * (r2 ")) * u) * v)) is Element of the carrier of V
r3 - ((r4 * (r2 ")) * u) is ext-real V25() V26() Element of REAL
(r3 - ((r4 * (r2 ")) * u)) * v is Element of the carrier of V
((r4 * (r2 ")) * W1) + ((r3 - ((r4 * (r2 ")) * u)) * v) is Element of the carrier of V
r2 * W2 is Element of the carrier of V
r2 * ((r4 * (r2 ")) * W1) is Element of the carrier of V
r2 * ((r3 - ((r4 * (r2 ")) * u)) * v) is Element of the carrier of V
(r2 * ((r4 * (r2 ")) * W1)) + (r2 * ((r3 - ((r4 * (r2 ")) * u)) * v)) is Element of the carrier of V
r2 * (r4 * (r2 ")) is ext-real V25() V26() Element of REAL
(r2 * (r4 * (r2 "))) * W1 is Element of the carrier of V
((r2 * (r4 * (r2 "))) * W1) + (r2 * ((r3 - ((r4 * (r2 ")) * u)) * v)) is Element of the carrier of V
r2 * (r2 ") is ext-real V25() V26() Element of REAL
r4 * (r2 * (r2 ")) is ext-real V25() V26() Element of REAL
(r4 * (r2 * (r2 "))) * W1 is Element of the carrier of V
((r4 * (r2 * (r2 "))) * W1) + (r2 * ((r3 - ((r4 * (r2 ")) * u)) * v)) is Element of the carrier of V
r4 * 1 is ext-real V25() V26() Element of REAL
(r4 * 1) * W1 is Element of the carrier of V
((r4 * 1) * W1) + (r2 * ((r3 - ((r4 * (r2 ")) * u)) * v)) is Element of the carrier of V
r4 * W1 is Element of the carrier of V
r2 * (r3 - ((r4 * (r2 ")) * u)) is ext-real V25() V26() Element of REAL
(r2 * (r3 - ((r4 * (r2 ")) * u))) * v is Element of the carrier of V
(r4 * W1) + ((r2 * (r3 - ((r4 * (r2 ")) * u))) * v) is Element of the carrier of V
r4 * u is ext-real V25() V26() Element of REAL
(r2 * (r2 ")) * (r4 * u) is ext-real V25() V26() Element of REAL
(r2 * r3) - ((r2 * (r2 ")) * (r4 * u)) is ext-real V25() V26() Element of REAL
((r2 * r3) - ((r2 * (r2 ")) * (r4 * u))) * v is Element of the carrier of V
(r4 * W1) + (((r2 * r3) - ((r2 * (r2 ")) * (r4 * u))) * v) is Element of the carrier of V
1 * (r4 * u) is ext-real V25() V26() Element of REAL
(r2 * r3) - (1 * (r4 * u)) is ext-real V25() V26() Element of REAL
((r2 * r3) - (1 * (r4 * u))) * v is Element of the carrier of V
(r4 * W1) + (((r2 * r3) - (1 * (r4 * u))) * v) is Element of the carrier of V
- ((u * r4) - (r2 * r3)) is ext-real V25() V26() Element of REAL
(- ((u * r4) - (r2 * r3))) * v is Element of the carrier of V
(r4 * W1) + ((- ((u * r4) - (r2 * r3))) * v) is Element of the carrier of V
((u * r4) - (r2 * r3)) * v is Element of the carrier of V
- (((u * r4) - (r2 * r3)) * v) is Element of the carrier of V
(r4 * W1) + (- (((u * r4) - (r2 * r3)) * v)) is Element of the carrier of V
(r2 * W2) - (r4 * W1) is Element of the carrier of V
- (r4 * W1) is Element of the carrier of V
K194(V,(r2 * W2),(- (r4 * W1))) is Element of the carrier of V
- ((r2 * W2) - (r4 * W1)) is Element of the carrier of V
- (r2 * W2) is Element of the carrier of V
(r4 * W1) + (- (r2 * W2)) is Element of the carrier of V
((u * r4) - (r2 * r3)) " is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3)) is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3))) * v is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * ((r4 * W1) + (- (r2 * W2))) is Element of the carrier of V
1 * v is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (r4 * W1) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (- (r2 * W2)) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r4 * W1)) + ((((u * r4) - (r2 * r3)) ") * (- (r2 * W2))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * r4 is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * r4) * W1 is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + ((((u * r4) - (r2 * r3)) ") * (- (r2 * W2))) is Element of the carrier of V
- r2 is ext-real V25() V26() Element of REAL
(- r2) * W2 is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * ((- r2) * W2) is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + ((((u * r4) - (r2 * r3)) ") * ((- r2) * W2)) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (- r2) is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * (- r2)) * W2 is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + (((((u * r4) - (r2 * r3)) ") * (- r2)) * W2) is Element of the carrier of V
- (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
(- (((u * r4) - (r2 * r3)) ")) * r2 is ext-real V25() V26() Element of REAL
((- (((u * r4) - (r2 * r3)) ")) * r2) * W2 is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + (((- (((u * r4) - (r2 * r3)) ")) * r2) * W2) is Element of the carrier of V
(- (((u * r4) - (r2 * r3)) ")) * (r2 * W2) is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + ((- (((u * r4) - (r2 * r3)) ")) * (r2 * W2)) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (r2 * W2) is Element of the carrier of V
- ((((u * r4) - (r2 * r3)) ") * (r2 * W2)) is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + (- ((((u * r4) - (r2 * r3)) ") * (r2 * W2))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * r2 is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * r2) * W2 is Element of the carrier of V
- (((((u * r4) - (r2 * r3)) ") * r2) * W2) is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + (- (((((u * r4) - (r2 * r3)) ") * r2) * W2)) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - (((((u * r4) - (r2 * r3)) ") * r2) * W2) is Element of the carrier of V
K194(V,((((u * r4) - (r2 * r3)) ") * (r4 * W1)),(- (((((u * r4) - (r2 * r3)) ") * r2) * W2))) is Element of the carrier of V
((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - (((((u * r4) - (r2 * r3)) ") * r2) * W2)) is Element of the carrier of V
((r2 ") * W1) - (((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - (((((u * r4) - (r2 * r3)) ") * r2) * W2))) is Element of the carrier of V
- (((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - (((((u * r4) - (r2 * r3)) ") * r2) * W2))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - (((((u * r4) - (r2 * r3)) ") * r2) * W2))))) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - ((((u * r4) - (r2 * r3)) ") * (r2 * W2)) is Element of the carrier of V
K194(V,((((u * r4) - (r2 * r3)) ") * (r4 * W1)),(- ((((u * r4) - (r2 * r3)) ") * (r2 * W2)))) is Element of the carrier of V
((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - ((((u * r4) - (r2 * r3)) ") * (r2 * W2))) is Element of the carrier of V
((r2 ") * W1) - (((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - ((((u * r4) - (r2 * r3)) ") * (r2 * W2)))) is Element of the carrier of V
- (((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - ((((u * r4) - (r2 * r3)) ") * (r2 * W2)))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (((r2 ") * u) * (((((u * r4) - (r2 * r3)) ") * (r4 * W1)) - ((((u * r4) - (r2 * r3)) ") * (r2 * W2)))))) is Element of the carrier of V
(r4 * W1) - (r2 * W2) is Element of the carrier of V
K194(V,(r4 * W1),(- (r2 * W2))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * ((r4 * W1) - (r2 * W2)) is Element of the carrier of V
((r2 ") * u) * ((((u * r4) - (r2 * r3)) ") * ((r4 * W1) - (r2 * W2))) is Element of the carrier of V
((r2 ") * W1) - (((r2 ") * u) * ((((u * r4) - (r2 * r3)) ") * ((r4 * W1) - (r2 * W2)))) is Element of the carrier of V
- (((r2 ") * u) * ((((u * r4) - (r2 * r3)) ") * ((r4 * W1) - (r2 * W2)))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (((r2 ") * u) * ((((u * r4) - (r2 * r3)) ") * ((r4 * W1) - (r2 * W2)))))) is Element of the carrier of V
u * (r2 ") is ext-real V25() V26() Element of REAL
(u * (r2 ")) * (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
((u * (r2 ")) * (((u * r4) - (r2 * r3)) ")) * ((r4 * W1) - (r2 * W2)) is Element of the carrier of V
((r2 ") * W1) - (((u * (r2 ")) * (((u * r4) - (r2 * r3)) ")) * ((r4 * W1) - (r2 * W2))) is Element of the carrier of V
- (((u * (r2 ")) * (((u * r4) - (r2 * r3)) ")) * ((r4 * W1) - (r2 * W2))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (((u * (r2 ")) * (((u * r4) - (r2 * r3)) ")) * ((r4 * W1) - (r2 * W2))))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (r2 ") is ext-real V25() V26() Element of REAL
u * ((((u * r4) - (r2 * r3)) ") * (r2 ")) is ext-real V25() V26() Element of REAL
(u * ((((u * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * W1) - (r2 * W2)) is Element of the carrier of V
((r2 ") * W1) - ((u * ((((u * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * W1) - (r2 * W2))) is Element of the carrier of V
- ((u * ((((u * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * W1) - (r2 * W2))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- ((u * ((((u * r4) - (r2 * r3)) ") * (r2 "))) * ((r4 * W1) - (r2 * W2))))) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * W1) - (r2 * W2)) is Element of the carrier of V
u * (((((u * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * W1) - (r2 * W2))) is Element of the carrier of V
((r2 ") * W1) - (u * (((((u * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * W1) - (r2 * W2)))) is Element of the carrier of V
- (u * (((((u * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * W1) - (r2 * W2)))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * (((((u * r4) - (r2 * r3)) ") * (r2 ")) * ((r4 * W1) - (r2 * W2)))))) is Element of the carrier of V
(r2 ") * ((r4 * W1) - (r2 * W2)) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * W1) - (r2 * W2))) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * W1) - (r2 * W2)))) is Element of the carrier of V
((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * W1) - (r2 * W2))))) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * W1) - (r2 * W2))))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * ((((u * r4) - (r2 * r3)) ") * ((r2 ") * ((r4 * W1) - (r2 * W2))))))) is Element of the carrier of V
(r2 ") * (r4 * W1) is Element of the carrier of V
(r2 ") * (r2 * W2) is Element of the carrier of V
((r2 ") * (r4 * W1)) - ((r2 ") * (r2 * W2)) is Element of the carrier of V
- ((r2 ") * (r2 * W2)) is Element of the carrier of V
K194(V,((r2 ") * (r4 * W1)),(- ((r2 ") * (r2 * W2)))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - ((r2 ") * (r2 * W2))) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - ((r2 ") * (r2 * W2)))) is Element of the carrier of V
((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - ((r2 ") * (r2 * W2))))) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - ((r2 ") * (r2 * W2))))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - ((r2 ") * (r2 * W2))))))) is Element of the carrier of V
((r2 ") * r2) * W2 is Element of the carrier of V
((r2 ") * (r4 * W1)) - (((r2 ") * r2) * W2) is Element of the carrier of V
- (((r2 ") * r2) * W2) is Element of the carrier of V
K194(V,((r2 ") * (r4 * W1)),(- (((r2 ") * r2) * W2))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - (((r2 ") * r2) * W2)) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - (((r2 ") * r2) * W2))) is Element of the carrier of V
((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - (((r2 ") * r2) * W2)))) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - (((r2 ") * r2) * W2)))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * (r4 * W1)) - (((r2 ") * r2) * W2)))))) is Element of the carrier of V
(r2 ") * r4 is ext-real V25() V26() Element of REAL
((r2 ") * r4) * W1 is Element of the carrier of V
(((r2 ") * r4) * W1) - (((r2 ") * r2) * W2) is Element of the carrier of V
K194(V,(((r2 ") * r4) * W1),(- (((r2 ") * r2) * W2))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (((r2 ") * r2) * W2)) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (((r2 ") * r2) * W2))) is Element of the carrier of V
((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (((r2 ") * r2) * W2)))) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (((r2 ") * r2) * W2)))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (((r2 ") * r2) * W2)))))) is Element of the carrier of V
1 * W2 is Element of the carrier of V
(((r2 ") * r4) * W1) - (1 * W2) is Element of the carrier of V
- (1 * W2) is Element of the carrier of V
K194(V,(((r2 ") * r4) * W1),(- (1 * W2))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (1 * W2)) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (1 * W2))) is Element of the carrier of V
((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (1 * W2)))) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (1 * W2)))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - (1 * W2)))))) is Element of the carrier of V
(((r2 ") * r4) * W1) - W2 is Element of the carrier of V
- W2 is Element of the carrier of V
K194(V,(((r2 ") * r4) * W1),(- W2)) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - W2) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - W2)) is Element of the carrier of V
((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - W2))) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - W2))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * ((((u * r4) - (r2 * r3)) ") * ((((r2 ") * r4) * W1) - W2))))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * W2 is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)) - ((((u * r4) - (r2 * r3)) ") * W2) is Element of the carrier of V
- ((((u * r4) - (r2 * r3)) ") * W2) is Element of the carrier of V
K194(V,((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)),(- ((((u * r4) - (r2 * r3)) ") * W2))) is Element of the carrier of V
u * (((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)) - ((((u * r4) - (r2 * r3)) ") * W2)) is Element of the carrier of V
((r2 ") * W1) - (u * (((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)) - ((((u * r4) - (r2 * r3)) ") * W2))) is Element of the carrier of V
- (u * (((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)) - ((((u * r4) - (r2 * r3)) ") * W2))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * (((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)) - ((((u * r4) - (r2 * r3)) ") * W2))))) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * W2) is Element of the carrier of V
(u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))) - (u * ((((u * r4) - (r2 * r3)) ") * W2)) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * W2)) is Element of the carrier of V
K194(V,(u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))),(- (u * ((((u * r4) - (r2 * r3)) ") * W2)))) is Element of the carrier of V
((r2 ") * W1) - ((u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))) - (u * ((((u * r4) - (r2 * r3)) ") * W2))) is Element of the carrier of V
- ((u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))) - (u * ((((u * r4) - (r2 * r3)) ") * W2))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- ((u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))) - (u * ((((u * r4) - (r2 * r3)) ") * W2))))) is Element of the carrier of V
((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))) is Element of the carrier of V
- (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1))))) is Element of the carrier of V
(((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)))) + (u * ((((u * r4) - (r2 * r3)) ") * W2)) is Element of the carrier of V
u * (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
(u * (((u * r4) - (r2 * r3)) ")) * W2 is Element of the carrier of V
(((r2 ") * W1) - (u * ((((u * r4) - (r2 * r3)) ") * (((r2 ") * r4) * W1)))) + ((u * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
(u * (((u * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * W1) is Element of the carrier of V
((r2 ") * W1) - ((u * (((u * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * W1)) is Element of the carrier of V
- ((u * (((u * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * W1)) is Element of the carrier of V
K194(V,((r2 ") * W1),(- ((u * (((u * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * W1)))) is Element of the carrier of V
(((r2 ") * W1) - ((u * (((u * r4) - (r2 * r3)) ")) * (((r2 ") * r4) * W1))) + ((u * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
(u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4) is ext-real V25() V26() Element of REAL
((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * W1 is Element of the carrier of V
((r2 ") * W1) - (((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * W1) is Element of the carrier of V
- (((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * W1) is Element of the carrier of V
K194(V,((r2 ") * W1),(- (((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * W1))) is Element of the carrier of V
(((r2 ") * W1) - (((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) * W1)) + ((u * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
(r2 ") - ((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4)) is ext-real V25() V26() Element of REAL
((r2 ") - ((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4))) * W1 is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * u is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * u) * W2 is Element of the carrier of V
(((r2 ") - ((u * (((u * r4) - (r2 * r3)) ")) * ((r2 ") * r4))) * W1) + (((((u * r4) - (r2 * r3)) ") * u) * W2) is Element of the carrier of V
u * ((((u * r4) - (r2 * r3)) ") * r4) is ext-real V25() V26() Element of REAL
1 - (u * ((((u * r4) - (r2 * r3)) ") * r4)) is ext-real V25() V26() Element of REAL
(r2 ") * (1 - (u * ((((u * r4) - (r2 * r3)) ") * r4))) is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * (u * r4) is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3))) - ((((u * r4) - (r2 * r3)) ") * (u * r4)) is ext-real V25() V26() Element of REAL
(r2 ") * (((((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3))) - ((((u * r4) - (r2 * r3)) ") * (u * r4))) is ext-real V25() V26() Element of REAL
((r2 ") * r2) * (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
- r3 is ext-real V25() V26() Element of REAL
(((r2 ") * r2) * (((u * r4) - (r2 * r3)) ")) * (- r3) is ext-real V25() V26() Element of REAL
1 * (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
(1 * (((u * r4) - (r2 * r3)) ")) * (- r3) is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * r3 is ext-real V25() V26() Element of REAL
- ((((u * r4) - (r2 * r3)) ") * r3) is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * r3) * W1 is Element of the carrier of V
- (((((u * r4) - (r2 * r3)) ") * r3) * W1) is Element of the carrier of V
(- (((((u * r4) - (r2 * r3)) ") * r3) * W1)) + (((((u * r4) - (r2 * r3)) ") * u) * W2) is Element of the carrier of V
- ((((u * r4) - (r2 * r3)) ") * r2) is ext-real V25() V26() Element of REAL
u " is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * r2) * (u ") is ext-real V25() V26() Element of REAL
(((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3 is ext-real V25() V26() Element of REAL
(u ") + ((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * (r2 * r3) is ext-real V25() V26() Element of REAL
1 + ((((u * r4) - (r2 * r3)) ") * (r2 * r3)) is ext-real V25() V26() Element of REAL
(u ") * (1 + ((((u * r4) - (r2 * r3)) ") * (r2 * r3))) is ext-real V25() V26() Element of REAL
((((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3))) + ((((u * r4) - (r2 * r3)) ") * (r2 * r3)) is ext-real V25() V26() Element of REAL
(u ") * (((((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3))) + ((((u * r4) - (r2 * r3)) ") * (r2 * r3))) is ext-real V25() V26() Element of REAL
(u ") * u is ext-real V25() V26() Element of REAL
((u ") * u) * r4 is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * (((u ") * u) * r4) is ext-real V25() V26() Element of REAL
1 * r4 is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * (1 * r4) is ext-real V25() V26() Element of REAL
(u ") * W1 is Element of the carrier of V
(u ") * (u * v) is Element of the carrier of V
(u ") * (r2 * x) is Element of the carrier of V
((u ") * (u * v)) + ((u ") * (r2 * x)) is Element of the carrier of V
((u ") * u) * v is Element of the carrier of V
(((u ") * u) * v) + ((u ") * (r2 * x)) is Element of the carrier of V
(1 * v) + ((u ") * (r2 * x)) is Element of the carrier of V
v + ((u ") * (r2 * x)) is Element of the carrier of V
r2 * (u ") is ext-real V25() V26() Element of REAL
(r2 * (u ")) * x is Element of the carrier of V
v + ((r2 * (u ")) * x) is Element of the carrier of V
((u ") * W1) - ((r2 * (u ")) * x) is Element of the carrier of V
- ((r2 * (u ")) * x) is Element of the carrier of V
K194(V,((u ") * W1),(- ((r2 * (u ")) * x))) is Element of the carrier of V
r3 * ((u ") * W1) is Element of the carrier of V
r3 * ((r2 * (u ")) * x) is Element of the carrier of V
(r3 * ((u ") * W1)) - (r3 * ((r2 * (u ")) * x)) is Element of the carrier of V
- (r3 * ((r2 * (u ")) * x)) is Element of the carrier of V
K194(V,(r3 * ((u ") * W1)),(- (r3 * ((r2 * (u ")) * x)))) is Element of the carrier of V
((r3 * ((u ") * W1)) - (r3 * ((r2 * (u ")) * x))) + (r4 * x) is Element of the carrier of V
r3 * (u ") is ext-real V25() V26() Element of REAL
(r3 * (u ")) * W1 is Element of the carrier of V
(u ") * r2 is ext-real V25() V26() Element of REAL
((u ") * r2) * x is Element of the carrier of V
r3 * (((u ") * r2) * x) is Element of the carrier of V
((r3 * (u ")) * W1) - (r3 * (((u ") * r2) * x)) is Element of the carrier of V
- (r3 * (((u ") * r2) * x)) is Element of the carrier of V
K194(V,((r3 * (u ")) * W1),(- (r3 * (((u ") * r2) * x)))) is Element of the carrier of V
(((r3 * (u ")) * W1) - (r3 * (((u ") * r2) * x))) + (r4 * x) is Element of the carrier of V
r3 * ((u ") * r2) is ext-real V25() V26() Element of REAL
(r3 * ((u ") * r2)) * x is Element of the carrier of V
((r3 * (u ")) * W1) - ((r3 * ((u ") * r2)) * x) is Element of the carrier of V
- ((r3 * ((u ") * r2)) * x) is Element of the carrier of V
K194(V,((r3 * (u ")) * W1),(- ((r3 * ((u ") * r2)) * x))) is Element of the carrier of V
(((r3 * (u ")) * W1) - ((r3 * ((u ") * r2)) * x)) + (r4 * x) is Element of the carrier of V
r3 * r2 is ext-real V25() V26() Element of REAL
(u ") * (r3 * r2) is ext-real V25() V26() Element of REAL
((u ") * (r3 * r2)) * x is Element of the carrier of V
((r3 * (u ")) * W1) - (((u ") * (r3 * r2)) * x) is Element of the carrier of V
- (((u ") * (r3 * r2)) * x) is Element of the carrier of V
K194(V,((r3 * (u ")) * W1),(- (((u ") * (r3 * r2)) * x))) is Element of the carrier of V
(((r3 * (u ")) * W1) - (((u ") * (r3 * r2)) * x)) + (r4 * x) is Element of the carrier of V
(u ") * r3 is ext-real V25() V26() Element of REAL
((u ") * r3) * W1 is Element of the carrier of V
(r3 * r2) * x is Element of the carrier of V
(u ") * ((r3 * r2) * x) is Element of the carrier of V
(((u ") * r3) * W1) - ((u ") * ((r3 * r2) * x)) is Element of the carrier of V
- ((u ") * ((r3 * r2) * x)) is Element of the carrier of V
K194(V,(((u ") * r3) * W1),(- ((u ") * ((r3 * r2) * x)))) is Element of the carrier of V
((((u ") * r3) * W1) - ((u ") * ((r3 * r2) * x))) + (r4 * x) is Element of the carrier of V
r3 * W1 is Element of the carrier of V
(u ") * (r3 * W1) is Element of the carrier of V
((u ") * (r3 * W1)) - ((u ") * ((r3 * r2) * x)) is Element of the carrier of V
K194(V,((u ") * (r3 * W1)),(- ((u ") * ((r3 * r2) * x)))) is Element of the carrier of V
(((u ") * (r3 * W1)) - ((u ") * ((r3 * r2) * x))) + (r4 * x) is Element of the carrier of V
u * W2 is Element of the carrier of V
u * (((u ") * (r3 * W1)) - ((u ") * ((r3 * r2) * x))) is Element of the carrier of V
u * (r4 * x) is Element of the carrier of V
(u * (((u ") * (r3 * W1)) - ((u ") * ((r3 * r2) * x)))) + (u * (r4 * x)) is Element of the carrier of V
(u * r4) * x is Element of the carrier of V
(u * (((u ") * (r3 * W1)) - ((u ") * ((r3 * r2) * x)))) + ((u * r4) * x) is Element of the carrier of V
u * ((u ") * (r3 * W1)) is Element of the carrier of V
u * ((u ") * ((r3 * r2) * x)) is Element of the carrier of V
(u * ((u ") * (r3 * W1))) - (u * ((u ") * ((r3 * r2) * x))) is Element of the carrier of V
- (u * ((u ") * ((r3 * r2) * x))) is Element of the carrier of V
K194(V,(u * ((u ") * (r3 * W1))),(- (u * ((u ") * ((r3 * r2) * x))))) is Element of the carrier of V
((u * ((u ") * (r3 * W1))) - (u * ((u ") * ((r3 * r2) * x)))) + ((u * r4) * x) is Element of the carrier of V
u * (u ") is ext-real V25() V26() Element of REAL
(u * (u ")) * (r3 * W1) is Element of the carrier of V
((u * (u ")) * (r3 * W1)) - (u * ((u ") * ((r3 * r2) * x))) is Element of the carrier of V
K194(V,((u * (u ")) * (r3 * W1)),(- (u * ((u ") * ((r3 * r2) * x))))) is Element of the carrier of V
(((u * (u ")) * (r3 * W1)) - (u * ((u ") * ((r3 * r2) * x)))) + ((u * r4) * x) is Element of the carrier of V
(u * (u ")) * ((r3 * r2) * x) is Element of the carrier of V
((u * (u ")) * (r3 * W1)) - ((u * (u ")) * ((r3 * r2) * x)) is Element of the carrier of V
- ((u * (u ")) * ((r3 * r2) * x)) is Element of the carrier of V
K194(V,((u * (u ")) * (r3 * W1)),(- ((u * (u ")) * ((r3 * r2) * x)))) is Element of the carrier of V
(((u * (u ")) * (r3 * W1)) - ((u * (u ")) * ((r3 * r2) * x))) + ((u * r4) * x) is Element of the carrier of V
1 * (r3 * W1) is Element of the carrier of V
(1 * (r3 * W1)) - ((u * (u ")) * ((r3 * r2) * x)) is Element of the carrier of V
K194(V,(1 * (r3 * W1)),(- ((u * (u ")) * ((r3 * r2) * x)))) is Element of the carrier of V
((1 * (r3 * W1)) - ((u * (u ")) * ((r3 * r2) * x))) + ((u * r4) * x) is Element of the carrier of V
1 * ((r3 * r2) * x) is Element of the carrier of V
(1 * (r3 * W1)) - (1 * ((r3 * r2) * x)) is Element of the carrier of V
- (1 * ((r3 * r2) * x)) is Element of the carrier of V
K194(V,(1 * (r3 * W1)),(- (1 * ((r3 * r2) * x)))) is Element of the carrier of V
((1 * (r3 * W1)) - (1 * ((r3 * r2) * x))) + ((u * r4) * x) is Element of the carrier of V
(r3 * W1) - (1 * ((r3 * r2) * x)) is Element of the carrier of V
K194(V,(r3 * W1),(- (1 * ((r3 * r2) * x)))) is Element of the carrier of V
((r3 * W1) - (1 * ((r3 * r2) * x))) + ((u * r4) * x) is Element of the carrier of V
(r3 * W1) - ((r3 * r2) * x) is Element of the carrier of V
- ((r3 * r2) * x) is Element of the carrier of V
K194(V,(r3 * W1),(- ((r3 * r2) * x))) is Element of the carrier of V
((r3 * W1) - ((r3 * r2) * x)) + ((u * r4) * x) is Element of the carrier of V
((r3 * r2) * x) - ((u * r4) * x) is Element of the carrier of V
- ((u * r4) * x) is Element of the carrier of V
K194(V,((r3 * r2) * x),(- ((u * r4) * x))) is Element of the carrier of V
(r3 * W1) - (((r3 * r2) * x) - ((u * r4) * x)) is Element of the carrier of V
- (((r3 * r2) * x) - ((u * r4) * x)) is Element of the carrier of V
K194(V,(r3 * W1),(- (((r3 * r2) * x) - ((u * r4) * x)))) is Element of the carrier of V
(r3 * r2) - (u * r4) is ext-real V25() V26() Element of REAL
((r3 * r2) - (u * r4)) * x is Element of the carrier of V
- (((r3 * r2) - (u * r4)) * x) is Element of the carrier of V
(r3 * W1) + (- (((r3 * r2) - (u * r4)) * x)) is Element of the carrier of V
- ((r3 * r2) - (u * r4)) is ext-real V25() V26() Element of REAL
(- ((r3 * r2) - (u * r4))) * x is Element of the carrier of V
(r3 * W1) + ((- ((r3 * r2) - (u * r4))) * x) is Element of the carrier of V
((u * r4) - (r2 * r3)) * x is Element of the carrier of V
(r3 * W1) + (((u * r4) - (r2 * r3)) * x) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (u * W2) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (r3 * W1) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (((u * r4) - (r2 * r3)) * x) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r3 * W1)) + ((((u * r4) - (r2 * r3)) ") * (((u * r4) - (r2 * r3)) * x)) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3))) * x is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r3 * W1)) + (((((u * r4) - (r2 * r3)) ") * ((u * r4) - (r2 * r3))) * x) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r3 * W1)) + (1 * x) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (r3 * W1)) + x is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * (u * W2)) - ((((u * r4) - (r2 * r3)) ") * (r3 * W1)) is Element of the carrier of V
- ((((u * r4) - (r2 * r3)) ") * (r3 * W1)) is Element of the carrier of V
K194(V,((((u * r4) - (r2 * r3)) ") * (u * W2)),(- ((((u * r4) - (r2 * r3)) ") * (r3 * W1)))) is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * u) * W2) - ((((u * r4) - (r2 * r3)) ") * (r3 * W1)) is Element of the carrier of V
K194(V,(((((u * r4) - (r2 * r3)) ") * u) * W2),(- ((((u * r4) - (r2 * r3)) ") * (r3 * W1)))) is Element of the carrier of V
(r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1)) is Element of the carrier of V
(r2 * (u ")) * (((((u * r4) - (r2 * r3)) ") * u) * W2) is Element of the carrier of V
((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (u ")) * (((((u * r4) - (r2 * r3)) ") * u) * W2)) is Element of the carrier of V
((u ") * W1) - (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (u ")) * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (u ")) * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
K194(V,((u ") * W1),(- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (u ")) * (((((u * r4) - (r2 * r3)) ") * u) * W2))))) is Element of the carrier of V
(r2 * (u ")) * ((((u * r4) - (r2 * r3)) ") * u) is ext-real V25() V26() Element of REAL
((r2 * (u ")) * ((((u * r4) - (r2 * r3)) ") * u)) * W2 is Element of the carrier of V
((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + (((r2 * (u ")) * ((((u * r4) - (r2 * r3)) ") * u)) * W2) is Element of the carrier of V
((u ") * W1) - (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + (((r2 * (u ")) * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + (((r2 * (u ")) * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + (((r2 * (u ")) * ((((u * r4) - (r2 * r3)) ") * u)) * W2)))) is Element of the carrier of V
((u ") * u) * (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
r2 * (((u ") * u) * (((u * r4) - (r2 * r3)) ")) is ext-real V25() V26() Element of REAL
(r2 * (((u ") * u) * (((u * r4) - (r2 * r3)) "))) * W2 is Element of the carrier of V
((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (((u ") * u) * (((u * r4) - (r2 * r3)) "))) * W2) is Element of the carrier of V
((u ") * W1) - (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (((u ") * u) * (((u * r4) - (r2 * r3)) "))) * W2)) is Element of the carrier of V
- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (((u ") * u) * (((u * r4) - (r2 * r3)) "))) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (((u ") * u) * (((u * r4) - (r2 * r3)) "))) * W2)))) is Element of the carrier of V
r2 * (1 * (((u * r4) - (r2 * r3)) ")) is ext-real V25() V26() Element of REAL
(r2 * (1 * (((u * r4) - (r2 * r3)) "))) * W2 is Element of the carrier of V
((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (1 * (((u * r4) - (r2 * r3)) "))) * W2) is Element of the carrier of V
((u ") * W1) - (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (1 * (((u * r4) - (r2 * r3)) "))) * W2)) is Element of the carrier of V
- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (1 * (((u * r4) - (r2 * r3)) "))) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- (((r2 * (u ")) * (- (((((u * r4) - (r2 * r3)) ") * r3) * W1))) + ((r2 * (1 * (((u * r4) - (r2 * r3)) "))) * W2)))) is Element of the carrier of V
(r2 * (u ")) * (- ((((u * r4) - (r2 * r3)) ") * (r3 * W1))) is Element of the carrier of V
r2 * (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
(r2 * (((u * r4) - (r2 * r3)) ")) * W2 is Element of the carrier of V
((r2 * (u ")) * (- ((((u * r4) - (r2 * r3)) ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - (((r2 * (u ")) * (- ((((u * r4) - (r2 * r3)) ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- (((r2 * (u ")) * (- ((((u * r4) - (r2 * r3)) ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- (((r2 * (u ")) * (- ((((u * r4) - (r2 * r3)) ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
(- (((u * r4) - (r2 * r3)) ")) * (r3 * W1) is Element of the carrier of V
(r2 * (u ")) * ((- (((u * r4) - (r2 * r3)) ")) * (r3 * W1)) is Element of the carrier of V
((r2 * (u ")) * ((- (((u * r4) - (r2 * r3)) ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - (((r2 * (u ")) * ((- (((u * r4) - (r2 * r3)) ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- (((r2 * (u ")) * ((- (((u * r4) - (r2 * r3)) ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- (((r2 * (u ")) * ((- (((u * r4) - (r2 * r3)) ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
(r2 * (u ")) * (- (((u * r4) - (r2 * r3)) ")) is ext-real V25() V26() Element of REAL
((r2 * (u ")) * (- (((u * r4) - (r2 * r3)) "))) * (r3 * W1) is Element of the carrier of V
(((r2 * (u ")) * (- (((u * r4) - (r2 * r3)) "))) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - ((((r2 * (u ")) * (- (((u * r4) - (r2 * r3)) "))) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- ((((r2 * (u ")) * (- (((u * r4) - (r2 * r3)) "))) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- ((((r2 * (u ")) * (- (((u * r4) - (r2 * r3)) "))) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
(- 1) * (((u * r4) - (r2 * r3)) ") is ext-real V25() V26() Element of REAL
((- 1) * (((u * r4) - (r2 * r3)) ")) * r2 is ext-real V25() V26() Element of REAL
(((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * (u ") is ext-real V25() V26() Element of REAL
((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * (u ")) * (r3 * W1) is Element of the carrier of V
(((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * (u ")) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - ((((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * (u ")) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- ((((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * (u ")) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- ((((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * (u ")) * (r3 * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
(((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * ((u ") * (r3 * W1)) is Element of the carrier of V
((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * ((u ") * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - (((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * ((u ") * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- (((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * ((u ") * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- (((((- 1) * (((u * r4) - (r2 * r3)) ")) * r2) * ((u ") * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
r2 * ((u ") * (r3 * W1)) is Element of the carrier of V
((- 1) * (((u * r4) - (r2 * r3)) ")) * (r2 * ((u ") * (r3 * W1))) is Element of the carrier of V
(((- 1) * (((u * r4) - (r2 * r3)) ")) * (r2 * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - ((((- 1) * (((u * r4) - (r2 * r3)) ")) * (r2 * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- ((((- 1) * (((u * r4) - (r2 * r3)) ")) * (r2 * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- ((((- 1) * (((u * r4) - (r2 * r3)) ")) * (r2 * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
(((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))) is Element of the carrier of V
(- 1) * ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1)))) is Element of the carrier of V
((- 1) * ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - (((- 1) * ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- (((- 1) * ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- (((- 1) * ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
- ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1)))) is Element of the carrier of V
(- ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - ((- ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- ((- ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- ((- ((((u * r4) - (r2 * r3)) ") * (r2 * ((u ") * (r3 * W1))))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
((((u * r4) - (r2 * r3)) ") * r2) * ((u ") * (r3 * W1)) is Element of the carrier of V
- (((((u * r4) - (r2 * r3)) ") * r2) * ((u ") * (r3 * W1))) is Element of the carrier of V
(- (((((u * r4) - (r2 * r3)) ") * r2) * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - ((- (((((u * r4) - (r2 * r3)) ") * r2) * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- ((- (((((u * r4) - (r2 * r3)) ") * r2) * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- ((- (((((u * r4) - (r2 * r3)) ") * r2) * ((u ") * (r3 * W1)))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * (r3 * W1) is Element of the carrier of V
- ((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * (r3 * W1)) is Element of the carrier of V
(- ((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - ((- ((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- ((- ((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- ((- ((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * (r3 * W1))) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1 is Element of the carrier of V
- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1) is Element of the carrier of V
(- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
((u ") * W1) - ((- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
- ((- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)) is Element of the carrier of V
K194(V,((u ") * W1),(- ((- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)) + ((r2 * (((u * r4) - (r2 * r3)) ")) * W2)))) is Element of the carrier of V
((u ") * W1) - (- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)) is Element of the carrier of V
- (- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)) is Element of the carrier of V
K194(V,((u ") * W1),(- (- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)))) is Element of the carrier of V
(((u ") * W1) - (- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1))) - ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
- ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
K194(V,(((u ") * W1) - (- (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1))),(- ((r2 * (((u * r4) - (r2 * r3)) ")) * W2))) is Element of the carrier of V
((u ") * W1) + (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1) is Element of the carrier of V
(((u ") * W1) + (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)) - ((r2 * (((u * r4) - (r2 * r3)) ")) * W2) is Element of the carrier of V
K194(V,(((u ") * W1) + (((((((u * r4) - (r2 * r3)) ") * r2) * (u ")) * r3) * W1)),(- ((r2 * (((u * r4) - (r2 * r3)) ")) * W2))) is Element of the carrier of V
(- ((((u * r4) - (r2 * r3)) ") * r2)) * W2 is Element of the carrier of V
(((((u * r4) - (r2 * r3)) ") * r4) * W1) + ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2) is Element of the carrier of V
(- ((((u * r4) - (r2 * r3)) ") * r3)) * W1 is Element of the carrier of V
((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1) + (((((u * r4) - (r2 * r3)) ") * u) * W2) is Element of the carrier of V
a is Element of the carrier of V
b is ext-real V25() V26() Element of REAL
b * v is Element of the carrier of V
r6 is ext-real V25() V26() Element of REAL
r6 * x is Element of the carrier of V
(b * v) + (r6 * x) is Element of the carrier of V
b * (((((u * r4) - (r2 * r3)) ") * r4) * W1) is Element of the carrier of V
b * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2) is Element of the carrier of V
(b * (((((u * r4) - (r2 * r3)) ") * r4) * W1)) + (b * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2)) is Element of the carrier of V
r6 * (((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1) + (((((u * r4) - (r2 * r3)) ") * u) * W2)) is Element of the carrier of V
((b * (((((u * r4) - (r2 * r3)) ") * r4) * W1)) + (b * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + (r6 * (((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1) + (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
r6 * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1) is Element of the carrier of V
r6 * (((((u * r4) - (r2 * r3)) ") * u) * W2) is Element of the carrier of V
(r6 * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + (r6 * (((((u * r4) - (r2 * r3)) ") * u) * W2)) is Element of the carrier of V
((b * (((((u * r4) - (r2 * r3)) ") * r4) * W1)) + (b * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + ((r6 * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + (r6 * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
b * ((((u * r4) - (r2 * r3)) ") * r4) is ext-real V25() V26() Element of REAL
(b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1 is Element of the carrier of V
((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (b * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2)) is Element of the carrier of V
(((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (b * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + ((r6 * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + (r6 * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
b * (- ((((u * r4) - (r2 * r3)) ") * r2)) is ext-real V25() V26() Element of REAL
(b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2 is Element of the carrier of V
((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) is Element of the carrier of V
(((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2)) + ((r6 * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + (r6 * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
r6 * (- ((((u * r4) - (r2 * r3)) ") * r3)) is ext-real V25() V26() Element of REAL
(r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1 is Element of the carrier of V
((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + (r6 * (((((u * r4) - (r2 * r3)) ") * u) * W2)) is Element of the carrier of V
(((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2)) + (((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + (r6 * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
r6 * ((((u * r4) - (r2 * r3)) ") * u) is ext-real V25() V26() Element of REAL
(r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2 is Element of the carrier of V
((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2) is Element of the carrier of V
(((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2)) + (((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + (((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + (((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2))) is Element of the carrier of V
((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2) is Element of the carrier of V
((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2))) is Element of the carrier of V
((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) is Element of the carrier of V
(((b * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1)) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
(b * ((((u * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((u * r4) - (r2 * r3)) ") * r3))) is ext-real V25() V26() Element of REAL
((b * ((((u * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((u * r4) - (r2 * r3)) ") * r3)))) * W1 is Element of the carrier of V
(((b * ((((u * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((u * r4) - (r2 * r3)) ") * r3)))) * W1) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((r6 * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
(b * (- ((((u * r4) - (r2 * r3)) ") * r2))) + (r6 * ((((u * r4) - (r2 * r3)) ") * u)) is ext-real V25() V26() Element of REAL
((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) + (r6 * ((((u * r4) - (r2 * r3)) ") * u))) * W2 is Element of the carrier of V
(((b * ((((u * r4) - (r2 * r3)) ") * r4)) + (r6 * (- ((((u * r4) - (r2 * r3)) ") * r3)))) * W1) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r2))) + (r6 * ((((u * r4) - (r2 * r3)) ") * u))) * W2) is Element of the carrier of V
b is ext-real V25() V26() Element of REAL
b * W1 is Element of the carrier of V
r6 is ext-real V25() V26() Element of REAL
r6 * W2 is Element of the carrier of V
(b * W1) + (r6 * W2) is Element of the carrier of V
b * ((u * v) + (r2 * x)) is Element of the carrier of V
r6 * (r3 * v) is Element of the carrier of V
r6 * (r4 * x) is Element of the carrier of V
(r6 * (r3 * v)) + (r6 * (r4 * x)) is Element of the carrier of V
(b * ((u * v) + (r2 * x))) + ((r6 * (r3 * v)) + (r6 * (r4 * x))) is Element of the carrier of V
b * (u * v) is Element of the carrier of V
b * (r2 * x) is Element of the carrier of V
(b * (u * v)) + (b * (r2 * x)) is Element of the carrier of V
((b * (u * v)) + (b * (r2 * x))) + ((r6 * (r3 * v)) + (r6 * (r4 * x))) is Element of the carrier of V
((b * (u * v)) + (b * (r2 * x))) + (r6 * (r3 * v)) is Element of the carrier of V
(((b * (u * v)) + (b * (r2 * x))) + (r6 * (r3 * v))) + (r6 * (r4 * x)) is Element of the carrier of V
(b * (u * v)) + (r6 * (r3 * v)) is Element of the carrier of V
((b * (u * v)) + (r6 * (r3 * v))) + (b * (r2 * x)) is Element of the carrier of V
(((b * (u * v)) + (r6 * (r3 * v))) + (b * (r2 * x))) + (r6 * (r4 * x)) is Element of the carrier of V
b * u is ext-real V25() V26() Element of REAL
(b * u) * v is Element of the carrier of V
((b * u) * v) + (r6 * (r3 * v)) is Element of the carrier of V
(((b * u) * v) + (r6 * (r3 * v))) + (b * (r2 * x)) is Element of the carrier of V
((((b * u) * v) + (r6 * (r3 * v))) + (b * (r2 * x))) + (r6 * (r4 * x)) is Element of the carrier of V
r6 * r3 is ext-real V25() V26() Element of REAL
(r6 * r3) * v is Element of the carrier of V
((b * u) * v) + ((r6 * r3) * v) is Element of the carrier of V
(((b * u) * v) + ((r6 * r3) * v)) + (b * (r2 * x)) is Element of the carrier of V
((((b * u) * v) + ((r6 * r3) * v)) + (b * (r2 * x))) + (r6 * (r4 * x)) is Element of the carrier of V
b * r2 is ext-real V25() V26() Element of REAL
(b * r2) * x is Element of the carrier of V
(((b * u) * v) + ((r6 * r3) * v)) + ((b * r2) * x) is Element of the carrier of V
((((b * u) * v) + ((r6 * r3) * v)) + ((b * r2) * x)) + (r6 * (r4 * x)) is Element of the carrier of V
r6 * r4 is ext-real V25() V26() Element of REAL
(r6 * r4) * x is Element of the carrier of V
((((b * u) * v) + ((r6 * r3) * v)) + ((b * r2) * x)) + ((r6 * r4) * x) is Element of the carrier of V
(b * u) + (r6 * r3) is ext-real V25() V26() Element of REAL
((b * u) + (r6 * r3)) * v is Element of the carrier of V
(((b * u) + (r6 * r3)) * v) + ((b * r2) * x) is Element of the carrier of V
((((b * u) + (r6 * r3)) * v) + ((b * r2) * x)) + ((r6 * r4) * x) is Element of the carrier of V
((b * r2) * x) + ((r6 * r4) * x) is Element of the carrier of V
(((b * u) + (r6 * r3)) * v) + (((b * r2) * x) + ((r6 * r4) * x)) is Element of the carrier of V
(b * r2) + (r6 * r4) is ext-real V25() V26() Element of REAL
((b * r2) + (r6 * r4)) * x is Element of the carrier of V
(((b * u) + (r6 * r3)) * v) + (((b * r2) + (r6 * r4)) * x) is Element of the carrier of V
a is ext-real V25() V26() Element of REAL
a * v is Element of the carrier of V
b is ext-real V25() V26() Element of REAL
b * x is Element of the carrier of V
(a * v) + (b * x) is Element of the carrier of V
a * (((((u * r4) - (r2 * r3)) ") * r4) * W1) is Element of the carrier of V
a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2) is Element of the carrier of V
(a * (((((u * r4) - (r2 * r3)) ") * r4) * W1)) + (a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2)) is Element of the carrier of V
b * (((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1) + (((((u * r4) - (r2 * r3)) ") * u) * W2)) is Element of the carrier of V
((a * (((((u * r4) - (r2 * r3)) ") * r4) * W1)) + (a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + (b * (((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1) + (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
b * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1) is Element of the carrier of V
b * (((((u * r4) - (r2 * r3)) ") * u) * W2) is Element of the carrier of V
(b * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + (b * (((((u * r4) - (r2 * r3)) ") * u) * W2)) is Element of the carrier of V
((a * (((((u * r4) - (r2 * r3)) ") * r4) * W1)) + (a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + ((b * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + (b * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
a * ((((u * r4) - (r2 * r3)) ") * r4) is ext-real V25() V26() Element of REAL
(a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1 is Element of the carrier of V
((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2)) is Element of the carrier of V
(((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + ((b * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + (b * (((((u * r4) - (r2 * r3)) ") * u) * W2))) is Element of the carrier of V
b * ((((u * r4) - (r2 * r3)) ") * u) is ext-real V25() V26() Element of REAL
(b * ((((u * r4) - (r2 * r3)) ") * u)) * W2 is Element of the carrier of V
(b * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2) is Element of the carrier of V
(((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + ((b * ((- ((((u * r4) - (r2 * r3)) ") * r3)) * W1)) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
b * (- ((((u * r4) - (r2 * r3)) ") * r3)) is ext-real V25() V26() Element of REAL
(b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1 is Element of the carrier of V
((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2) is Element of the carrier of V
(((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (a * ((- ((((u * r4) - (r2 * r3)) ") * r2)) * W2))) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
a * (- ((((u * r4) - (r2 * r3)) ") * r2)) is ext-real V25() V26() Element of REAL
(a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2 is Element of the carrier of V
((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) is Element of the carrier of V
(((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2)) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2))) is Element of the carrier of V
((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2) is Element of the carrier of V
((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + (((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + (((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) + (((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2))) is Element of the carrier of V
((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1) is Element of the carrier of V
(((a * ((((u * r4) - (r2 * r3)) ") * r4)) * W1) + ((b * (- ((((u * r4) - (r2 * r3)) ") * r3))) * W1)) + (((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
(a * ((((u * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((u * r4) - (r2 * r3)) ") * r3))) is ext-real V25() V26() Element of REAL
((a * ((((u * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((u * r4) - (r2 * r3)) ") * r3)))) * W1 is Element of the carrier of V
(((a * ((((u * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((u * r4) - (r2 * r3)) ") * r3)))) * W1) + (((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) * W2) + ((b * ((((u * r4) - (r2 * r3)) ") * u)) * W2)) is Element of the carrier of V
(a * (- ((((u * r4) - (r2 * r3)) ") * r2))) + (b * ((((u * r4) - (r2 * r3)) ") * u)) is ext-real V25() V26() Element of REAL
((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) + (b * ((((u * r4) - (r2 * r3)) ") * u))) * W2 is Element of the carrier of V
(((a * ((((u * r4) - (r2 * r3)) ") * r4)) + (b * (- ((((u * r4) - (r2 * r3)) ") * r3)))) * W1) + (((a * (- ((((u * r4) - (r2 * r3)) ") * r2))) + (b * ((((u * r4) - (r2 * r3)) ") * u))) * W2) is Element of the carrier of V
r4 * a is ext-real V25() V26() Element of REAL
(- r3) * b is ext-real V25() V26() Element of REAL
(r4 * a) + ((- r3) * b) is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * ((r4 * a) + ((- r3) * b)) is ext-real V25() V26() Element of REAL
r3 * b is ext-real V25() V26() Element of REAL
(r4 * a) - (r3 * b) is ext-real V25() V26() Element of REAL
(- r2) * a is ext-real V25() V26() Element of REAL
u * b is ext-real V25() V26() Element of REAL
((- r2) * a) + (u * b) is ext-real V25() V26() Element of REAL
(((u * r4) - (r2 * r3)) ") * (((- r2) * a) + (u * b)) is ext-real V25() V26() Element of REAL
r2 * a is ext-real V25() V26() Element of REAL
- (r2 * a) is ext-real V25() V26() Element of REAL
(u * b) + (- (r2 * a)) is ext-real V25() V26() Element of REAL
a " is ext-real V25() V26() Element of REAL
(a ") * (u * b) is ext-real V25() V26() Element of REAL
(a ") * a is ext-real V25() V26() Element of REAL
((a ") * a) * r2 is ext-real V25() V26() Element of REAL
1 * r2 is ext-real V25() V26() Element of REAL
(a ") * b is ext-real V25() V26() Element of REAL
u * ((a ") * b) is ext-real V25() V26() Element of REAL
((a ") * b) * x is Element of the carrier of V
u * (((a ") * b) * x) is Element of the carrier of V
(u * v) + (u * (((a ") * b) * x)) is Element of the carrier of V
v + (((a ") * b) * x) is Element of the carrier of V
u * (v + (((a ") * b) * x)) is Element of the carrier of V
((a ") * a) * r4 is ext-real V25() V26() Element of REAL
(a ") * (r3 * b) is ext-real V25() V26() Element of REAL
r3 * ((a ") * b) is ext-real V25() V26() Element of REAL
r3 * (((a ") * b) * x) is Element of the carrier of V
(r3 * v) + (r3 * (((a ") * b) * x)) is Element of the carrier of V
r3 * (v + (((a ") * b) * x)) is Element of the carrier of V
b " is ext-real V25() V26() Element of REAL
(b ") * b is ext-real V25() V26() Element of REAL
((b ") * b) * u is ext-real V25() V26() Element of REAL
(b ") * (r2 * a) is ext-real V25() V26() Element of REAL
1 * u is ext-real V25() V26() Element of REAL
(b ") * a is ext-real V25() V26() Element of REAL
r2 * ((b ") * a) is ext-real V25() V26() Element of REAL
((b ") * a) * v is Element of the carrier of V
r2 * (((b ") * a) * v) is Element of the carrier of V
(r2 * (((b ") * a) * v)) + (r2 * x) is Element of the carrier of V
(((b ") * a) * v) + x is Element of the carrier of V
r2 * ((((b ") * a) * v) + x) is Element of the carrier of V
((b ") * b) * r3 is ext-real V25() V26() Element of REAL
(b ") * (r4 * a) is ext-real V25() V26() Element of REAL
1 * r3 is ext-real V25() V26() Element of REAL
r4 * ((b ") * a) is ext-real V25() V26() Element of REAL
r4 * (((b ") * a) * v) is Element of the carrier of V
(r4 * (((b ") * a) * v)) + (r4 * x) is Element of the carrier of V
r4 * ((((b ") * a) * v) + x) is Element of the carrier of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
(0). V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
W1 is set
0. V is V55(V) Element of the carrier of V
the carrier of V is non empty set
v is set
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
0. W2 is V55(W2) Element of the carrier of W2
the carrier of W2 is non empty set
(0). W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of W2
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W1 /\ W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 /\ v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W1 + W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 + v is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V
V is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
W1 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
W2 is non empty V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V
v is Element of the carrier of V
v + W1 is Element of bool the carrier of V
bool the carrier of V is non empty set
v + W2 is Element of bool the carrier of V
x is set
u is Element of the carrier of V
v + u is Element of the carrier of V