:: RLAFFIN1 semantic presentation

REAL is non empty non trivial non finite V65() V66() V67() V71() set
NAT is non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() Element of K19(REAL)
K19(REAL) is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V65() V71() set
RAT is non empty non trivial non finite V65() V66() V67() V68() V71() set
INT is non empty non trivial non finite V65() V66() V67() V68() V69() V71() set
K20(COMPLEX,COMPLEX) is Relation-like non empty non trivial non finite V55() set
K19(K20(COMPLEX,COMPLEX)) is non empty non trivial non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like non empty non trivial non finite V55() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty non trivial non finite set
K20(REAL,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set
K19(K20(REAL,REAL)) is non empty non trivial non finite set
K20(K20(REAL,REAL),REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set
K19(K20(K20(REAL,REAL),REAL)) is non empty non trivial non finite set
K20(RAT,RAT) is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set
K19(K20(RAT,RAT)) is non empty non trivial non finite set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued non empty non trivial non finite V55() V56() V57() set
K19(K20(K20(RAT,RAT),RAT)) is non empty non trivial non finite set
K20(INT,INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set
K19(K20(INT,INT)) is non empty non trivial non finite set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued non empty non trivial non finite V55() V56() V57() set
K19(K20(K20(INT,INT),INT)) is non empty non trivial non finite set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
K19(K20(K20(NAT,NAT),NAT)) is non empty set
omega is non trivial ordinal non finite cardinal limit_cardinal V65() V66() V67() V68() V69() V70() V71() set
K19(omega) is non empty non trivial non finite set
K19(NAT) is non empty non trivial non finite set
{} is set
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() set
2 is non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
K204(NAT) is V54() set
1 is non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
K20(NAT,REAL) is Relation-like non trivial non finite V55() V56() V57() set
K19(K20(NAT,REAL)) is non empty non trivial non finite set
0 is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
- 1 is non empty V24() V32() ext-real non positive negative Element of REAL
<*> REAL is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (<*> REAL) is V24() V32() ext-real Element of REAL
K148() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like non empty total quasi_total V21( REAL ) V22( REAL ) V55() V56() V57() V215( REAL ) Element of K19(K20(K20(REAL,REAL),REAL))
K406(REAL,(<*> REAL),K148()) is V24() V32() ext-real Element of REAL
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() convex Element of K19( the carrier of r) is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() convex Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
v is set
w is set
[#] r is non empty non proper Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is non empty Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of r is non empty set
V is Element of the carrier of r
{V} is non empty trivial finite 1 -element Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
conv {V} is non empty convex Element of K19( the carrier of r)
Convex-Family {V} is Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family {V}) is Element of K19( the carrier of r)
v is Element of the carrier of r
w is Element of the carrier of r
p is V24() V32() ext-real Element of REAL
p * v is Element of the carrier of r
1 - p is V24() V32() ext-real Element of REAL
(1 - p) * w is Element of the carrier of r
(p * v) + ((1 - p) * w) is Element of the carrier of r
p + (1 - p) is V24() V32() ext-real Element of REAL
(p + (1 - p)) * v is Element of the carrier of r
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
conv v is convex Element of K19( the carrier of r)
Convex-Family v is Element of K19(K19( the carrier of r))
meet (Convex-Family v) is Element of K19( the carrier of r)
w is set
p is Element of K19( the carrier of r)
[#] r is non empty non proper Element of K19( the carrier of r)
w is set
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
v is Element of K19( the carrier of r)
V is Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
V \/ v is Element of K19( the carrier of r)
conv (V \/ v) is convex Element of K19( the carrier of r)
Convex-Family (V \/ v) is Element of K19(K19( the carrier of r))
meet (Convex-Family (V \/ v)) is Element of K19( the carrier of r)
r is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
V \ v is Element of K19( the carrier of r)
w is Element of the carrier of r
w + V is Element of K19( the carrier of r)
{ (w + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
w + v is Element of K19( the carrier of r)
{ (w + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
(w + V) \ (w + v) is Element of K19( the carrier of r)
w + (V \ v) is Element of K19( the carrier of r)
{ (w + b₁) where b₁ is Element of the carrier of r : b₁ in V \ v } is set
p is set
I is Element of the carrier of r
w + I is Element of the carrier of r
p is set
I is Element of the carrier of r
w + I is Element of the carrier of r
A is Element of the carrier of r
w + A is Element of the carrier of r
r is non empty addLoopStr
the carrier of r is non empty set
V is Element of the carrier of r
v is Element of the carrier of r
V + v is Element of the carrier of r
{(V + v)} is non empty trivial finite 1 -element Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{v} is non empty trivial finite 1 -element Element of K19( the carrier of r)
V + {v} is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in {v} } is set
w is set
w is set
p is Element of the carrier of r
V + p is Element of the carrier of r
r is non empty add-associative addLoopStr
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of the carrier of r
w is Element of the carrier of r
v + w is Element of the carrier of r
(v + w) + V is Element of K19( the carrier of r)
{ ((v + w) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
w + V is Element of K19( the carrier of r)
{ (w + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
v + (w + V) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in w + V } is set
I is set
A is Element of the carrier of r
(v + w) + A is Element of the carrier of r
w + A is Element of the carrier of r
v + (w + A) is Element of the carrier of r
I is set
A is Element of the carrier of r
v + A is Element of the carrier of r
u2 is Element of the carrier of r
w + u2 is Element of the carrier of r
(v + w) + u2 is Element of the carrier of r
r is non empty Abelian right_zeroed V135() addLoopStr
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
V is Element of K19( the carrier of r)
(0. r) + V is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
v is set
w is Element of the carrier of r
(0. r) + w is Element of the carrier of r
v is set
w is Element of the carrier of r
(0. r) + w is Element of the carrier of r
r is non empty addLoopStr
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
card V is ordinal cardinal set
v is Element of the carrier of r
v + V is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
card (v + V) is ordinal cardinal set
{ H₁(b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
card { H₁(b₁) where b₁ is Element of the carrier of r : b₁ in V } is ordinal cardinal set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of the carrier of r
v is Element of K19( the carrier of r)
card v is ordinal cardinal set
V + v is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
card (V + v) is ordinal cardinal set
- V is Element of the carrier of r
(- V) + (V + v) is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in V + v } is set
(- V) + V is Element of the carrier of r
((- V) + V) + v is Element of K19( the carrier of r)
{ (((- V) + V) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(0. r) + v is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
r is non empty addLoopStr
the carrier of r is non empty set
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
V is Element of the carrier of r
V + ({} r) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in {} r } is set
v is set
w is Element of the carrier of r
V + w is Element of the carrier of r
r is V24() V32() ext-real Element of REAL
V is non empty RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of K19( the carrier of V)
w is Element of K19( the carrier of V)
r * v is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
r * w is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
p is set
I is Element of the carrier of V
r * I is Element of the carrier of V
r is V24() V32() ext-real Element of REAL
V is V24() V32() ext-real Element of REAL
r * V is V24() V32() ext-real Element of REAL
v is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
K19( the carrier of v) is non empty set
w is Element of K19( the carrier of v)
(r * V) * w is Element of K19( the carrier of v)
{ ((r * V) * b₁) where b₁ is Element of the carrier of v : b₁ in w } is set
V * w is Element of K19( the carrier of v)
{ (V * b₁) where b₁ is Element of the carrier of v : b₁ in w } is set
r * (V * w) is Element of K19( the carrier of v)
{ (r * b₁) where b₁ is Element of the carrier of v : b₁ in V * w } is set
I is set
A is Element of the carrier of v
(r * V) * A is Element of the carrier of v
V * A is Element of the carrier of v
r * (V * A) is Element of the carrier of v
I is set
A is Element of the carrier of v
r * A is Element of the carrier of v
u2 is Element of the carrier of v
V * u2 is Element of the carrier of v
(r * V) * u2 is Element of the carrier of v
r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
1 * V is Element of K19( the carrier of r)
{ (1 * b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
v is set
w is Element of the carrier of r
1 * w is Element of the carrier of r
v is set
w is Element of the carrier of r
1 * w is Element of the carrier of r
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element Element of K19( the carrier of r)
V is Element of K19( the carrier of r)
0 * V is Element of K19( the carrier of r)
{ (0 * b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
v is set
w is Element of the carrier of r
0 * w is Element of the carrier of r
r is non empty addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
V + v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
(V + v) * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
V * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
v * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
(V * w) + (v * w) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
K376(K148(),(V * w),(v * w)) is set
len (V * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len (v * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
(len w) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
len ((V + v) * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
A is V24() ordinal natural V32() ext-real non negative finite cardinal set
dom ((V + v) * w) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
((V + v) * w) . A is V24() V32() ext-real Element of REAL
w . A is set
(V + v) . (w . A) is V24() V32() ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL
dom p is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom V is set
p . A is V24() V32() ext-real Element of REAL
V . (w . A) is V24() V32() ext-real Element of REAL
I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL
dom I is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)
I . A is V24() V32() ext-real Element of REAL
v . (w . A) is V24() V32() ext-real Element of REAL
(p . A) + (I . A) is V24() V32() ext-real Element of REAL
p + I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL
K376(K148(),p,I) is set
(p + I) . A is V24() V32() ext-real Element of REAL
len (p + I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
r * v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
w is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(r * v) * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
v * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
r * (v * w) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
K518(r) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20(REAL,REAL))
K150() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like non empty total quasi_total V21( REAL ) V22( REAL ) V55() V56() V57() V215( REAL ) Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total quasi_total V55() V56() V57() V59() V61() Element of K19(K20(REAL,REAL))
K378(K150(),r,(id REAL)) is set
(v * w) * K518(r) is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() set
len ((r * v) * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len (v * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
(len w) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
A is V24() ordinal natural V32() ext-real non negative finite cardinal set
I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL
dom I is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)
I . A is V24() V32() ext-real Element of REAL
w . A is set
v . (w . A) is V24() V32() ext-real Element of REAL
dom v is set
p is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL
dom p is len w -element V65() V66() V67() V68() V69() V70() Element of K19(NAT)
p . A is V24() V32() ext-real Element of REAL
(r * v) . (w . A) is V24() V32() ext-real Element of REAL
r * I is Relation-like NAT -defined REAL -valued Function-like len w -element FinSequence-like V55() V56() V57() Element of (len w) -tuples_on REAL
I * K518(r) is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() set
(r * I) . A is V24() V32() ext-real Element of REAL
r * (I . A) is V24() V32() ext-real Element of REAL
len (r * I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
Lin v is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
bool the carrier of r is non empty Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
w is set
p is set
union p is set
A is set
u2 is set
the Element of p is Element of p
A is Element of K19( the carrier of r)
{ b₁ where b₁ is Element of K19( the carrier of r) : ( a₁ in b₁ & b₁ in p ) } is set
q is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A
Sum q is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
Carrier q is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not q . b₁ = 0 } is set
LI is Relation-like Function-like set
dom LI is set
rng LI is set
qI is non empty set
LI is set
LI . LI is set
LA is set
pA is Element of K19( the carrier of r)
{ b₁ where b₁ is Element of K19( the carrier of r) : ( LI in b₁ & b₁ in p ) } is set
union qI is set
the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI is Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI
rng the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI is set
the Element of qI is Element of qI
dom the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI is set
pA is set
u is set
the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI . u is set
v is set
LI . v is set
{ b₁ where b₁ is Element of K19( the carrier of r) : ( v in b₁ & b₁ in p ) } is set
x is Element of K19( the carrier of r)
pA is set
u is set
union (rng the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI) is set
pA is Element of K19( the carrier of r)
u is set
LI . u is set
{ b₁ where b₁ is Element of K19( the carrier of r) : ( u in b₁ & b₁ in p ) } is set
the Relation-like qI -defined union qI -valued Function-like quasi_total Choice_Function of qI . (LI . u) is set
v is Element of K19( the carrier of r)
q is set
LI is set
qI is Element of K19( the carrier of r)
q is Element of K19( the carrier of r)
p is set
I is Element of K19( the carrier of r)
A is linearly-independent Element of K19( the carrier of r)
Lin A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
u2 is Element of the carrier of r
q is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
Sum q is Element of the carrier of r
Carrier q is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not q . b₁ = 0 } is set
the carrier of (Lin A) is non empty set
LI is set
qI is Element of the carrier of r
Up (Lin A) is non empty Element of K19( the carrier of r)
LI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of Up (Lin A)
Sum LI is Element of the carrier of r
Lin (Up (Lin A)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
u2 is Element of the carrier of r
u2 is Element of the carrier of r
{u2} is non empty trivial finite 1 -element Element of K19( the carrier of r)
A \/ {u2} is Element of K19( the carrier of r)
q is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A \/ {u2}
Sum q is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
Carrier q is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not q . b₁ = 0 } is set
q . u2 is V24() V32() ext-real Element of REAL
- (q . u2) is V24() V32() ext-real Element of REAL
K20( the carrier of r,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set
K19(K20( the carrier of r,REAL)) is non empty non trivial non finite set
LI is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))
LI . u2 is V24() V32() ext-real Element of REAL
Funcs ( the carrier of r,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of r, REAL
LI is Element of the carrier of r
(Carrier q) \ {u2} is finite Element of K19( the carrier of r)
q . LI is V24() V32() ext-real Element of REAL
qI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)
qI . LI is V24() V32() ext-real Element of REAL
LI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier LI is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not LI . b₁ = 0 } is set
LA is set
pA is Element of the carrier of r
LI . pA is V24() V32() ext-real Element of REAL
q . pA is V24() V32() ext-real Element of REAL
pA is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))
pA . u2 is V24() V32() ext-real Element of REAL
v is Element of the carrier of r
u is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)
u . v is V24() V32() ext-real Element of REAL
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier v is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not v . b₁ = 0 } is set
x is set
u is Element of the carrier of r
v . u is V24() V32() ext-real Element of REAL
x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {u2}
Sum x is Element of the carrier of r
(- (q . u2)) * u2 is Element of the carrier of r
u is Element of the carrier of r
LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A
LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(LA - x) . u is V24() V32() ext-real Element of REAL
LA . u is V24() V32() ext-real Element of REAL
x . u is V24() V32() ext-real Element of REAL
(LA . u) - (x . u) is V24() V32() ext-real Element of REAL
q . u is V24() V32() ext-real Element of REAL
u is Element of the carrier of r
LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A
LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(LA - x) . u is V24() V32() ext-real Element of REAL
LA . u is V24() V32() ext-real Element of REAL
x . u is V24() V32() ext-real Element of REAL
(LA . u) - (x . u) is V24() V32() ext-real Element of REAL
q . u is V24() V32() ext-real Element of REAL
(q . u) - (x . u) is V24() V32() ext-real Element of REAL
(q . u) - 0 is V24() V32() ext-real Element of REAL
u is Element of the carrier of r
LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A
LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(LA - x) . u is V24() V32() ext-real Element of REAL
q . u is V24() V32() ext-real Element of REAL
LA is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of A
LA - x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * x is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
LA + (- x) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
u is Element of the carrier of r
(LA - x) . u is V24() V32() ext-real Element of REAL
q . u is V24() V32() ext-real Element of REAL
Sum LA is Element of the carrier of r
(Sum LA) - (Sum x) is Element of the carrier of r
(0. r) + (Sum x) is Element of the carrier of r
(- (q . u2)) " is V24() V32() ext-real Element of REAL
((- (q . u2)) ") * ((- (q . u2)) * u2) is Element of the carrier of r
((- (q . u2)) ") * (- (q . u2)) is V24() V32() ext-real Element of REAL
(((- (q . u2)) ") * (- (q . u2))) * u2 is Element of the carrier of r
1 * u2 is Element of the carrier of r
LI is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v is Element of the carrier of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
{ H₁(b₁) where b₁ is Element of the carrier of r : b₁ in Carrier V } is set
p is set
I is Element of the carrier of r
v + I is Element of the carrier of r
K20( the carrier of r,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set
K19(K20( the carrier of r,REAL)) is non empty non trivial non finite set
I is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))
Funcs ( the carrier of r,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of r, REAL
u2 is Element of the carrier of r
p is finite Element of K19( the carrier of r)
A is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)
A . u2 is V24() V32() ext-real Element of REAL
u2 - v is Element of the carrier of r
V . (u2 - v) is V24() V32() ext-real Element of REAL
v + (u2 - v) is Element of the carrier of r
- v is Element of the carrier of r
u2 + (- v) is Element of the carrier of r
(u2 + (- v)) + v is Element of the carrier of r
v + (- v) is Element of the carrier of r
u2 + (v + (- v)) is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
u2 + (0. r) is Element of the carrier of r
u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
q is Element of the carrier of r
u2 . q is V24() V32() ext-real Element of REAL
q - v is Element of the carrier of r
V . (q - v) is V24() V32() ext-real Element of REAL
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
I is Element of the carrier of r
w . I is V24() V32() ext-real Element of REAL
I - v is Element of the carrier of r
V . (I - v) is V24() V32() ext-real Element of REAL
p . I is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
v is Element of the carrier of r
(r,V,v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier (r,V,v) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,V,v) . b₁ = 0 } is set
v + (Carrier V) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier V } is set
w is set
p is Element of the carrier of r
(r,V,v) . p is V24() V32() ext-real Element of REAL
p - v is Element of the carrier of r
v + (p - v) is Element of the carrier of r
- v is Element of the carrier of r
p + (- v) is Element of the carrier of r
(p + (- v)) + v is Element of the carrier of r
v + (- v) is Element of the carrier of r
p + (v + (- v)) is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
p + (0. r) is Element of the carrier of r
V . (p - v) is V24() V32() ext-real Element of REAL
w is set
p is Element of the carrier of r
v + p is Element of the carrier of r
(v + p) - v is Element of the carrier of r
- v is Element of the carrier of r
(v + p) + (- v) is Element of the carrier of r
(- v) + v is Element of the carrier of r
((- v) + v) + p is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(0. r) + p is Element of the carrier of r
(r,V,v) . (v + p) is V24() V32() ext-real Element of REAL
V . p is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
V + v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
w is Element of the carrier of r
(r,(V + v),w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,v,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V,w) + (r,v,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p is Element of the carrier of r
(r,(V + v),w) . p is V24() V32() ext-real Element of REAL
p - w is Element of the carrier of r
(V + v) . (p - w) is V24() V32() ext-real Element of REAL
V . (p - w) is V24() V32() ext-real Element of REAL
v . (p - w) is V24() V32() ext-real Element of REAL
(V . (p - w)) + (v . (p - w)) is V24() V32() ext-real Element of REAL
(r,V,w) . p is V24() V32() ext-real Element of REAL
((r,V,w) . p) + (v . (p - w)) is V24() V32() ext-real Element of REAL
(r,v,w) . p is V24() V32() ext-real Element of REAL
((r,V,w) . p) + ((r,v,w) . p) is V24() V32() ext-real Element of REAL
((r,V,w) + (r,v,w)) . p is V24() V32() ext-real Element of REAL
r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
v is Element of the carrier of V
w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
r * w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,(r * w),v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,w,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
r * (V,w,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p is Element of the carrier of V
(V,(r * w),v) . p is V24() V32() ext-real Element of REAL
p - v is Element of the carrier of V
(r * w) . (p - v) is V24() V32() ext-real Element of REAL
w . (p - v) is V24() V32() ext-real Element of REAL
r * (w . (p - v)) is V24() V32() ext-real Element of REAL
(V,w,v) . p is V24() V32() ext-real Element of REAL
r * ((V,w,v) . p) is V24() V32() ext-real Element of REAL
(r * (V,w,v)) . p is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v is Element of the carrier of r
w is Element of the carrier of r
(r,V,w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(r,V,w),v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v + w is Element of the carrier of r
(r,V,(v + w)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p is Element of the carrier of r
(r,(r,V,w),v) . p is V24() V32() ext-real Element of REAL
p - v is Element of the carrier of r
(r,V,w) . (p - v) is V24() V32() ext-real Element of REAL
(p - v) - w is Element of the carrier of r
V . ((p - v) - w) is V24() V32() ext-real Element of REAL
p - (v + w) is Element of the carrier of r
V . (p - (v + w)) is V24() V32() ext-real Element of REAL
(r,V,(v + w)) . p is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
V is Element of the carrier of r
(r,(ZeroLC r),V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier (ZeroLC r) is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not (ZeroLC r) . b₁ = 0 } is set
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)
V + (Carrier (ZeroLC r)) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier (ZeroLC r) } is set
Carrier (r,(ZeroLC r),V) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,(ZeroLC r),V) . b₁ = 0 } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V,(0. r)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v is Element of the carrier of r
(r,V,(0. r)) . v is V24() V32() ext-real Element of REAL
v - (0. r) is Element of the carrier of r
V . (v - (0. r)) is V24() V32() ext-real Element of REAL
V . v is V24() V32() ext-real Element of REAL
r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of r is non empty set
v is V24() V32() ext-real Element of REAL
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v " is V24() V32() ext-real Element of REAL
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
K20( the carrier of r,REAL) is Relation-like non empty non trivial non finite V55() V56() V57() set
K19(K20( the carrier of r,REAL)) is non empty non trivial non finite set
w is Relation-like the carrier of r -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20( the carrier of r,REAL))
Funcs ( the carrier of r,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of r, REAL
I is Element of the carrier of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
v * (Carrier V) is Element of K19( the carrier of r)
{ (v * b₁) where b₁ is Element of the carrier of r : b₁ in Carrier V } is set
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Element of Funcs ( the carrier of r,REAL)
p . I is V24() V32() ext-real Element of REAL
(v ") * I is Element of the carrier of r
V . ((v ") * I) is V24() V32() ext-real Element of REAL
v * ((v ") * I) is Element of the carrier of r
v * (v ") is V24() V32() ext-real Element of REAL
(v * (v ")) * I is Element of the carrier of r
1 * I is Element of the carrier of r
{ H₂(b₁) where b₁ is Element of the carrier of r : b₁ in Carrier V } is set
I is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
A is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
u2 is Element of the carrier of r
A . u2 is V24() V32() ext-real Element of REAL
(v ") * u2 is Element of the carrier of r
V . ((v ") * u2) is V24() V32() ext-real Element of REAL
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
I is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
I is Element of the carrier of r
w . I is V24() V32() ext-real Element of REAL
(v ") * I is Element of the carrier of r
V . ((v ") * I) is V24() V32() ext-real Element of REAL
p . I is V24() V32() ext-real Element of REAL
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
I is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
A is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
r is V24() V32() ext-real Element of REAL
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Carrier (V,v,r) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not (V,v,r) . b₁ = 0 } is set
Carrier v is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0 } is set
r * (Carrier v) is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in Carrier v } is set
w is set
p is Element of the carrier of V
(V,v,r) . p is V24() V32() ext-real Element of REAL
(V,v,0) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
r " is V24() V32() ext-real Element of REAL
(r ") * p is Element of the carrier of V
v . ((r ") * p) is V24() V32() ext-real Element of REAL
r * ((r ") * p) is Element of the carrier of V
r * (r ") is V24() V32() ext-real Element of REAL
(r * (r ")) * p is Element of the carrier of V
1 * p is Element of the carrier of V
r is V24() V32() ext-real Element of REAL
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Carrier (V,v,r) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not (V,v,r) . b₁ = 0 } is set
Carrier v is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0 } is set
r * (Carrier v) is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in Carrier v } is set
w is set
p is Element of the carrier of V
r * p is Element of the carrier of V
r " is V24() V32() ext-real Element of REAL
(r ") * (r * p) is Element of the carrier of V
(r ") * r is V24() V32() ext-real Element of REAL
((r ") * r) * p is Element of the carrier of V
1 * p is Element of the carrier of V
v . p is V24() V32() ext-real Element of REAL
(V,v,r) . w is V24() V32() ext-real Element of REAL
r is V24() V32() ext-real Element of REAL
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
v + w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,(v + w),r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,v,r) + (V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(ZeroLC V) + (ZeroLC V) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
I is Element of the carrier of V
((ZeroLC V) + (ZeroLC V)) . I is V24() V32() ext-real Element of REAL
(ZeroLC V) . I is V24() V32() ext-real Element of REAL
((ZeroLC V) . I) + ((ZeroLC V) . I) is V24() V32() ext-real Element of REAL
((ZeroLC V) . I) + 0 is V24() V32() ext-real Element of REAL
(V,v,r) + (ZeroLC V) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p is Element of the carrier of V
(V,(v + w),r) . p is V24() V32() ext-real Element of REAL
r " is V24() V32() ext-real Element of REAL
(r ") * p is Element of the carrier of V
(v + w) . ((r ") * p) is V24() V32() ext-real Element of REAL
v . ((r ") * p) is V24() V32() ext-real Element of REAL
w . ((r ") * p) is V24() V32() ext-real Element of REAL
(v . ((r ") * p)) + (w . ((r ") * p)) is V24() V32() ext-real Element of REAL
(V,v,r) . p is V24() V32() ext-real Element of REAL
((V,v,r) . p) + (w . ((r ") * p)) is V24() V32() ext-real Element of REAL
(V,w,r) . p is V24() V32() ext-real Element of REAL
((V,v,r) . p) + ((V,w,r) . p) is V24() V32() ext-real Element of REAL
((V,v,r) + (V,w,r)) . p is V24() V32() ext-real Element of REAL
r is V24() V32() ext-real Element of REAL
V is V24() V32() ext-real Element of REAL
v is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of v is non empty set
w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(v,w,V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
r * (v,w,V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
r * w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(v,(r * w),V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
ZeroLC v is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
r * (ZeroLC v) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
0 * w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
r * (0 * w) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
r * 0 is V24() V32() ext-real Element of REAL
(r * 0) * w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
p is Element of the carrier of v
(r * (v,w,V)) . p is V24() V32() ext-real Element of REAL
(v,w,V) . p is V24() V32() ext-real Element of REAL
r * ((v,w,V) . p) is V24() V32() ext-real Element of REAL
V " is V24() V32() ext-real Element of REAL
(V ") * p is Element of the carrier of v
w . ((V ") * p) is V24() V32() ext-real Element of REAL
r * (w . ((V ") * p)) is V24() V32() ext-real Element of REAL
(r * w) . ((V ") * p) is V24() V32() ext-real Element of REAL
(v,(r * w),V) . p is V24() V32() ext-real Element of REAL
r is V24() V32() ext-real Element of REAL
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
the carrier of V is non empty set
(V,(ZeroLC V),r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
v is Element of the carrier of V
(V,(ZeroLC V),r) . v is V24() V32() ext-real Element of REAL
r " is V24() V32() ext-real Element of REAL
(r ") * v is Element of the carrier of V
(ZeroLC V) . ((r ") * v) is V24() V32() ext-real Element of REAL
(ZeroLC V) . v is V24() V32() ext-real Element of REAL
r is V24() V32() ext-real Element of REAL
V is V24() V32() ext-real Element of REAL
r * V is V24() V32() ext-real Element of REAL
v is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of v is non empty set
w is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(v,w,V) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(v,(v,w,V),r) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(v,w,(r * V)) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
ZeroLC v is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
p is Element of the carrier of v
(v,(v,w,V),r) . p is V24() V32() ext-real Element of REAL
r " is V24() V32() ext-real Element of REAL
(r ") * p is Element of the carrier of v
(v,w,V) . ((r ") * p) is V24() V32() ext-real Element of REAL
V " is V24() V32() ext-real Element of REAL
(V ") * ((r ") * p) is Element of the carrier of v
w . ((V ") * ((r ") * p)) is V24() V32() ext-real Element of REAL
(V ") * (r ") is V24() V32() ext-real Element of REAL
((V ") * (r ")) * p is Element of the carrier of v
w . (((V ") * (r ")) * p) is V24() V32() ext-real Element of REAL
(r * V) " is V24() V32() ext-real Element of REAL
((r * V) ") * p is Element of the carrier of v
w . (((r * V) ") * p) is V24() V32() ext-real Element of REAL
(v,w,(r * V)) . p is V24() V32() ext-real Element of REAL
r is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V,1) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v is Element of the carrier of r
(r,V,1) . v is V24() V32() ext-real Element of REAL
1 " is non empty V24() V32() ext-real positive non negative Element of REAL
(1 ") * v is Element of the carrier of r
V . ((1 ") * v) is V24() V32() ext-real Element of REAL
V . v is V24() V32() ext-real Element of REAL
r is non empty addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
v is Relation-like Function-like FinSequence-like set
rng v is set
w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
V * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * w) is V24() V32() ext-real Element of REAL
K406(REAL,(V * w),K148()) is V24() V32() ext-real Element of REAL
v is V24() V32() ext-real Element of REAL
w is V24() V32() ext-real Element of REAL
p is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng p is set
V * p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * p) is V24() V32() ext-real Element of REAL
K406(REAL,(V * p),K148()) is V24() V32() ext-real Element of REAL
p " is Relation-like Function-like set
dom (p ") is set
len p is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
card (Carrier V) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
I is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng I is set
V * I is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * I) is V24() V32() ext-real Element of REAL
K406(REAL,(V * I),K148()) is V24() V32() ext-real Element of REAL
I * (p ") is Relation-like NAT -defined Function-like set
dom I is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
len I is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
Seg (len I) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
{ b₁ where b₁ is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT : ( 1 <= b₁ & b₁ <= len I ) } is set
dom (I * (p ")) is set
Seg (len p) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
{ b₁ where b₁ is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
dom p is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
rng (p ") is set
rng (I * (p ")) is set
K20((Seg (len p)),(Seg (len p))) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
K19(K20((Seg (len p)),(Seg (len p)))) is non empty set
u2 is Relation-like Seg (len p) -defined Seg (len p) -valued Function-like total quasi_total V55() V56() V57() V58() Element of K19(K20((Seg (len p)),(Seg (len p))))
len (V * p) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
dom (V * p) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
K20((dom (V * p)),(dom (V * p))) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
K19(K20((dom (V * p)),(dom (V * p)))) is non empty set
q is Relation-like dom (V * p) -defined dom (V * p) -valued Function-like one-to-one total quasi_total onto bijective V55() V56() V57() V58() Element of K19(K20((dom (V * p)),(dom (V * p))))
(V * p) * q is Relation-like dom (V * p) -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20((dom (V * p)),REAL))
K20((dom (V * p)),REAL) is Relation-like V55() V56() V57() set
K19(K20((dom (V * p)),REAL)) is non empty set
p * q is Relation-like dom (V * p) -defined the carrier of r -valued Function-like Element of K19(K20((dom (V * p)), the carrier of r))
K20((dom (V * p)), the carrier of r) is Relation-like set
K19(K20((dom (V * p)), the carrier of r)) is non empty set
V * (p * q) is Relation-like dom (V * p) -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20((dom (V * p)),REAL))
(p ") * p is Relation-like the carrier of r -valued Function-like set
I * ((p ") * p) is Relation-like NAT -defined the carrier of r -valued Function-like set
(I * ((p ") * p)) * V is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() set
id (Carrier V) is Relation-like Carrier V -defined Carrier V -valued Function-like one-to-one total quasi_total finite Element of K19(K20((Carrier V),(Carrier V)))
K20((Carrier V),(Carrier V)) is Relation-like finite set
K19(K20((Carrier V),(Carrier V))) is non empty finite V44() set
(id (Carrier V)) * I is Relation-like NAT -defined Carrier V -valued Function-like Element of K19(K20(NAT,(Carrier V)))
K20(NAT,(Carrier V)) is Relation-like set
K19(K20(NAT,(Carrier V))) is non empty set
V * ((id (Carrier V)) * I) is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20(NAT,REAL))
r is non empty addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
v is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng v is set
V * v is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * v) is V24() V32() ext-real Element of REAL
K406(REAL,(V * v),K148()) is V24() V32() ext-real Element of REAL
len (V * v) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
(len (V * v)) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like len (V * v) -element FinSequence-like V55() V56() V57() Element of (len (V * v)) -tuples_on REAL
(len (V * v)) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
I is V24() ordinal natural V32() ext-real non negative finite cardinal set
dom (V * v) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom v is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
v . I is set
dom V is set
(V * v) . I is V24() V32() ext-real Element of REAL
V . (v . I) is V24() V32() ext-real Element of REAL
((len (V * v)) |-> 0) . I is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of REAL
len ((len (V * v)) |-> 0) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
r is non empty addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
(r,V) is V24() V32() ext-real Element of REAL
v is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng v is set
V * v is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * v) is V24() V32() ext-real Element of REAL
K406(REAL,(V * v),K148()) is V24() V32() ext-real Element of REAL
w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng w is set
V * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * w) is V24() V32() ext-real Element of REAL
K406(REAL,(V * w),K148()) is V24() V32() ext-real Element of REAL
K19((rng v)) is non empty set
p is Element of K19((rng v))
v - p is Relation-like Function-like FinSequence-like set
p ` is Element of K19((rng v))
(rng v) \ p is set
v - (p `) is Relation-like Function-like FinSequence-like set
dom v is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
K20((dom v),(dom v)) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
K19(K20((dom v),(dom v))) is non empty set
(v - (p `)) ^ (v - p) is Relation-like Function-like FinSequence-like set
u2 is Relation-like dom v -defined dom v -valued Function-like one-to-one total quasi_total onto bijective V55() V56() V57() V58() Element of K19(K20((dom v),(dom v)))
v * u2 is Relation-like dom v -defined the carrier of r -valued Function-like Element of K19(K20((dom v), the carrier of r))
K20((dom v), the carrier of r) is Relation-like set
K19(K20((dom v), the carrier of r)) is non empty set
(rng v) \ (p `) is Element of K19((rng v))
(p `) ` is Element of K19((rng v))
(rng v) \ (p `) is set
A is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng A is set
dom w is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
K20((dom w),(dom w)) is Relation-like RAT -valued INT -valued V55() V56() V57() V58() set
K19(K20((dom w),(dom w))) is non empty set
q is Relation-like dom w -defined dom w -valued Function-like one-to-one total quasi_total onto bijective V55() V56() V57() V58() Element of K19(K20((dom w),(dom w)))
w * q is Relation-like dom w -defined the carrier of r -valued Function-like Element of K19(K20((dom w), the carrier of r))
K20((dom w), the carrier of r) is Relation-like set
K19(K20((dom w), the carrier of r)) is non empty set
len (V * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
dom (V * w) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(V * w) * q is Relation-like dom w -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20((dom w),REAL))
K20((dom w),REAL) is Relation-like V55() V56() V57() set
K19(K20((dom w),REAL)) is non empty set
V * A is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * A) is V24() V32() ext-real Element of REAL
K406(REAL,(V * A),K148()) is V24() V32() ext-real Element of REAL
len (V * v) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len v is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
dom (V * v) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(rng v) \ p is Element of K19((rng v))
I is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng I is set
A ^ I is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
V * (A ^ I) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
V * I is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
(V * A) ^ (V * I) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * I) is V24() V32() ext-real Element of REAL
K406(REAL,(V * I),K148()) is V24() V32() ext-real Element of REAL
(V * v) * u2 is Relation-like dom v -defined REAL -valued Function-like V55() V56() V57() Element of K19(K20((dom v),REAL))
K20((dom v),REAL) is Relation-like V55() V56() V57() set
K19(K20((dom v),REAL)) is non empty set
Sum (V * (A ^ I)) is V24() V32() ext-real Element of REAL
K406(REAL,(V * (A ^ I)),K148()) is V24() V32() ext-real Element of REAL
(r,V) + 0 is V24() V32() ext-real Element of REAL
r is non empty addLoopStr
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
the carrier of r is non empty set
(r,(ZeroLC r)) is V24() V32() ext-real Element of REAL
Carrier (ZeroLC r) is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not (ZeroLC r) . b₁ = 0 } is set
V is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng V is set
(ZeroLC r) * V is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum ((ZeroLC r) * V) is V24() V32() ext-real Element of REAL
K406(REAL,((ZeroLC r) * V),K148()) is V24() V32() ext-real Element of REAL
r is non empty addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
(r,V) is V24() V32() ext-real Element of REAL
v is Element of the carrier of r
{v} is non empty trivial finite 1 -element Element of K19( the carrier of r)
V . v is V24() V32() ext-real Element of REAL
w is Relation-like Function-like FinSequence-like set
rng w is set
dom V is set
p is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
<*v*> is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
[1,v] is set
{1,v} is finite set
{1} is non empty trivial finite V44() 1 -element V65() V66() V67() V68() V69() V70() set
{{1,v},{1}} is finite V44() set
{[1,v]} is Relation-like Function-like constant non empty trivial finite 1 -element set
V * p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
<*(V . v)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
[1,(V . v)] is set
{1,(V . v)} is finite V65() V66() V67() set
{{1,(V . v)},{1}} is finite V44() set
{[1,(V . v)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
Sum (V * p) is V24() V32() ext-real Element of REAL
K406(REAL,(V * p),K148()) is V24() V32() ext-real Element of REAL
r is non empty addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
(r,V) is V24() V32() ext-real Element of REAL
v is Element of the carrier of r
w is Element of the carrier of r
{v,w} is finite Element of K19( the carrier of r)
V . v is V24() V32() ext-real Element of REAL
V . w is V24() V32() ext-real Element of REAL
(V . v) + (V . w) is V24() V32() ext-real Element of REAL
p is Relation-like Function-like FinSequence-like set
rng p is set
dom V is set
<*(V . v)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
[1,(V . v)] is set
{1,(V . v)} is finite V65() V66() V67() set
{1} is non empty trivial finite V44() 1 -element V65() V66() V67() V68() V69() V70() set
{{1,(V . v)},{1}} is finite V44() set
{[1,(V . v)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
Sum <*(V . v)*> is V24() V32() ext-real Element of REAL
K406(REAL,<*(V . v)*>,K148()) is V24() V32() ext-real Element of REAL
I is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
<*v,w*> is set
<*v*> is Relation-like Function-like set
[1,v] is set
{1,v} is finite set
{{1,v},{1}} is finite V44() set
{[1,v]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*w*> is Relation-like Function-like set
[1,w] is set
{1,w} is finite set
{{1,w},{1}} is finite V44() set
{[1,w]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*v*> ^ <*w*> is Relation-like Function-like FinSequence-like set
<*w,v*> is set
<*w*> ^ <*v*> is Relation-like Function-like FinSequence-like set
V * I is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
<*(V . v),(V . w)*> is set
<*(V . v)*> is Relation-like Function-like set
<*(V . w)*> is Relation-like Function-like set
[1,(V . w)] is set
{1,(V . w)} is finite V65() V66() V67() set
{{1,(V . w)},{1}} is finite V44() set
{[1,(V . w)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*(V . v)*> ^ <*(V . w)*> is Relation-like Function-like FinSequence-like set
<*(V . w),(V . v)*> is set
<*(V . w)*> ^ <*(V . v)*> is Relation-like Function-like FinSequence-like set
Sum (V * I) is V24() V32() ext-real Element of REAL
K406(REAL,(V * I),K148()) is V24() V32() ext-real Element of REAL
(V . w) + (V . v) is V24() V32() ext-real Element of REAL
r is non empty addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V) is V24() V32() ext-real Element of REAL
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
V + v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(V + v)) is V24() V32() ext-real Element of REAL
(r,v) is V24() V32() ext-real Element of REAL
(r,V) + (r,v) is V24() V32() ext-real Element of REAL
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
Carrier v is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not v . b₁ = 0 } is set
(Carrier V) \ (Carrier v) is finite Element of K19( the carrier of r)
I is Relation-like Function-like FinSequence-like set
rng I is set
(Carrier V) /\ (Carrier v) is finite Element of K19( the carrier of r)
A is Relation-like Function-like FinSequence-like set
rng A is set
(Carrier v) \ (Carrier V) is finite Element of K19( the carrier of r)
u2 is Relation-like Function-like FinSequence-like set
rng u2 is set
q is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
LI is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
q ^ LI is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng (q ^ LI) is set
((Carrier V) \ (Carrier v)) \/ ((Carrier V) /\ (Carrier v)) is finite Element of K19( the carrier of r)
qI is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
(q ^ LI) ^ qI is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng ((q ^ LI) ^ qI) is set
(Carrier V) \/ ((Carrier v) \ (Carrier V)) is finite Element of K19( the carrier of r)
(Carrier V) \/ (Carrier v) is finite Element of K19( the carrier of r)
LI ^ qI is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng (LI ^ qI) is set
((Carrier V) /\ (Carrier v)) \/ ((Carrier v) \ (Carrier V)) is finite Element of K19( the carrier of r)
q ^ (LI ^ qI) is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
v * ((q ^ LI) ^ qI) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
v * q is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
v * (LI ^ qI) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
(v * q) ^ (v * (LI ^ qI)) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (v * q) is V24() V32() ext-real Element of REAL
K406(REAL,(v * q),K148()) is V24() V32() ext-real Element of REAL
Sum (v * ((q ^ LI) ^ qI)) is V24() V32() ext-real Element of REAL
K406(REAL,(v * ((q ^ LI) ^ qI)),K148()) is V24() V32() ext-real Element of REAL
Sum (v * (LI ^ qI)) is V24() V32() ext-real Element of REAL
K406(REAL,(v * (LI ^ qI)),K148()) is V24() V32() ext-real Element of REAL
0 + (Sum (v * (LI ^ qI))) is V24() V32() ext-real Element of REAL
V * ((q ^ LI) ^ qI) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len (V * ((q ^ LI) ^ qI)) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len ((q ^ LI) ^ qI) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len (v * ((q ^ LI) ^ qI)) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
(len ((q ^ LI) ^ qI)) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
(V + v) * ((q ^ LI) ^ qI) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
u is Relation-like NAT -defined REAL -valued Function-like len ((q ^ LI) ^ qI) -element FinSequence-like V55() V56() V57() Element of (len ((q ^ LI) ^ qI)) -tuples_on REAL
v is Relation-like NAT -defined REAL -valued Function-like len ((q ^ LI) ^ qI) -element FinSequence-like V55() V56() V57() Element of (len ((q ^ LI) ^ qI)) -tuples_on REAL
u + v is Relation-like NAT -defined REAL -valued Function-like len ((q ^ LI) ^ qI) -element FinSequence-like V55() V56() V57() Element of (len ((q ^ LI) ^ qI)) -tuples_on REAL
K376(K148(),u,v) is set
V * (q ^ LI) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
V * qI is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
(V * (q ^ LI)) ^ (V * qI) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * qI) is V24() V32() ext-real Element of REAL
K406(REAL,(V * qI),K148()) is V24() V32() ext-real Element of REAL
Sum (V * ((q ^ LI) ^ qI)) is V24() V32() ext-real Element of REAL
K406(REAL,(V * ((q ^ LI) ^ qI)),K148()) is V24() V32() ext-real Element of REAL
Sum (V * (q ^ LI)) is V24() V32() ext-real Element of REAL
K406(REAL,(V * (q ^ LI)),K148()) is V24() V32() ext-real Element of REAL
(Sum (V * (q ^ LI))) + 0 is V24() V32() ext-real Element of REAL
Carrier (V + v) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (V + v) . b₁ = 0 } is set
x is set
u is Element of the carrier of r
(V + v) . u is V24() V32() ext-real Element of REAL
V . u is V24() V32() ext-real Element of REAL
v . u is V24() V32() ext-real Element of REAL
(V . u) + (v . u) is V24() V32() ext-real Element of REAL
Sum (u + v) is V24() V32() ext-real Element of REAL
K406(REAL,(u + v),K148()) is V24() V32() ext-real Element of REAL
r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
r * v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,(r * v)) is V24() V32() ext-real Element of REAL
(V,v) is V24() V32() ext-real Element of REAL
r * (V,v) is V24() V32() ext-real Element of REAL
Carrier v is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0 } is set
w is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng w is set
v * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (v * w) is V24() V32() ext-real Element of REAL
K406(REAL,(v * w),K148()) is V24() V32() ext-real Element of REAL
Carrier (r * v) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (r * v) . b₁ = 0 } is set
r * (v * w) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
K518(r) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total V55() V56() V57() Element of K19(K20(REAL,REAL))
K150() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like non empty total quasi_total V21( REAL ) V22( REAL ) V55() V56() V57() V215( REAL ) Element of K19(K20(K20(REAL,REAL),REAL))
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total quasi_total V55() V56() V57() V59() V61() Element of K19(K20(REAL,REAL))
K378(K150(),r,(id REAL)) is set
(v * w) * K518(r) is Relation-like NAT -defined REAL -valued Function-like V55() V56() V57() set
Sum (r * (v * w)) is V24() V32() ext-real Element of REAL
K406(REAL,(r * (v * w)),K148()) is V24() V32() ext-real Element of REAL
(r * v) * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum ((r * v) * w) is V24() V32() ext-real Element of REAL
K406(REAL,((r * v) * w),K148()) is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V) is V24() V32() ext-real Element of REAL
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
V - v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
V + (- v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(V - v)) is V24() V32() ext-real Element of REAL
(r,v) is V24() V32() ext-real Element of REAL
(r,V) - (r,v) is V24() V32() ext-real Element of REAL
(r,((- 1) * v)) is V24() V32() ext-real Element of REAL
(r,V) + (r,((- 1) * v)) is V24() V32() ext-real Element of REAL
(- 1) * (r,v) is V24() V32() ext-real Element of REAL
(r,V) + ((- 1) * (r,v)) is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed V135() addLoopStr
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V) is V24() V32() ext-real Element of REAL
v is Element of the carrier of r
(r,V,v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(r,V,v)) is V24() V32() ext-real Element of REAL
K20( the carrier of r, the carrier of r) is Relation-like non empty set
K19(K20( the carrier of r, the carrier of r)) is non empty set
p is Relation-like the carrier of r -defined the carrier of r -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of r, the carrier of r))
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
I is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng I is set
V * I is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * I) is V24() V32() ext-real Element of REAL
K406(REAL,(V * I),K148()) is V24() V32() ext-real Element of REAL
p * I is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
len (p * I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len I is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len (V * I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
(r,V,v) * (p * I) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len ((r,V,v) * (p * I)) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
A is V24() ordinal natural V32() ext-real non negative finite cardinal set
dom I is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
I /. A is Element of the carrier of r
I . A is set
dom (V * I) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(V * I) . A is V24() V32() ext-real Element of REAL
V . (I . A) is V24() V32() ext-real Element of REAL
dom ((r,V,v) * (p * I)) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
((r,V,v) * (p * I)) . A is V24() V32() ext-real Element of REAL
(p * I) . A is set
(r,V,v) . ((p * I) . A) is V24() V32() ext-real Element of REAL
dom (p * I) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
p . (I . A) is set
(I /. A) + v is Element of the carrier of r
((I /. A) + v) - v is Element of the carrier of r
V . (((I /. A) + v) - v) is V24() V32() ext-real Element of REAL
- v is Element of the carrier of r
((I /. A) + v) + (- v) is Element of the carrier of r
V . (((I /. A) + v) + (- v)) is V24() V32() ext-real Element of REAL
v + (- v) is Element of the carrier of r
(I /. A) + (v + (- v)) is Element of the carrier of r
V . ((I /. A) + (v + (- v))) is V24() V32() ext-real Element of REAL
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(I /. A) + (0. r) is Element of the carrier of r
V . ((I /. A) + (0. r)) is V24() V32() ext-real Element of REAL
A is set
u2 is set
(p * I) . A is set
(p * I) . u2 is set
I /. A is Element of the carrier of r
p . (I /. A) is Element of the carrier of r
(I /. A) + v is Element of the carrier of r
I . A is set
I . u2 is set
I /. u2 is Element of the carrier of r
p . (I . A) is set
p . (I . u2) is set
(I /. u2) + v is Element of the carrier of r
Carrier (r,V,v) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,V,v) . b₁ = 0 } is set
rng (p * I) is set
A is set
v + (Carrier V) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier V } is set
u2 is Element of the carrier of r
v + u2 is Element of the carrier of r
q is set
I . q is set
p . (I . q) is set
dom p is non empty set
(p * I) . q is set
Sum ((r,V,v) * (p * I)) is V24() V32() ext-real Element of REAL
K406(REAL,((r,V,v) * (p * I)),K148()) is V24() V32() ext-real Element of REAL
r is V24() V32() ext-real Element of REAL
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,v) is V24() V32() ext-real Element of REAL
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,(V,v,r)) is V24() V32() ext-real Element of REAL
K20( the carrier of V, the carrier of V) is Relation-like non empty set
K19(K20( the carrier of V, the carrier of V)) is non empty set
p is Relation-like the carrier of V -defined the carrier of V -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of V, the carrier of V))
Carrier v is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0 } is set
I is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng I is set
v * I is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (v * I) is V24() V32() ext-real Element of REAL
K406(REAL,(v * I),K148()) is V24() V32() ext-real Element of REAL
A is set
p * I is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
dom (p * I) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
u2 is set
(p * I) . A is set
(p * I) . u2 is set
I /. A is Element of the carrier of V
p . (I /. A) is Element of the carrier of V
r * (I /. A) is Element of the carrier of V
dom I is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
I . A is set
I . u2 is set
I /. u2 is Element of the carrier of V
p . (I . A) is set
p . (I . u2) is set
r * (I /. u2) is Element of the carrier of V
1 * (I /. A) is Element of the carrier of V
r " is V24() V32() ext-real Element of REAL
(r ") * r is V24() V32() ext-real Element of REAL
((r ") * r) * (I /. A) is Element of the carrier of V
(r ") * (r * (I /. u2)) is Element of the carrier of V
((r ") * r) * (I /. u2) is Element of the carrier of V
1 * (I /. u2) is Element of the carrier of V
len (v * I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len I is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len (p * I) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
(V,v,r) * (p * I) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len ((V,v,r) * (p * I)) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
A is V24() ordinal natural V32() ext-real non negative finite cardinal set
I /. A is Element of the carrier of V
I . A is set
dom (v * I) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(v * I) . A is V24() V32() ext-real Element of REAL
v . (I . A) is V24() V32() ext-real Element of REAL
(p * I) . A is set
p . (I . A) is set
dom ((V,v,r) * (p * I)) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
((V,v,r) * (p * I)) . A is V24() V32() ext-real Element of REAL
(V,v,r) . ((p * I) . A) is V24() V32() ext-real Element of REAL
r * (I /. A) is Element of the carrier of V
(V,v,r) . (r * (I /. A)) is V24() V32() ext-real Element of REAL
(r ") * (r * (I /. A)) is Element of the carrier of V
v . ((r ") * (r * (I /. A))) is V24() V32() ext-real Element of REAL
((r ") * r) * (I /. A) is Element of the carrier of V
v . (((r ") * r) * (I /. A)) is V24() V32() ext-real Element of REAL
1 * (I /. A) is Element of the carrier of V
v . (1 * (I /. A)) is V24() V32() ext-real Element of REAL
Carrier (V,v,r) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (V,v,r) . b₁ = 0 } is set
rng (p * I) is set
A is set
r * (Carrier v) is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in Carrier v } is set
u2 is Element of the carrier of V
r * u2 is Element of the carrier of V
q is set
I . q is set
p . u2 is Element of the carrier of V
(p * I) . q is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
V is Element of the carrier of r
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,v,V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,v,V) is Element of the carrier of r
(r,v) is V24() V32() ext-real Element of REAL
(r,v) * V is Element of the carrier of r
Sum v is Element of the carrier of r
((r,v) * V) + (Sum v) is Element of the carrier of r
w is V24() ordinal natural V32() ext-real non negative finite cardinal set
w + 1 is non empty V24() ordinal natural V32() ext-real positive non negative finite cardinal Element of REAL
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier p is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not p . b₁ = 0 } is set
card (Carrier p) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(r,p,V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,p,V) is Element of the carrier of r
(r,p) is V24() V32() ext-real Element of REAL
(r,p) * V is Element of the carrier of r
Sum p is Element of the carrier of r
((r,p) * V) + (Sum p) is Element of the carrier of r
I is set
A is Element of the carrier of r
{A} is non empty trivial finite 1 -element Element of K19( the carrier of r)
(Carrier p) \ {A} is finite Element of K19( the carrier of r)
card ((Carrier p) \ {A}) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
p . A is V24() V32() ext-real Element of REAL
u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {A}
u2 . A is V24() V32() ext-real Element of REAL
p - u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p + (- u2) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(p - u2) . A is V24() V32() ext-real Element of REAL
(p . A) - (u2 . A) is V24() V32() ext-real Element of REAL
Carrier (p - u2) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (p - u2) . b₁ = 0 } is set
Carrier u2 is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not u2 . b₁ = 0 } is set
(Carrier p) \/ (Carrier u2) is finite Element of K19( the carrier of r)
(Carrier p) \/ {A} is finite Element of K19( the carrier of r)
card (Carrier (p - u2)) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(r,(p - u2),V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,(p - u2),V) is Element of the carrier of r
(r,(p - u2)) is V24() V32() ext-real Element of REAL
(r,(p - u2)) * V is Element of the carrier of r
Sum (p - u2) is Element of the carrier of r
((r,(p - u2)) * V) + (Sum (p - u2)) is Element of the carrier of r
(p - u2) + u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
u2 - u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
u2 + (- u2) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p + (u2 - u2) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p + (ZeroLC r) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum u2 is Element of the carrier of r
(Sum (p - u2)) + (Sum u2) is Element of the carrier of r
(u2 . A) * A is Element of the carrier of r
(Sum (p - u2)) + ((u2 . A) * A) is Element of the carrier of r
V + (Carrier u2) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier u2 } is set
V + {A} is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in {A} } is set
V + A is Element of the carrier of r
{(V + A)} is non empty trivial finite 1 -element Element of K19( the carrier of r)
(r,u2,V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier (r,u2,V) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,u2,V) . b₁ = 0 } is set
Sum (r,u2,V) is Element of the carrier of r
(r,u2,V) . (V + A) is V24() V32() ext-real Element of REAL
((r,u2,V) . (V + A)) * (V + A) is Element of the carrier of r
(V + A) - V is Element of the carrier of r
u2 . ((V + A) - V) is V24() V32() ext-real Element of REAL
(u2 . ((V + A) - V)) * (V + A) is Element of the carrier of r
(u2 . A) * (V + A) is Element of the carrier of r
(r,u2) is V24() V32() ext-real Element of REAL
(r,(p - u2)) + (r,u2) is V24() V32() ext-real Element of REAL
(r,(p - u2)) + (u2 . A) is V24() V32() ext-real Element of REAL
(r,(p - u2),V) + (r,u2,V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(Sum (r,(p - u2),V)) + (Sum (r,u2,V)) is Element of the carrier of r
(u2 . A) * V is Element of the carrier of r
((u2 . A) * V) + ((u2 . A) * A) is Element of the carrier of r
(((r,(p - u2)) * V) + (Sum (p - u2))) + (((u2 . A) * V) + ((u2 . A) * A)) is Element of the carrier of r
(((r,(p - u2)) * V) + (Sum (p - u2))) + ((u2 . A) * V) is Element of the carrier of r
((((r,(p - u2)) * V) + (Sum (p - u2))) + ((u2 . A) * V)) + ((u2 . A) * A) is Element of the carrier of r
((r,(p - u2)) * V) + ((u2 . A) * V) is Element of the carrier of r
(((r,(p - u2)) * V) + ((u2 . A) * V)) + (Sum (p - u2)) is Element of the carrier of r
((((r,(p - u2)) * V) + ((u2 . A) * V)) + (Sum (p - u2))) + ((u2 . A) * A) is Element of the carrier of r
((r,p) * V) + (Sum (p - u2)) is Element of the carrier of r
(((r,p) * V) + (Sum (p - u2))) + ((u2 . A) * A) is Element of the carrier of r
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier w is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not w . b₁ = 0 } is set
card (Carrier w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(r,w,V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,w,V) is Element of the carrier of r
(r,w) is V24() V32() ext-real Element of REAL
(r,w) * V is Element of the carrier of r
Sum w is Element of the carrier of r
((r,w) * V) + (Sum w) is Element of the carrier of r
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
V + (Carrier w) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier w } is set
Carrier (r,w,V) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,w,V) . b₁ = 0 } is set
(0. r) + (0. r) is Element of the carrier of r
Carrier v is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not v . b₁ = 0 } is set
card (Carrier v) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier w is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not w . b₁ = 0 } is set
card (Carrier w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(r,w,V) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,w,V) is Element of the carrier of r
(r,w) is V24() V32() ext-real Element of REAL
(r,w) * V is Element of the carrier of r
Sum w is Element of the carrier of r
((r,w) * V) + (Sum w) is Element of the carrier of r
r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum (V,v,r) is Element of the carrier of V
Sum v is Element of the carrier of V
r * (Sum v) is Element of the carrier of V
w is V24() ordinal natural V32() ext-real non negative finite cardinal set
w + 1 is non empty V24() ordinal natural V32() ext-real positive non negative finite cardinal Element of REAL
p is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Carrier p is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not p . b₁ = 0 } is set
card (Carrier p) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(V,p,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum (V,p,r) is Element of the carrier of V
Sum p is Element of the carrier of V
r * (Sum p) is Element of the carrier of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
0. V is V84(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
I is set
A is Element of the carrier of V
{A} is non empty trivial finite 1 -element Element of K19( the carrier of V)
(Carrier p) \ {A} is finite Element of K19( the carrier of V)
card ((Carrier p) \ {A}) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
p . A is V24() V32() ext-real Element of REAL
u2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {A}
u2 . A is V24() V32() ext-real Element of REAL
p - u2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
- u2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(- 1) * u2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p + (- u2) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(p - u2) . A is V24() V32() ext-real Element of REAL
(p . A) - (u2 . A) is V24() V32() ext-real Element of REAL
Carrier (p - u2) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (p - u2) . b₁ = 0 } is set
Carrier u2 is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not u2 . b₁ = 0 } is set
(Carrier p) \/ (Carrier u2) is finite Element of K19( the carrier of V)
(Carrier p) \/ {A} is finite Element of K19( the carrier of V)
r * (Carrier u2) is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in Carrier u2 } is set
r * A is Element of the carrier of V
{(r * A)} is non empty trivial finite 1 -element Element of K19( the carrier of V)
LI is set
qI is Element of the carrier of V
r * qI is Element of the carrier of V
(V,u2,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Carrier (V,u2,r) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (V,u2,r) . b₁ = 0 } is set
Sum (V,u2,r) is Element of the carrier of V
(V,u2,r) . (r * A) is V24() V32() ext-real Element of REAL
((V,u2,r) . (r * A)) * (r * A) is Element of the carrier of V
r " is V24() V32() ext-real Element of REAL
(r ") * (r * A) is Element of the carrier of V
u2 . ((r ") * (r * A)) is V24() V32() ext-real Element of REAL
(u2 . ((r ") * (r * A))) * (r * A) is Element of the carrier of V
(r ") * r is V24() V32() ext-real Element of REAL
((r ") * r) * A is Element of the carrier of V
u2 . (((r ") * r) * A) is V24() V32() ext-real Element of REAL
(u2 . (((r ") * r) * A)) * (r * A) is Element of the carrier of V
1 * A is Element of the carrier of V
u2 . (1 * A) is V24() V32() ext-real Element of REAL
(u2 . (1 * A)) * (r * A) is Element of the carrier of V
(u2 . A) * (r * A) is Element of the carrier of V
(p - u2) + u2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
u2 - u2 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
u2 + (- u2) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p + (u2 - u2) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p + (ZeroLC V) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum (p - u2) is Element of the carrier of V
Sum u2 is Element of the carrier of V
(Sum (p - u2)) + (Sum u2) is Element of the carrier of V
(u2 . A) * A is Element of the carrier of V
(Sum (p - u2)) + ((u2 . A) * A) is Element of the carrier of V
card (Carrier (p - u2)) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(V,(p - u2),r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum (V,(p - u2),r) is Element of the carrier of V
r * (Sum (p - u2)) is Element of the carrier of V
(V,(p - u2),r) + (V,u2,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(Sum (V,(p - u2),r)) + (Sum (V,u2,r)) is Element of the carrier of V
(u2 . A) * r is V24() V32() ext-real Element of REAL
((u2 . A) * r) * A is Element of the carrier of V
(r * (Sum (p - u2))) + (((u2 . A) * r) * A) is Element of the carrier of V
r * ((u2 . A) * A) is Element of the carrier of V
(r * (Sum (p - u2))) + (r * ((u2 . A) * A)) is Element of the carrier of V
w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Carrier w is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not w . b₁ = 0 } is set
card (Carrier w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum (V,w,r) is Element of the carrier of V
Sum w is Element of the carrier of V
r * (Sum w) is Element of the carrier of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
0. V is V84(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
r * (0. V) is Element of the carrier of V
Carrier v is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0 } is set
card (Carrier v) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
w is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Carrier w is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not w . b₁ = 0 } is set
card (Carrier w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum (V,w,r) is Element of the carrier of V
Sum w is Element of the carrier of V
r * (Sum w) is Element of the carrier of V
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
V is Element of the carrier of r
{V} is non empty trivial finite 1 -element Element of K19( the carrier of r)
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element Element of K19( the carrier of r)
- V is Element of the carrier of r
(- V) + {V} is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in {V} } is set
((- V) + {V}) \ {(0. r)} is Element of K19( the carrier of r)
(- V) + V is Element of the carrier of r
{} the carrier of r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() (r) Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
v is Element of the carrier of r
{V,v} is finite Element of K19( the carrier of r)
{v} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
w is Element of K19( the carrier of r)
- V is Element of the carrier of r
(- V) + {V,v} is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in {V,v} } is set
(- V) + v is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{((- V) + v),(0. r)} is finite Element of K19( the carrier of r)
w is set
p is Element of the carrier of r
(- V) + p is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
((- V) + {V,v}) \ {(0. r)} is Element of K19( the carrier of r)
{((- V) + v),(0. r)} \ {(0. r)} is finite Element of K19( the carrier of r)
- (- V) is Element of the carrier of r
v + (- V) is Element of the carrier of r
{((- V) + v)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
w is Element of K19( the carrier of r)
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
the Element of the carrier of r is Element of the carrier of r
{ the Element of the carrier of r} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
V is Element of K19( the carrier of r)
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum v is Element of the carrier of r
(r,v) is V24() V32() ext-real Element of REAL
Carrier v is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not v . b₁ = 0 } is set
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
w is Element of the carrier of r
- w is Element of the carrier of r
(- w) + V is Element of K19( the carrier of r)
{ ((- w) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
((- w) + V) \ {(0. r)} is Element of K19( the carrier of r)
{w} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
V \/ {w} is Element of K19( the carrier of r)
v . w is V24() V32() ext-real Element of REAL
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {w}
p . w is V24() V32() ext-real Element of REAL
v - p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v + (- p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(v - p),(- w)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(v - p),(- w)) . (0. r) is V24() V32() ext-real Element of REAL
(0. r) - (- w) is Element of the carrier of r
(v - p) . ((0. r) - (- w)) is V24() V32() ext-real Element of REAL
- (- w) is Element of the carrier of r
(v - p) . (- (- w)) is V24() V32() ext-real Element of REAL
(v - p) . w is V24() V32() ext-real Element of REAL
(v . w) - (p . w) is V24() V32() ext-real Element of REAL
Carrier (r,(v - p),(- w)) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,(v - p),(- w)) . b₁ = 0 } is set
Carrier p is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not p . b₁ = 0 } is set
Carrier (v - p) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (v - p) . b₁ = 0 } is set
(Carrier v) \/ (Carrier p) is finite Element of K19( the carrier of r)
(- w) + (Carrier (v - p)) is Element of K19( the carrier of r)
{ ((- w) + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier (v - p) } is set
(v - p) + p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p - p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
p + (- p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v + (p - p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v + (ZeroLC r) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,p,(- w)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,p,(- w)) is Element of the carrier of r
(r,p) is V24() V32() ext-real Element of REAL
(r,p) * (- w) is Element of the carrier of r
Sum p is Element of the carrier of r
((r,p) * (- w)) + (Sum p) is Element of the carrier of r
(p . w) * w is Element of the carrier of r
((r,p) * (- w)) + ((p . w) * w) is Element of the carrier of r
(p . w) * (- w) is Element of the carrier of r
((p . w) * (- w)) + ((p . w) * w) is Element of the carrier of r
(- w) + w is Element of the carrier of r
(p . w) * ((- w) + w) is Element of the carrier of r
(p . w) * (0. r) is Element of the carrier of r
(r,v,(- w)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,v,(- w)) is Element of the carrier of r
(r,v) * (- w) is Element of the carrier of r
((r,v) * (- w)) + (Sum v) is Element of the carrier of r
(0. r) + (0. r) is Element of the carrier of r
(r,(v - p),(- w)) + (r,p,(- w)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum ((r,(v - p),(- w)) + (r,p,(- w))) is Element of the carrier of r
Sum (r,(v - p),(- w)) is Element of the carrier of r
(Sum (r,(v - p),(- w))) + (0. r) is Element of the carrier of r
(r,(v - p),(0. r)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
w + (- w) is Element of the carrier of r
(r,(v - p),(w + (- w))) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(r,(v - p),(- w)),w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(v - p)) is V24() V32() ext-real Element of REAL
0 + (r,p) is V24() V32() ext-real Element of REAL
0 + (p . w) is V24() V32() ext-real Element of REAL
(Carrier (v - p)) \/ (Carrier p) is finite Element of K19( the carrier of r)
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
V is Element of K19( the carrier of r)
v is Element of the carrier of r
- v is Element of the carrier of r
(- v) + V is Element of K19( the carrier of r)
{ ((- v) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
((- v) + V) \ {(0. r)} is Element of K19( the carrier of r)
(- v) + v is Element of the carrier of r
(((- v) + V) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
I is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of ((- v) + V) \ {(0. r)}
Sum I is Element of the carrier of r
Carrier I is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not I . b₁ = 0 } is set
(r,I) is V24() V32() ext-real Element of REAL
- (r,I) is V24() V32() ext-real Element of REAL
A is V24() V32() ext-real Element of REAL
u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {(0. r)}
u2 . (0. r) is V24() V32() ext-real Element of REAL
I + u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(I + u2),v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier u2 is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not u2 . b₁ = 0 } is set
v + ((- v) + V) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in (- v) + V } is set
v + (- v) is Element of the carrier of r
(v + (- v)) + V is Element of K19( the carrier of r)
{ ((v + (- v)) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(0. r) + V is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
Carrier (r,(I + u2),v) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,(I + u2),v) . b₁ = 0 } is set
Carrier (I + u2) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (I + u2) . b₁ = 0 } is set
v + (Carrier (I + u2)) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier (I + u2) } is set
(Carrier I) \/ (Carrier u2) is finite Element of K19( the carrier of r)
(r,(r,(I + u2),v)) is V24() V32() ext-real Element of REAL
(r,(I + u2)) is V24() V32() ext-real Element of REAL
(r,u2) is V24() V32() ext-real Element of REAL
(r,I) + (r,u2) is V24() V32() ext-real Element of REAL
(r,I) + A is V24() V32() ext-real Element of REAL
Sum (r,(I + u2),v) is Element of the carrier of r
0 * v is Element of the carrier of r
Sum (I + u2) is Element of the carrier of r
(0 * v) + (Sum (I + u2)) is Element of the carrier of r
(0. r) + (Sum (I + u2)) is Element of the carrier of r
Sum u2 is Element of the carrier of r
(Sum I) + (Sum u2) is Element of the carrier of r
(u2 . (0. r)) * (0. r) is Element of the carrier of r
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(I + u2),(0. r)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(I + u2),((- v) + v)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(ZeroLC r),(- v)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
qI is set
LI is Element of the carrier of r
u2 . LI is V24() V32() ext-real Element of REAL
I . LI is V24() V32() ext-real Element of REAL
(I . LI) + 0 is V24() V32() ext-real Element of REAL
(I + u2) . LI is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
V is Element of K19( the carrier of r)
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum v is Element of the carrier of r
(r,v) is V24() V32() ext-real Element of REAL
Carrier v is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not v . b₁ = 0 } is set
v is Element of the carrier of r
- v is Element of the carrier of r
(- v) + V is Element of K19( the carrier of r)
{ ((- v) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
((- v) + V) \ {(0. r)} is Element of K19( the carrier of r)
v is set
w is Element of the carrier of r
- w is Element of the carrier of r
(- w) + V is Element of K19( the carrier of r)
{ ((- w) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
((- w) + V) \ {(0. r)} is Element of K19( the carrier of r)
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
V is Element of K19( the carrier of r)
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum v is Element of the carrier of r
(r,v) is V24() V32() ext-real Element of REAL
Carrier v is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not v . b₁ = 0 } is set
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
v is Element of the carrier of r
- v is Element of the carrier of r
(- v) + V is Element of K19( the carrier of r)
{ ((- v) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
((- v) + V) \ {(0. r)} is Element of K19( the carrier of r)
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
Sum w is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(r,w) is V24() V32() ext-real Element of REAL
Carrier w is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not w . b₁ = 0 } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
v is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum v is Element of the carrier of r
(r,v) is V24() V32() ext-real Element of REAL
Carrier v is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not v . b₁ = 0 } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is (r) Element of K19( the carrier of r)
v is Element of the carrier of r
v + V is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v + V
Sum p is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(r,p) is V24() V32() ext-real Element of REAL
- v is Element of the carrier of r
(r,p,(- v)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(r,p,(- v))) is V24() V32() ext-real Element of REAL
Carrier (r,p,(- v)) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,p,(- v)) . b₁ = 0 } is set
Carrier p is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not p . b₁ = 0 } is set
(- v) + (Carrier p) is Element of K19( the carrier of r)
{ ((- v) + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier p } is set
(- v) + (v + V) is Element of K19( the carrier of r)
{ ((- v) + b₁) where b₁ is Element of the carrier of r : b₁ in v + V } is set
(- v) + v is Element of the carrier of r
((- v) + v) + V is Element of K19( the carrier of r)
{ (((- v) + v) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(0. r) + V is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
Sum (r,p,(- v)) is Element of the carrier of r
0 * (- v) is Element of the carrier of r
(0 * (- v)) + (0. r) is Element of the carrier of r
(0. r) + (0. r) is Element of the carrier of r
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,p,(0. r)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v + (- v) is Element of the carrier of r
(r,p,(v + (- v))) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(ZeroLC r),v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of the carrier of r
v is Element of K19( the carrier of r)
V + v is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
- V is Element of the carrier of r
(- V) + (V + v) is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in V + v } is set
(- V) + V is Element of the carrier of r
((- V) + V) + v is Element of K19( the carrier of r)
{ (((- V) + V) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(0. r) + v is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is (r) Element of K19( the carrier of r)
v is V24() V32() ext-real Element of REAL
v * V is Element of K19( the carrier of r)
{ (v * b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() (r) Element of K19( the carrier of r)
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v * V
Sum w is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(r,w) is V24() V32() ext-real Element of REAL
v " is V24() V32() ext-real Element of REAL
(r,w,(v ")) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (r,w,(v ")) is Element of the carrier of r
(v ") * (0. r) is Element of the carrier of r
Carrier (r,w,(v ")) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,w,(v ")) . b₁ = 0 } is set
Carrier w is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not w . b₁ = 0 } is set
(v ") * (Carrier w) is Element of K19( the carrier of r)
{ ((v ") * b₁) where b₁ is Element of the carrier of r : b₁ in Carrier w } is set
(v ") * (v * V) is Element of K19( the carrier of r)
{ ((v ") * b₁) where b₁ is Element of the carrier of r : b₁ in v * V } is set
(v ") * v is V24() V32() ext-real Element of REAL
((v ") * v) * V is Element of K19( the carrier of r)
{ (((v ") * v) * b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
1 * V is Element of K19( the carrier of r)
{ (1 * b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(r,(r,w,(v "))) is V24() V32() ext-real Element of REAL
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,w,1) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
v * (v ") is V24() V32() ext-real Element of REAL
(r,w,(v * (v "))) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(ZeroLC r),v) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of K19( the carrier of V)
r * v is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
r " is V24() V32() ext-real Element of REAL
(r ") * (r * v) is Element of K19( the carrier of V)
{ ((r ") * b₁) where b₁ is Element of the carrier of V : b₁ in r * v } is set
(r ") * r is V24() V32() ext-real Element of REAL
((r ") * r) * v is Element of K19( the carrier of V)
{ (((r ") * r) * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
1 * v is Element of K19( the carrier of V)
{ (1 * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
V is Element of K19( the carrier of r)
V \ {(0. r)} is Element of K19( the carrier of r)
- (0. r) is Element of the carrier of r
(- (0. r)) + V is Element of K19( the carrier of r)
{ ((- (0. r)) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(0. r) + V is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
K19(K19( the carrier of r)) is non empty set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
K19(K19( the carrier of r)) is non empty set
V is Element of K19(K19( the carrier of r))
v is Element of K19( the carrier of r)
V is (r) Element of K19( the carrier of r)
{V} is non empty trivial finite 1 -element Element of K19(K19( the carrier of r))
v is Element of K19( the carrier of r)
v is Element of K19(K19( the carrier of r))
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
K19(K19( the carrier of r)) is non empty set
bool the carrier of r is non empty Element of K19(K19( the carrier of r))
{} (bool the carrier of r) is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() (r) Element of K19((bool the carrier of r))
K19((bool the carrier of r)) is non empty set
the (r) Element of K19( the carrier of r) is (r) Element of K19( the carrier of r)
{ the (r) Element of K19( the carrier of r)} is non empty trivial finite 1 -element (r) Element of K19(K19( the carrier of r))
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
K19(K19( the carrier of r)) is non empty set
V is Element of K19(K19( the carrier of r))
v is Element of K19(K19( the carrier of r))
V \/ v is Element of K19(K19( the carrier of r))
w is Element of K19( the carrier of r)
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
K19(K19( the carrier of r)) is non empty set
V is Element of K19(K19( the carrier of r))
v is Element of K19(K19( the carrier of r))
w is Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
[#] r is non empty non proper Element of K19( the carrier of r)
bool ([#] r) is non empty Element of K19(K19(([#] r)))
K19(([#] r)) is non empty set
K19(K19(([#] r))) is non empty set
w is set
p is Affine Element of K19( the carrier of r)
K19(K19( the carrier of r)) is non empty set
w is Element of K19(K19( the carrier of r))
meet w is Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
(r,V) is Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
w is Element of the carrier of r
p is Element of the carrier of r
I is V24() V32() ext-real Element of REAL
1 - I is V24() V32() ext-real Element of REAL
(1 - I) * w is Element of the carrier of r
I * p is Element of the carrier of r
((1 - I) * w) + (I * p) is Element of the carrier of r
A is set
u2 is Affine Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
w is set
p is Affine Element of K19( the carrier of r)
[#] r is non empty non proper Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Affine Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() Element of K19( the carrier of r)
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is non empty Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Affine Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of the carrier of r
v is Element of K19( the carrier of r)
V + v is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
(r,(V + v)) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V + v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V + v c= b₁ } is set
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
V + (r,v) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in (r,v) } is set
- V is Element of the carrier of r
(- V) + (V + v) is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in V + v } is set
(- V) + V is Element of the carrier of r
((- V) + V) + v is Element of K19( the carrier of r)
{ (((- V) + V) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(0. r) + v is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
(- V) + (r,(V + v)) is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in (r,(V + v)) } is set
V + ((- V) + (r,(V + v))) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in (- V) + (r,(V + v)) } is set
V + (- V) is Element of the carrier of r
(V + (- V)) + (r,(V + v)) is Element of K19( the carrier of r)
{ ((V + (- V)) + b₁) where b₁ is Element of the carrier of r : b₁ in (r,(V + v)) } is set
(0. r) + (r,(V + v)) is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in (r,(V + v)) } is set
r is V24() V32() ext-real Element of REAL
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of K19( the carrier of V)
r * v is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
w is Element of the carrier of V
p is Element of the carrier of V
I is V24() V32() ext-real Element of REAL
1 - I is V24() V32() ext-real Element of REAL
(1 - I) * w is Element of the carrier of V
I * p is Element of the carrier of V
((1 - I) * w) + (I * p) is Element of the carrier of V
A is Element of the carrier of V
r * A is Element of the carrier of V
u2 is Element of the carrier of V
r * u2 is Element of the carrier of V
(1 - I) * A is Element of the carrier of V
I * u2 is Element of the carrier of V
((1 - I) * A) + (I * u2) is Element of the carrier of V
(1 - I) * (r * A) is Element of the carrier of V
(1 - I) * r is V24() V32() ext-real Element of REAL
((1 - I) * r) * A is Element of the carrier of V
r * ((1 - I) * A) is Element of the carrier of V
I * (r * u2) is Element of the carrier of V
I * r is V24() V32() ext-real Element of REAL
(I * r) * u2 is Element of the carrier of V
r * (I * u2) is Element of the carrier of V
r * (((1 - I) * A) + (I * u2)) is Element of the carrier of V
r is V24() V32() ext-real Element of REAL
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of K19( the carrier of V)
r * v is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(V,(r * v)) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : r * v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : r * v c= b₁ } is set
(V,v) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
r * (V,v) is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in (V,v) } is set
r " is V24() V32() ext-real Element of REAL
(r ") * (r * v) is Element of K19( the carrier of V)
{ ((r ") * b₁) where b₁ is Element of the carrier of V : b₁ in r * v } is set
(r ") * r is V24() V32() ext-real Element of REAL
((r ") * r) * v is Element of K19( the carrier of V)
{ (((r ") * r) * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
1 * v is Element of K19( the carrier of V)
{ (1 * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(r ") * (V,(r * v)) is Element of K19( the carrier of V)
{ ((r ") * b₁) where b₁ is Element of the carrier of V : b₁ in (V,(r * v)) } is set
r * ((r ") * (V,(r * v))) is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in (r ") * (V,(r * v)) } is set
r * (r ") is V24() V32() ext-real Element of REAL
(r * (r ")) * (V,(r * v)) is Element of K19( the carrier of V)
{ ((r * (r ")) * b₁) where b₁ is Element of the carrier of V : b₁ in (V,(r * v)) } is set
1 * (V,(r * v)) is Element of K19( the carrier of V)
{ (1 * b₁) where b₁ is Element of the carrier of V : b₁ in (V,(r * v)) } is set
r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of K19( the carrier of V)
r * v is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(V,(r * v)) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : r * v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : r * v c= b₁ } is set
(V,v) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
r * (V,v) is Element of K19( the carrier of V)
{ (r * b₁) where b₁ is Element of the carrier of V : b₁ in (V,v) } is set
0. V is V84(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty trivial finite 1 -element (V) Element of K19( the carrier of V)
w is set
p is Element of the carrier of V
r * p is Element of the carrier of V
p is set
I is Element of the carrier of V
r * I is Element of the carrier of V
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of the carrier of r
- V is Element of the carrier of r
v is Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
(- V) + v is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
Lin ((- V) + v) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((- V) + v)) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((- V) + v)) is non empty set
V + (Up (Lin ((- V) + v))) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- V) + v)) } is set
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : (- V) + v c= b₁ } is set
I is set
(r,((- V) + v)) is Affine Element of K19( the carrier of r)
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : (- V) + v c= b₁ } is set
(- V) + V is Element of the carrier of r
(- V) + (r,v) is Element of K19( the carrier of r)
{ ((- V) + b₁) where b₁ is Element of the carrier of r : b₁ in (r,v) } is set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
I is set
A is Affine Element of K19( the carrier of r)
Lin A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
the carrier of (Lin A) is non empty set
V + ((- V) + (r,v)) is Element of K19( the carrier of r)
{ (V + b₁) where b₁ is Element of the carrier of r : b₁ in (- V) + (r,v) } is set
V + (- V) is Element of the carrier of r
(V + (- V)) + (r,v) is Element of K19( the carrier of r)
{ ((V + (- V)) + b₁) where b₁ is Element of the carrier of r : b₁ in (r,v) } is set
(0. r) + (r,v) is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in (r,v) } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
V is Element of K19( the carrier of r)
V \/ {(0. r)} is Element of K19( the carrier of r)
Lin (V \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
(0). r is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
the carrier of ((0). r) is non empty set
Lin {(0. r)} is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
(Lin V) + ((0). r) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
w is set
p is Element of the carrier of r
{p} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
V \ {p} is Element of K19( the carrier of r)
(r,(V \ {p})) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V \ {p} c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V \ {p} c= b₁ } is set
I is set
A is Element of the carrier of r
- A is Element of the carrier of r
- (- A) is Element of the carrier of r
(- A) + p is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(- A) + V is Element of K19( the carrier of r)
{ ((- A) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
((- A) + V) \ {(0. r)} is Element of K19( the carrier of r)
{((- A) + p)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
(((- A) + V) \ {(0. r)}) \ {((- A) + p)} is Element of K19( the carrier of r)
Lin ((((- A) + V) \ {(0. r)}) \ {((- A) + p)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
A + ((- A) + p) is Element of the carrier of r
A + (- A) is Element of the carrier of r
(A + (- A)) + p is Element of the carrier of r
(0. r) + p is Element of the carrier of r
(- A) + A is Element of the carrier of r
((- A) + V) \ {((- A) + p)} is Element of K19( the carrier of r)
{(0. r)} \/ {((- A) + p)} is finite Element of K19( the carrier of r)
((- A) + V) \ ({(0. r)} \/ {((- A) + p)}) is Element of K19( the carrier of r)
(((- A) + V) \ {((- A) + p)}) \ {(0. r)} is Element of K19( the carrier of r)
((((- A) + V) \ {((- A) + p)}) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
Lin (((((- A) + V) \ {((- A) + p)}) \ {(0. r)}) \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin (((- A) + V) \ {((- A) + p)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
(- A) + {p} is (r) Element of K19( the carrier of r)
{ ((- A) + b₁) where b₁ is Element of the carrier of r : b₁ in {p} } is set
((- A) + V) \ ((- A) + {p}) is Element of K19( the carrier of r)
Lin (((- A) + V) \ ((- A) + {p})) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
(- A) + (V \ {p}) is Element of K19( the carrier of r)
{ ((- A) + b₁) where b₁ is Element of the carrier of r : b₁ in V \ {p} } is set
Lin ((- A) + (V \ {p})) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((((- A) + V) \ {(0. r)}) \ {((- A) + p)})) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((((- A) + V) \ {(0. r)}) \ {((- A) + p)})) is non empty set
A + (Up (Lin ((((- A) + V) \ {(0. r)}) \ {((- A) + p)}))) is Element of K19( the carrier of r)
{ (A + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((((- A) + V) \ {(0. r)}) \ {((- A) + p)})) } is set
q is Element of the carrier of r
A + q is Element of the carrier of r
v is Element of the carrier of r
- v is Element of the carrier of r
(- v) + V is Element of K19( the carrier of r)
{ ((- v) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
((- v) + V) \ {(0. r)} is Element of K19( the carrier of r)
Lin (((- v) + V) \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
the carrier of (Lin (((- v) + V) \ {(0. r)})) is non empty set
p is set
K19( the carrier of (Lin (((- v) + V) \ {(0. r)}))) is non empty set
(- v) + v is Element of the carrier of r
p is Element of K19( the carrier of (Lin (((- v) + V) \ {(0. r)})))
p \/ {(0. r)} is set
Lin p is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin (((- v) + V) \ {(0. r)})
I is Element of K19( the carrier of (Lin (((- v) + V) \ {(0. r)})))
Lin I is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin (((- v) + V) \ {(0. r)})
A is linearly-independent (r) Element of K19( the carrier of r)
A \/ {(0. r)} is Element of K19( the carrier of r)
v + (0. r) is Element of the carrier of r
v + (A \/ {(0. r)}) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in A \/ {(0. r)} } is set
(r,(v + (A \/ {(0. r)}))) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v + (A \/ {(0. r)}) c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v + (A \/ {(0. r)}) c= b₁ } is set
v + ((- v) + V) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in (- v) + V } is set
v + (- v) is Element of the carrier of r
(v + (- v)) + V is Element of K19( the carrier of r)
{ ((v + (- v)) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(0. r) + V is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(- v) + (v + (A \/ {(0. r)})) is Element of K19( the carrier of r)
{ ((- v) + b₁) where b₁ is Element of the carrier of r : b₁ in v + (A \/ {(0. r)}) } is set
((- v) + v) + (A \/ {(0. r)}) is Element of K19( the carrier of r)
{ (((- v) + v) + b₁) where b₁ is Element of the carrier of r : b₁ in A \/ {(0. r)} } is set
(0. r) + (A \/ {(0. r)}) is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in A \/ {(0. r)} } is set
Lin ((- v) + V) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((- v) + V)) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((- v) + V)) is non empty set
v + (Up (Lin ((- v) + V))) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- v) + V)) } is set
(((- v) + V) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
Lin ((((- v) + V) \ {(0. r)}) \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((((- v) + V) \ {(0. r)}) \/ {(0. r)})) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((((- v) + V) \ {(0. r)}) \/ {(0. r)})) is non empty set
v + (Up (Lin ((((- v) + V) \ {(0. r)}) \/ {(0. r)}))) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((((- v) + V) \ {(0. r)}) \/ {(0. r)})) } is set
Up (Lin (((- v) + V) \ {(0. r)})) is non empty Element of K19( the carrier of r)
v + (Up (Lin (((- v) + V) \ {(0. r)}))) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin (((- v) + V) \ {(0. r)})) } is set
Lin A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin A) is non empty Element of K19( the carrier of r)
the carrier of (Lin A) is non empty set
v + (Up (Lin A)) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin A) } is set
Lin ((- v) + (v + (A \/ {(0. r)}))) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((- v) + (v + (A \/ {(0. r)})))) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((- v) + (v + (A \/ {(0. r)})))) is non empty set
v + (Up (Lin ((- v) + (v + (A \/ {(0. r)}))))) is Element of K19( the carrier of r)
{ (v + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- v) + (v + (A \/ {(0. r)})))) } is set
(A \/ {(0. r)}) \ {(0. r)} is Element of K19( the carrier of r)
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
{ (Sum b₁) where b₁ is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V : (r,b₁) = 1 } is set
w is set
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum p is Element of the carrier of r
(r,p) is V24() V32() ext-real Element of REAL
{} the carrier of r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() (r) Element of K19( the carrier of r)
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
w is set
p is Element of the carrier of r
- p is Element of the carrier of r
(- p) + V is Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
Lin ((- p) + V) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((- p) + V)) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((- p) + V)) is non empty set
p + (Up (Lin ((- p) + V))) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- p) + V)) } is set
I is set
A is Element of the carrier of r
p + A is Element of the carrier of r
u2 is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of (- p) + V
Sum u2 is Element of the carrier of r
(r,u2,p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
(r,u2) is V24() V32() ext-real Element of REAL
1 - (r,u2) is V24() V32() ext-real Element of REAL
LI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {(0. r)}
LI . (0. r) is V24() V32() ext-real Element of REAL
u2 + LI is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,(u2 + LI),p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,LI,p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier LI is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not LI . b₁ = 0 } is set
p + (Carrier LI) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier LI } is set
p + {(0. r)} is (r) Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in {(0. r)} } is set
Carrier (r,u2,p) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,u2,p) . b₁ = 0 } is set
Carrier u2 is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not u2 . b₁ = 0 } is set
p + (Carrier u2) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier u2 } is set
p + ((- p) + V) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in (- p) + V } is set
p + (- p) is Element of the carrier of r
(p + (- p)) + V is Element of K19( the carrier of r)
{ ((p + (- p)) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(0. r) + V is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
(r,u2,p) + (r,LI,p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier ((r,u2,p) + (r,LI,p)) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not ((r,u2,p) + (r,LI,p)) . b₁ = 0 } is set
Carrier (r,LI,p) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,LI,p) . b₁ = 0 } is set
(Carrier (r,u2,p)) \/ (Carrier (r,LI,p)) is finite Element of K19( the carrier of r)
p + (0. r) is Element of the carrier of r
{(p + (0. r))} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
{p} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
V \/ {p} is Element of K19( the carrier of r)
Carrier (r,(u2 + LI),p) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,(u2 + LI),p) . b₁ = 0 } is set
(r,(r,(u2 + LI),p)) is V24() V32() ext-real Element of REAL
(r,(u2 + LI)) is V24() V32() ext-real Element of REAL
(r,LI) is V24() V32() ext-real Element of REAL
(r,u2) + (r,LI) is V24() V32() ext-real Element of REAL
(r,u2) + (1 - (r,u2)) is V24() V32() ext-real Element of REAL
Sum (r,(u2 + LI),p) is Element of the carrier of r
1 * p is Element of the carrier of r
Sum (u2 + LI) is Element of the carrier of r
(1 * p) + (Sum (u2 + LI)) is Element of the carrier of r
Sum LI is Element of the carrier of r
A + (Sum LI) is Element of the carrier of r
(1 * p) + (A + (Sum LI)) is Element of the carrier of r
(LI . (0. r)) * (0. r) is Element of the carrier of r
A + ((LI . (0. r)) * (0. r)) is Element of the carrier of r
(1 * p) + (A + ((LI . (0. r)) * (0. r))) is Element of the carrier of r
A + (0. r) is Element of the carrier of r
(1 * p) + (A + (0. r)) is Element of the carrier of r
p + (A + (0. r)) is Element of the carrier of r
I is set
A is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum A is Element of the carrier of r
(r,A) is V24() V32() ext-real Element of REAL
(r,A,(- p)) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Carrier A is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not A . b₁ = 0 } is set
(- p) + (Carrier A) is Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in Carrier A } is set
Carrier (r,A,(- p)) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (r,A,(- p)) . b₁ = 0 } is set
Sum (r,A,(- p)) is Element of the carrier of r
p + (Sum (r,A,(- p))) is Element of the carrier of r
1 * (- p) is Element of the carrier of r
(1 * (- p)) + (Sum A) is Element of the carrier of r
p + ((1 * (- p)) + (Sum A)) is Element of the carrier of r
(- p) + (Sum A) is Element of the carrier of r
p + ((- p) + (Sum A)) is Element of the carrier of r
p + (- p) is Element of the carrier of r
(p + (- p)) + (Sum A) is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(0. r) + (Sum A) is Element of the carrier of r
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is (r) Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
w is set
p is Element of the carrier of r
- p is Element of the carrier of r
(- p) + V is Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
Lin ((- p) + V) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
[#] (Lin ((- p) + V)) is non empty non proper Element of K19( the carrier of (Lin ((- p) + V)))
the carrier of (Lin ((- p) + V)) is non empty set
K19( the carrier of (Lin ((- p) + V))) is non empty set
A is set
A is Element of K19( the carrier of (Lin ((- p) + V)))
Lin A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin ((- p) + V)
u2 is Element of K19( the carrier of (Lin ((- p) + V)))
Lin u2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin ((- p) + V)
[#] r is non empty non proper Element of K19( the carrier of r)
q is Element of K19( the carrier of r)
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
q \/ {(0. r)} is Element of K19( the carrier of r)
(q \/ {(0. r)}) \ {(0. r)} is Element of K19( the carrier of r)
p + (q \/ {(0. r)}) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in q \/ {(0. r)} } is set
qI is (r) Element of K19( the carrier of r)
(r,qI) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : qI c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : qI c= b₁ } is set
LI is set
LA is Element of the carrier of r
p + LA is Element of the carrier of r
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
pA is Element of the carrier of r
(- p) + pA is Element of the carrier of r
p + (- p) is Element of the carrier of r
(p + (- p)) + pA is Element of the carrier of r
(0. r) + pA is Element of the carrier of r
(- p) + qI is (r) Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in qI } is set
(- p) + p is Element of the carrier of r
((- p) + p) + (q \/ {(0. r)}) is Element of K19( the carrier of r)
{ (((- p) + p) + b₁) where b₁ is Element of the carrier of r : b₁ in q \/ {(0. r)} } is set
(0. r) + (q \/ {(0. r)}) is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in q \/ {(0. r)} } is set
p + (0. r) is Element of the carrier of r
Lin (q \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin (q \/ {(0. r)})) is non empty Element of K19( the carrier of r)
the carrier of (Lin (q \/ {(0. r)})) is non empty set
p + (Up (Lin (q \/ {(0. r)}))) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin (q \/ {(0. r)})) } is set
Lin q is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin q) is non empty Element of K19( the carrier of r)
the carrier of (Lin q) is non empty set
p + (Up (Lin q)) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin q) } is set
Up (Lin ((- p) + V)) is non empty Element of K19( the carrier of r)
p + (Up (Lin ((- p) + V))) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- p) + V)) } is set
w is set
p is Element of the carrier of r
- p is Element of the carrier of r
(- p) + v is (r) Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
((- p) + v) \ {(0. r)} is Element of K19( the carrier of r)
(- p) + V is Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
Lin ((- p) + V) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((- p) + V)) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((- p) + V)) is non empty set
A is set
K19( the carrier of (Lin ((- p) + V))) is non empty set
u2 is Element of K19( the carrier of (Lin ((- p) + V)))
Lin u2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin ((- p) + V)
A is Element of K19( the carrier of (Lin ((- p) + V)))
q is linearly-independent ( Lin ((- p) + V)) Element of K19( the carrier of (Lin ((- p) + V)))
Lin q is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin ((- p) + V)
LI is linearly-independent (r) Element of K19( the carrier of r)
LI \/ {(0. r)} is Element of K19( the carrier of r)
(LI \/ {(0. r)}) \ {(0. r)} is Element of K19( the carrier of r)
p + (LI \/ {(0. r)}) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in LI \/ {(0. r)} } is set
LI is (r) Element of K19( the carrier of r)
(r,LI) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : LI c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : LI c= b₁ } is set
(- p) + p is Element of the carrier of r
p + ((- p) + v) is (r) Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in (- p) + v } is set
(0. r) + v is (r) Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in v } is set
(((- p) + v) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
LA is set
pA is Element of the carrier of r
p + pA is Element of the carrier of r
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
u is Element of the carrier of r
(- p) + u is Element of the carrier of r
p + (- p) is Element of the carrier of r
(p + (- p)) + u is Element of the carrier of r
(0. r) + u is Element of the carrier of r
(- p) + LI is (r) Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in LI } is set
(0. r) + (LI \/ {(0. r)}) is Element of K19( the carrier of r)
{ ((0. r) + b₁) where b₁ is Element of the carrier of r : b₁ in LI \/ {(0. r)} } is set
Lin (LI \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin (LI \/ {(0. r)})) is non empty Element of K19( the carrier of r)
the carrier of (Lin (LI \/ {(0. r)})) is non empty set
p + (Up (Lin (LI \/ {(0. r)}))) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin (LI \/ {(0. r)})) } is set
Lin LI is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin LI) is non empty Element of K19( the carrier of r)
the carrier of (Lin LI) is non empty set
p + (Up (Lin LI)) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin LI) } is set
p + (Up (Lin ((- p) + V))) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- p) + V)) } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is finite Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is finite Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
card v is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
card V is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
w is set
(card V) - 1 is V24() V32() ext-real Element of REAL
I is Element of the carrier of r
- I is Element of the carrier of r
(- I) + V is Element of K19( the carrier of r)
{ ((- I) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
Lin ((- I) + V) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() (r) Element of K19( the carrier of r)
u2 is (r) Element of K19( the carrier of r)
(r,u2) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : u2 c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : u2 c= b₁ } is set
q is set
[#] (Lin ((- I) + V)) is non empty non proper Element of K19( the carrier of (Lin ((- I) + V)))
the carrier of (Lin ((- I) + V)) is non empty set
K19( the carrier of (Lin ((- I) + V))) is non empty set
LI is set
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
((- I) + V) \ {(0. r)} is Element of K19( the carrier of r)
LI is Element of K19( the carrier of (Lin ((- I) + V)))
LI \ {(0. r)} is Element of K19( the carrier of (Lin ((- I) + V)))
(- I) + I is Element of the carrier of r
(((- I) + V) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
Lin ((((- I) + V) \ {(0. r)}) \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin (((- I) + V) \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin (LI \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin ((- I) + V)
I + (Lin ((- I) + V)) is Element of K19( the carrier of r)
Up (Lin ((- I) + V)) is non empty Element of K19( the carrier of r)
I + (Up (Lin ((- I) + V))) is Element of K19( the carrier of r)
{ (I + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- I) + V)) } is set
LI is Element of the carrier of r
- LI is Element of the carrier of r
(- LI) + u2 is (r) Element of K19( the carrier of r)
{ ((- LI) + b₁) where b₁ is Element of the carrier of r : b₁ in u2 } is set
Lin ((- LI) + u2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Up (Lin ((- LI) + u2)) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((- LI) + u2)) is non empty set
LI + (Up (Lin ((- LI) + u2))) is Element of K19( the carrier of r)
{ (LI + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- LI) + u2)) } is set
LI + (Lin ((- LI) + u2)) is Element of K19( the carrier of r)
[#] (Lin ((- LI) + u2)) is non empty non proper Element of K19( the carrier of (Lin ((- LI) + u2)))
K19( the carrier of (Lin ((- LI) + u2))) is non empty set
pA is set
card LI is ordinal cardinal set
p is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
p + 1 is non empty V24() ordinal natural V32() ext-real positive non negative finite cardinal Element of REAL
card (LI \ {(0. r)}) is ordinal cardinal set
((- LI) + u2) \ {(0. r)} is Element of K19( the carrier of r)
pA is Element of K19( the carrier of (Lin ((- LI) + u2)))
pA \ {(0. r)} is Element of K19( the carrier of (Lin ((- LI) + u2)))
(- LI) + LI is Element of the carrier of r
(((- LI) + u2) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
Lin ((((- LI) + u2) \ {(0. r)}) \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin (((- LI) + u2) \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin (pA \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin ((- LI) + u2)
card (pA \ {(0. r)}) is ordinal cardinal set
(pA \ {(0. r)}) \/ {(0. r)} is set
card ((pA \ {(0. r)}) \/ {(0. r)}) is ordinal cardinal set
card pA is ordinal cardinal set
card u2 is ordinal cardinal set
qI is finite set
card qI is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
V is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(r,V) is V24() V32() ext-real Element of REAL
Carrier V is finite Element of K19( the carrier of r)
K19( the carrier of r) is non empty set
{ b₁ where b₁ is Element of the carrier of r : not V . b₁ = 0 } is set
v is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng v is set
len v is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
Sum w is V24() V32() ext-real Element of REAL
K406(REAL,w,K148()) is V24() V32() ext-real Element of REAL
dom w is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
Sum w is V24() V32() ext-real Element of REAL
K406(REAL,w,K148()) is V24() V32() ext-real Element of REAL
dom w is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
V * v is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len (V * v) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
p is V24() ordinal natural V32() ext-real non negative finite cardinal set
w . p is V24() V32() ext-real Element of REAL
v . p is set
V . (v . p) is V24() V32() ext-real Element of REAL
dom (V * v) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
(V * v) . p is V24() V32() ext-real Element of REAL
p is Element of the carrier of r
dom v is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
I is set
v . I is set
w . I is V24() V32() ext-real Element of REAL
V . (v . I) is V24() V32() ext-real Element of REAL
V . p is V24() V32() ext-real Element of REAL
p is Element of the carrier of r
V . p is V24() V32() ext-real Element of REAL
p is Element of the carrier of r
v is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng v is set
V * v is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (V * v) is V24() V32() ext-real Element of REAL
K406(REAL,(V * v),K148()) is V24() V32() ext-real Element of REAL
w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng w is set
V * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len p is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
Sum p is V24() V32() ext-real Element of REAL
K406(REAL,p,K148()) is V24() V32() ext-real Element of REAL
dom w is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom p is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
I is V24() ordinal natural V32() ext-real non negative finite cardinal set
p . I is V24() V32() ext-real Element of REAL
w . I is set
V . (w . I) is V24() V32() ext-real Element of REAL
w /. I is Element of the carrier of r
w is Relation-like NAT -defined the carrier of r -valued Function-like FinSequence-like FinSequence of the carrier of r
rng w is set
p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
len p is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
Sum p is V24() V32() ext-real Element of REAL
K406(REAL,p,K148()) is V24() V32() ext-real Element of REAL
dom p is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
r is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
v . r is V24() V32() ext-real Element of REAL
(V,v) is V24() V32() ext-real Element of REAL
Carrier v is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0 } is set
w is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng w is set
v * w is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum (v * w) is V24() V32() ext-real Element of REAL
K406(REAL,(v * w),K148()) is V24() V32() ext-real Element of REAL
dom v is set
p is Element of the carrier of V
dom w is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
I is set
w . I is set
len (v * w) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len w is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
dom (v * w) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
A is V24() ordinal natural V32() ext-real non negative finite cardinal set
(v * w) . A is V24() V32() ext-real Element of REAL
w . A is set
v . (w . A) is V24() V32() ext-real Element of REAL
w /. A is Element of the carrier of V
A is V24() ordinal natural V32() ext-real non negative finite cardinal set
(v * w) . A is V24() V32() ext-real Element of REAL
r is set
{r} is non empty trivial finite 1 -element set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
v . r is V24() V32() ext-real Element of REAL
Carrier v is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0 } is set
dom v is set
w is Element of the carrier of V
{w} is non empty trivial finite 1 -element (V) Element of K19( the carrier of V)
p is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {w}
p . w is V24() V32() ext-real Element of REAL
v - p is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
- p is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(- 1) * p is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
v + (- p) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Carrier p is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not p . b₁ = 0 } is set
(V,(v - p)) is V24() V32() ext-real Element of REAL
(V,v) is V24() V32() ext-real Element of REAL
(V,p) is V24() V32() ext-real Element of REAL
(V,v) - (V,p) is V24() V32() ext-real Element of REAL
(V,v) - 1 is V24() V32() ext-real Element of REAL
1 - 1 is V24() V32() ext-real Element of REAL
Carrier (v - p) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (v - p) . b₁ = 0 } is set
A is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng A is set
(v - p) * A is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V55() V56() V57() FinSequence of REAL
Sum ((v - p) * A) is V24() V32() ext-real Element of REAL
K406(REAL,((v - p) * A),K148()) is V24() V32() ext-real Element of REAL
len ((v - p) * A) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
len A is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
dom ((v - p) * A) is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
dom A is V65() V66() V67() V68() V69() V70() Element of K19(NAT)
u2 is V24() ordinal natural V32() ext-real non negative finite cardinal set
((v - p) * A) . u2 is V24() V32() ext-real Element of REAL
A . u2 is set
(v - p) . (A . u2) is V24() V32() ext-real Element of REAL
v . (A . u2) is V24() V32() ext-real Element of REAL
p . (A . u2) is V24() V32() ext-real Element of REAL
(v . (A . u2)) - (p . (A . u2)) is V24() V32() ext-real Element of REAL
u2 is set
q is Element of the carrier of V
LI is set
A . LI is set
qI is V24() ordinal natural V32() ext-real non negative finite cardinal set
((v - p) * A) . qI is V24() V32() ext-real Element of REAL
(v - p) . q is V24() V32() ext-real Element of REAL
v . q is V24() V32() ext-real Element of REAL
p . q is V24() V32() ext-real Element of REAL
(v . q) - (p . q) is V24() V32() ext-real Element of REAL
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
- v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(- 1) * v is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
- (- v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(- 1) * (- v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is non empty Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is set
w is non empty Element of K19( the carrier of r)
conv w is non empty convex Element of K19( the carrier of r)
Convex-Family w is non empty Element of K19(K19( the carrier of r))
meet (Convex-Family w) is Element of K19( the carrier of r)
ConvexComb r is set
{ (Sum b₁) where b₁ is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() convex Linear_Combination of w : b₁ in ConvexComb r } is set
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() convex Linear_Combination of w
Sum p is Element of the carrier of r
(r,p) is V24() V32() ext-real Element of REAL
{ (Sum b₁) where b₁ is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V : (r,b₁) = 1 } is set
r is set
{r} is non empty trivial finite 1 -element set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of K19( the carrier of V)
conv v is convex Element of K19( the carrier of V)
Convex-Family v is non empty Element of K19(K19( the carrier of V))
K19(K19( the carrier of V)) is non empty set
meet (Convex-Family v) is Element of K19( the carrier of V)
(conv v) \ {r} is Element of K19( the carrier of V)
w is non empty Element of K19( the carrier of V)
conv w is non empty convex Element of K19( the carrier of V)
Convex-Family w is non empty Element of K19(K19( the carrier of V))
meet (Convex-Family w) is Element of K19( the carrier of V)
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() convex Linear_Combination of w : b₁ in ConvexComb V } is set
p is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() convex Linear_Combination of w
Sum p is Element of the carrier of V
Carrier p is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not p . b₁ = 0 } is set
A is set
(V,p) is V24() V32() ext-real Element of REAL
u2 is Element of the carrier of V
{u2} is non empty trivial finite 1 -element (V) Element of K19( the carrier of V)
(Carrier p) \ {u2} is finite Element of K19( the carrier of V)
p . u2 is V24() V32() ext-real Element of REAL
(p . u2) * u2 is Element of the carrier of V
q is set
LI is Element of the carrier of V
p . LI is V24() V32() ext-real Element of REAL
p . u2 is V24() V32() ext-real Element of REAL
min ((p . u2),(p . LI)) is V24() V32() ext-real set
{LI} is non empty trivial finite 1 -element (V) Element of K19( the carrier of V)
qI is V24() V32() ext-real Element of REAL
LI is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {LI}
LI . LI is V24() V32() ext-real Element of REAL
u2 - LI is Element of the carrier of V
0. V is V84(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
Carrier LI is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not LI . b₁ = 0 } is set
LA is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {u2}
LA . u2 is V24() V32() ext-real Element of REAL
Carrier LA is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not LA . b₁ = 0 } is set
LA - LI is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
- LI is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(- 1) * LI is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
LA + (- LI) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
- (LA - LI) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(- 1) * (LA - LI) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p + (LA - LI) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p - (LA - LI) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
p + (- (LA - LI)) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
u is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of w
Sum u is Element of the carrier of V
Sum (LA - LI) is Element of the carrier of V
(Sum p) - (Sum (LA - LI)) is Element of the carrier of V
- (Sum (LA - LI)) is Element of the carrier of V
(Sum p) + (- (Sum (LA - LI))) is Element of the carrier of V
v is Element of the carrier of V
u . v is V24() V32() ext-real Element of REAL
p . v is V24() V32() ext-real Element of REAL
(LA - LI) . v is V24() V32() ext-real Element of REAL
(p . v) - ((LA - LI) . v) is V24() V32() ext-real Element of REAL
LA . v is V24() V32() ext-real Element of REAL
LI . v is V24() V32() ext-real Element of REAL
(LA . v) - (LI . v) is V24() V32() ext-real Element of REAL
(p . v) - ((LA . v) - (LI . v)) is V24() V32() ext-real Element of REAL
qI - qI is V24() V32() ext-real Element of REAL
(p . u2) - qI is V24() V32() ext-real Element of REAL
Sum LA is Element of the carrier of V
Sum LI is Element of the carrier of V
(Sum LA) - (Sum LI) is Element of the carrier of V
qI * u2 is Element of the carrier of V
(qI * u2) - (Sum LI) is Element of the carrier of V
qI * LI is Element of the carrier of V
(qI * u2) - (qI * LI) is Element of the carrier of V
qI * (u2 - LI) is Element of the carrier of V
(V,(LA - LI)) is V24() V32() ext-real Element of REAL
(V,LA) is V24() V32() ext-real Element of REAL
(V,LI) is V24() V32() ext-real Element of REAL
(V,LA) - (V,LI) is V24() V32() ext-real Element of REAL
qI - (V,LI) is V24() V32() ext-real Element of REAL
qI - qI is V24() V32() ext-real Element of REAL
pA is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of w
v is Element of the carrier of V
pA . v is V24() V32() ext-real Element of REAL
p . v is V24() V32() ext-real Element of REAL
(LA - LI) . v is V24() V32() ext-real Element of REAL
(p . v) + ((LA - LI) . v) is V24() V32() ext-real Element of REAL
LA . v is V24() V32() ext-real Element of REAL
LI . v is V24() V32() ext-real Element of REAL
(LA . v) - (LI . v) is V24() V32() ext-real Element of REAL
(p . v) + ((LA . v) - (LI . v)) is V24() V32() ext-real Element of REAL
qI - 0 is V24() V32() ext-real Element of REAL
(p . v) + (qI - 0) is V24() V32() ext-real Element of REAL
(p . LI) - qI is V24() V32() ext-real Element of REAL
(V,u) is V24() V32() ext-real Element of REAL
(V,p) - (V,(LA - LI)) is V24() V32() ext-real Element of REAL
1 + 0 is non empty V24() ordinal natural V32() ext-real positive non negative finite cardinal Element of REAL
(V,pA) is V24() V32() ext-real Element of REAL
(V,p) + (V,(LA - LI)) is V24() V32() ext-real Element of REAL
Sum pA is Element of the carrier of V
- (0. V) is Element of the carrier of V
(Sum p) + (Sum (LA - LI)) is Element of the carrier of V
1 / 2 is non empty V24() V32() ext-real positive non negative Element of REAL
(1 / 2) * (Sum pA) is Element of the carrier of V
1 - (1 / 2) is V24() V32() ext-real Element of REAL
(1 - (1 / 2)) * (Sum u) is Element of the carrier of V
((1 / 2) * (Sum pA)) + ((1 - (1 / 2)) * (Sum u)) is Element of the carrier of V
(1 / 2) * ((Sum p) + (Sum (LA - LI))) is Element of the carrier of V
(1 / 2) * ((Sum p) + (- (Sum (LA - LI)))) is Element of the carrier of V
((1 / 2) * ((Sum p) + (Sum (LA - LI)))) + ((1 / 2) * ((Sum p) + (- (Sum (LA - LI))))) is Element of the carrier of V
(1 / 2) * (Sum p) is Element of the carrier of V
(1 / 2) * (Sum (LA - LI)) is Element of the carrier of V
((1 / 2) * (Sum p)) + ((1 / 2) * (Sum (LA - LI))) is Element of the carrier of V
(((1 / 2) * (Sum p)) + ((1 / 2) * (Sum (LA - LI)))) + ((1 / 2) * ((Sum p) + (- (Sum (LA - LI))))) is Element of the carrier of V
(1 / 2) * (- (Sum (LA - LI))) is Element of the carrier of V
((1 / 2) * (Sum p)) + ((1 / 2) * (- (Sum (LA - LI)))) is Element of the carrier of V
(((1 / 2) * (Sum p)) + ((1 / 2) * (Sum (LA - LI)))) + (((1 / 2) * (Sum p)) + ((1 / 2) * (- (Sum (LA - LI))))) is Element of the carrier of V
((1 / 2) * (- (Sum (LA - LI)))) + ((1 / 2) * (Sum p)) is Element of the carrier of V
((1 / 2) * (Sum (LA - LI))) + (((1 / 2) * (- (Sum (LA - LI)))) + ((1 / 2) * (Sum p))) is Element of the carrier of V
((1 / 2) * (Sum p)) + (((1 / 2) * (Sum (LA - LI))) + (((1 / 2) * (- (Sum (LA - LI)))) + ((1 / 2) * (Sum p)))) is Element of the carrier of V
((1 / 2) * (Sum (LA - LI))) + ((1 / 2) * (- (Sum (LA - LI)))) is Element of the carrier of V
(((1 / 2) * (Sum (LA - LI))) + ((1 / 2) * (- (Sum (LA - LI))))) + ((1 / 2) * (Sum p)) is Element of the carrier of V
((1 / 2) * (Sum p)) + ((((1 / 2) * (Sum (LA - LI))) + ((1 / 2) * (- (Sum (LA - LI))))) + ((1 / 2) * (Sum p))) is Element of the carrier of V
(Sum (LA - LI)) + (- (Sum (LA - LI))) is Element of the carrier of V
(1 / 2) * ((Sum (LA - LI)) + (- (Sum (LA - LI)))) is Element of the carrier of V
((1 / 2) * ((Sum (LA - LI)) + (- (Sum (LA - LI))))) + ((1 / 2) * (Sum p)) is Element of the carrier of V
((1 / 2) * (Sum p)) + (((1 / 2) * ((Sum (LA - LI)) + (- (Sum (LA - LI))))) + ((1 / 2) * (Sum p))) is Element of the carrier of V
(1 / 2) * (0. V) is Element of the carrier of V
((1 / 2) * (0. V)) + ((1 / 2) * (Sum p)) is Element of the carrier of V
((1 / 2) * (Sum p)) + (((1 / 2) * (0. V)) + ((1 / 2) * (Sum p))) is Element of the carrier of V
(0. V) + ((1 / 2) * (Sum p)) is Element of the carrier of V
((1 / 2) * (Sum p)) + ((0. V) + ((1 / 2) * (Sum p))) is Element of the carrier of V
((1 / 2) * (Sum p)) + ((1 / 2) * (Sum p)) is Element of the carrier of V
(1 / 2) + (1 / 2) is non empty V24() V32() ext-real positive non negative Element of REAL
((1 / 2) + (1 / 2)) * (Sum p) is Element of the carrier of V
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is non empty Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
(r,(conv V)) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : conv V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : conv V c= b₁ } is set
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is set
{ (Sum b₁) where b₁ is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V : (r,b₁) = 1 } is set
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum w is Element of the carrier of r
(r,w) is V24() V32() ext-real Element of REAL
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of conv V
Sum p is Element of the carrier of r
{ (Sum b₁) where b₁ is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of conv V : (r,b₁) = 1 } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
conv V is convex Element of K19( the carrier of r)
Convex-Family V is non empty Element of K19(K19( the carrier of r))
K19(K19( the carrier of r)) is non empty set
meet (Convex-Family V) is Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is Element of K19( the carrier of r)
conv v is convex Element of K19( the carrier of r)
Convex-Family v is non empty Element of K19(K19( the carrier of r))
meet (Convex-Family v) is Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
(r,(conv V)) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : conv V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : conv V c= b₁ } is set
(r,(conv v)) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : conv v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : conv v c= b₁ } is set
r is non empty RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
V \/ v is Element of K19( the carrier of r)
(r,(V \/ v)) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V \/ v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V \/ v c= b₁ } is set
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of K19( the carrier of r)
v is set
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
{ (Sum b₁) where b₁ is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V : (r,b₁) = 1 } is set
w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum w is Element of the carrier of r
(r,w) is V24() V32() ext-real Element of REAL
p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum p is Element of the carrier of r
(r,p) is V24() V32() ext-real Element of REAL
w - p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * p is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
w + (- p) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
Sum (w - p) is Element of the carrier of r
(Sum w) - (Sum w) is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
(r,(w - p)) is V24() V32() ext-real Element of REAL
1 - 1 is V24() V32() ext-real Element of REAL
Carrier (w - p) is finite Element of K19( the carrier of r)
{ b₁ where b₁ is Element of the carrier of r : not (w - p) . b₁ = 0 } is set
ZeroLC r is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * w is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
- (- w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
(- 1) * (- w) is Relation-like the carrier of r -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of r
r is V24() V32() ext-real Element of REAL
1 - r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of the carrier of V
(1 - r) * v is Element of the carrier of V
w is Element of the carrier of V
r * w is Element of the carrier of V
((1 - r) * v) + (r * w) is Element of the carrier of V
p is (V) Element of K19( the carrier of V)
(V,p) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : p c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : p c= b₁ } is set
(V,p,(((1 - r) * v) + (r * w))) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of p
(V,p,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of p
(1 - r) * (V,p,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,p,w) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of p
r * (V,p,w) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
((1 - r) * (V,p,v)) + (r * (V,p,w)) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
Sum (((1 - r) * (V,p,v)) + (r * (V,p,w))) is Element of the carrier of V
Sum ((1 - r) * (V,p,v)) is Element of the carrier of V
Sum (r * (V,p,w)) is Element of the carrier of V
(Sum ((1 - r) * (V,p,v))) + (Sum (r * (V,p,w))) is Element of the carrier of V
Sum (V,p,v) is Element of the carrier of V
(1 - r) * (Sum (V,p,v)) is Element of the carrier of V
((1 - r) * (Sum (V,p,v))) + (Sum (r * (V,p,w))) is Element of the carrier of V
Sum (V,p,w) is Element of the carrier of V
r * (Sum (V,p,w)) is Element of the carrier of V
((1 - r) * (Sum (V,p,v))) + (r * (Sum (V,p,w))) is Element of the carrier of V
((1 - r) * v) + (r * (Sum (V,p,w))) is Element of the carrier of V
(V,(((1 - r) * (V,p,v)) + (r * (V,p,w)))) is V24() V32() ext-real Element of REAL
(V,((1 - r) * (V,p,v))) is V24() V32() ext-real Element of REAL
(V,(r * (V,p,w))) is V24() V32() ext-real Element of REAL
(V,((1 - r) * (V,p,v))) + (V,(r * (V,p,w))) is V24() V32() ext-real Element of REAL
(V,(V,p,v)) is V24() V32() ext-real Element of REAL
(1 - r) * (V,(V,p,v)) is V24() V32() ext-real Element of REAL
((1 - r) * (V,(V,p,v))) + (V,(r * (V,p,w))) is V24() V32() ext-real Element of REAL
(V,(V,p,w)) is V24() V32() ext-real Element of REAL
r * (V,(V,p,w)) is V24() V32() ext-real Element of REAL
((1 - r) * (V,(V,p,v))) + (r * (V,(V,p,w))) is V24() V32() ext-real Element of REAL
(1 - r) * 1 is V24() V32() ext-real Element of REAL
((1 - r) * 1) + (r * (V,(V,p,w))) is V24() V32() ext-real Element of REAL
r * 1 is V24() V32() ext-real Element of REAL
((1 - r) * 1) + (r * 1) is V24() V32() ext-real Element of REAL
r is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of the carrier of V
w is (V) Element of K19( the carrier of V)
conv w is convex Element of K19( the carrier of V)
Convex-Family w is non empty Element of K19(K19( the carrier of V))
K19(K19( the carrier of V)) is non empty set
meet (Convex-Family w) is Element of K19( the carrier of V)
(V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of w
(V,w,r) . v is V24() V32() ext-real Element of REAL
p is non empty Element of K19( the carrier of V)
conv p is non empty convex Element of K19( the carrier of V)
Convex-Family p is non empty Element of K19(K19( the carrier of V))
meet (Convex-Family p) is Element of K19( the carrier of V)
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() convex Linear_Combination of p : b₁ in ConvexComb V } is set
I is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() convex Linear_Combination of p
Sum I is Element of the carrier of V
(V,w) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : w c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : w c= b₁ } is set
(V,I) is V24() V32() ext-real Element of REAL
r is set
V is set
v is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of v is non empty set
K19( the carrier of v) is non empty set
w is (v) Element of K19( the carrier of v)
conv w is convex Element of K19( the carrier of v)
Convex-Family w is non empty Element of K19(K19( the carrier of v))
K19(K19( the carrier of v)) is non empty set
meet (Convex-Family w) is Element of K19( the carrier of v)
(v,w,r) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of w
(v,w,r) . V is V24() V32() ext-real Element of REAL
Carrier (v,w,r) is finite Element of K19( the carrier of v)
{ b₁ where b₁ is Element of the carrier of v : not (v,w,r) . b₁ = 0 } is set
{V} is non empty trivial finite 1 -element set
(v,w) is Affine Element of K19( the carrier of v)
{ b₁ where b₁ is Affine Element of K19( the carrier of v) : w c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of v) : w c= b₁ } is set
Sum (v,w,r) is Element of the carrier of v
I is Element of the carrier of v
(v,w,r) . I is V24() V32() ext-real Element of REAL
((v,w,r) . I) * I is Element of the carrier of v
p is Element of the carrier of v
{p} is non empty trivial finite 1 -element (v) Element of K19( the carrier of v)
I is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of {p}
I . p is V24() V32() ext-real Element of REAL
Carrier I is finite Element of K19( the carrier of v)
{ b₁ where b₁ is Element of the carrier of v : not I . b₁ = 0 } is set
(v,I) is V24() V32() ext-real Element of REAL
Sum I is Element of the carrier of v
1 * p is Element of the carrier of v
r is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is (V) Element of K19( the carrier of V)
(V,v) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
conv v is convex Element of K19( the carrier of V)
Convex-Family v is non empty Element of K19(K19( the carrier of V))
K19(K19( the carrier of V)) is non empty set
meet (Convex-Family v) is Element of K19( the carrier of V)
Sum (V,v,r) is Element of the carrier of V
I is Element of the carrier of V
(V,v,r) . I is V24() V32() ext-real Element of REAL
Carrier (V,v,r) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (V,v,r) . b₁ = 0 } is set
(V,(V,v,r)) is V24() V32() ext-real Element of REAL
p is non empty Element of K19( the carrier of V)
conv p is non empty convex Element of K19( the carrier of V)
Convex-Family p is non empty Element of K19(K19( the carrier of V))
meet (Convex-Family p) is Element of K19( the carrier of V)
ConvexComb V is set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() convex Linear_Combination of p : b₁ in ConvexComb V } is set
r is set
{r} is non empty trivial finite 1 -element set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is (V) Element of K19( the carrier of V)
conv v is convex Element of K19( the carrier of V)
Convex-Family v is non empty Element of K19(K19( the carrier of V))
K19(K19( the carrier of V)) is non empty set
meet (Convex-Family v) is Element of K19( the carrier of V)
(conv v) \ {r} is Element of K19( the carrier of V)
(V,v) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
p is Element of the carrier of V
A is V24() V32() ext-real Element of REAL
A * p is Element of the carrier of V
I is Element of the carrier of V
1 - A is V24() V32() ext-real Element of REAL
(1 - A) * I is Element of the carrier of V
(A * p) + ((1 - A) * I) is Element of the carrier of V
1 - 1 is V24() V32() ext-real Element of REAL
(V,v,I) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
w is Element of the carrier of V
(V,v,I) . w is V24() V32() ext-real Element of REAL
(V,v,p) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(V,v,p) . w is V24() V32() ext-real Element of REAL
(V,v,((A * p) + ((1 - A) * I))) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(1 - A) * (V,v,I) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
A * (V,v,p) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
((1 - A) * (V,v,I)) + (A * (V,v,p)) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
q is Element of the carrier of V
(V,v,((A * p) + ((1 - A) * I))) . q is V24() V32() ext-real Element of REAL
((1 - A) * (V,v,I)) . q is V24() V32() ext-real Element of REAL
(A * (V,v,p)) . q is V24() V32() ext-real Element of REAL
(((1 - A) * (V,v,I)) . q) + ((A * (V,v,p)) . q) is V24() V32() ext-real Element of REAL
(V,v,I) . q is V24() V32() ext-real Element of REAL
(1 - A) * ((V,v,I) . q) is V24() V32() ext-real Element of REAL
((1 - A) * ((V,v,I) . q)) + ((A * (V,v,p)) . q) is V24() V32() ext-real Element of REAL
(V,v,p) . q is V24() V32() ext-real Element of REAL
A * ((V,v,p) . q) is V24() V32() ext-real Element of REAL
((1 - A) * ((V,v,I) . q)) + (A * ((V,v,p) . q)) is V24() V32() ext-real Element of REAL
A * 1 is V24() V32() ext-real Element of REAL
A * ((V,v,p) . w) is V24() V32() ext-real Element of REAL
(1 - A) * 1 is V24() V32() ext-real Element of REAL
(1 - A) * ((V,v,I) . w) is V24() V32() ext-real Element of REAL
((1 - A) * 1) + (A * 1) is V24() V32() ext-real Element of REAL
((1 - A) * ((V,v,I) . w)) + (A * ((V,v,p) . w)) is V24() V32() ext-real Element of REAL
(V,v,((A * p) + ((1 - A) * I))) . w is V24() V32() ext-real Element of REAL
((1 - A) * (V,v,I)) . w is V24() V32() ext-real Element of REAL
(A * (V,v,p)) . w is V24() V32() ext-real Element of REAL
(((1 - A) * (V,v,I)) . w) + ((A * (V,v,p)) . w) is V24() V32() ext-real Element of REAL
((1 - A) * ((V,v,I) . w)) + ((A * (V,v,p)) . w) is V24() V32() ext-real Element of REAL
r is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is (V) Element of K19( the carrier of V)
(V,v) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
w is Element of K19( the carrier of V)
v \ w is Element of K19( the carrier of V)
(V,(v \ w)) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v \ w c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v \ w c= b₁ } is set
(V,(v \ w),r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v \ w
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v : (V,b₁) = 1 } is set
p is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
Sum p is Element of the carrier of V
(V,p) is V24() V32() ext-real Element of REAL
Carrier p is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not p . b₁ = 0 } is set
I is set
p . I is V24() V32() ext-real Element of REAL
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v \ w : (V,b₁) = 1 } is set
r is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is (V) Element of K19( the carrier of V)
conv v is convex Element of K19( the carrier of V)
Convex-Family v is non empty Element of K19(K19( the carrier of V))
K19(K19( the carrier of V)) is non empty set
meet (Convex-Family v) is Element of K19( the carrier of V)
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
w is Element of K19( the carrier of V)
v \ w is Element of K19( the carrier of V)
conv (v \ w) is convex Element of K19( the carrier of V)
Convex-Family (v \ w) is non empty Element of K19(K19( the carrier of V))
meet (Convex-Family (v \ w)) is Element of K19( the carrier of V)
(V,v) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
(V,(v \ w),r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v \ w
I is Element of the carrier of V
(V,(v \ w),r) . I is V24() V32() ext-real Element of REAL
(V,(v \ w)) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v \ w c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v \ w c= b₁ } is set
r is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of K19( the carrier of V)
(V,v) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : v c= b₁ } is set
(V,v,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
w is (V) Element of K19( the carrier of V)
(V,w,r) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of w
Sum (V,v,r) is Element of the carrier of V
(V,(V,v,r)) is V24() V32() ext-real Element of REAL
(V,w) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : w c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : w c= b₁ } is set
r is V24() V32() ext-real Element of REAL
V is V24() V32() ext-real Element of REAL
r + V is V24() V32() ext-real Element of REAL
v is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of v is non empty set
K19( the carrier of v) is non empty set
w is Element of the carrier of v
r * w is Element of the carrier of v
p is Element of the carrier of v
V * p is Element of the carrier of v
(r * w) + (V * p) is Element of the carrier of v
I is Element of K19( the carrier of v)
(v,I) is Affine Element of K19( the carrier of v)
{ b₁ where b₁ is Affine Element of K19( the carrier of v) : I c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of v) : I c= b₁ } is set
{ (Sum b₁) where b₁ is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of I : (v,b₁) = 1 } is set
A is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of I
Sum A is Element of the carrier of v
(v,A) is V24() V32() ext-real Element of REAL
u2 is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of I
Sum u2 is Element of the carrier of v
(v,u2) is V24() V32() ext-real Element of REAL
r * A is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
V * u2 is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(r * A) + (V * u2) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
Sum ((r * A) + (V * u2)) is Element of the carrier of v
Sum (r * A) is Element of the carrier of v
Sum (V * u2) is Element of the carrier of v
(Sum (r * A)) + (Sum (V * u2)) is Element of the carrier of v
r * (Sum A) is Element of the carrier of v
(r * (Sum A)) + (Sum (V * u2)) is Element of the carrier of v
(v,((r * A) + (V * u2))) is V24() V32() ext-real Element of REAL
(v,(r * A)) is V24() V32() ext-real Element of REAL
(v,(V * u2)) is V24() V32() ext-real Element of REAL
(v,(r * A)) + (v,(V * u2)) is V24() V32() ext-real Element of REAL
r * (v,A) is V24() V32() ext-real Element of REAL
(r * (v,A)) + (v,(V * u2)) is V24() V32() ext-real Element of REAL
r * 1 is V24() V32() ext-real Element of REAL
V * 1 is V24() V32() ext-real Element of REAL
(r * 1) + (V * 1) is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is finite Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is finite Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
card V is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
card v is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
w is set
p is Element of the carrier of r
- p is Element of the carrier of r
(- p) + V is Element of K19( the carrier of r)
{ ((- p) + b₁) where b₁ is Element of the carrier of r : b₁ in V } is set
Lin ((- p) + V) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
card ((- p) + V) is ordinal cardinal set
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() (r) Element of K19( the carrier of r)
A is (r) Element of K19( the carrier of r)
(r,A) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : A c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : A c= b₁ } is set
u2 is set
q is Element of the carrier of r
- q is Element of the carrier of r
(- q) + A is (r) Element of K19( the carrier of r)
{ ((- q) + b₁) where b₁ is Element of the carrier of r : b₁ in A } is set
Lin ((- q) + A) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
card A is ordinal cardinal set
card ((- q) + A) is ordinal cardinal set
the carrier of (Lin ((- q) + A)) is non empty set
qI is set
K19( the carrier of (Lin ((- q) + A))) is non empty set
(- q) + q is Element of the carrier of r
0. r is V84(r) Element of the carrier of r
the ZeroF of r is Element of the carrier of r
qI is finite Element of K19( the carrier of (Lin ((- q) + A)))
{(0. r)} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
((- q) + A) \ {(0. r)} is Element of K19( the carrier of r)
(((- q) + A) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
Lin ((((- q) + A) \ {(0. r)}) \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin (((- q) + A) \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
qI \ {(0. r)} is finite Element of K19( the carrier of (Lin ((- q) + A)))
Lin (qI \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of Lin ((- q) + A)
LI is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() finite-dimensional Subspace of r
Up LI is non empty Element of K19( the carrier of r)
the carrier of LI is non empty set
q + (Up LI) is Element of K19( the carrier of r)
{ (q + b₁) where b₁ is Element of the carrier of r : b₁ in Up LI } is set
Up (Lin ((- p) + V)) is non empty Element of K19( the carrier of r)
the carrier of (Lin ((- p) + V)) is non empty set
p + (Up (Lin ((- p) + V))) is Element of K19( the carrier of r)
{ (p + b₁) where b₁ is Element of the carrier of r : b₁ in Up (Lin ((- p) + V)) } is set
LA is set
2 + (- 1) is V24() V32() ext-real Element of REAL
2 * q is Element of the carrier of r
(- 1) * p is Element of the carrier of r
(2 * q) + ((- 1) * p) is Element of the carrier of r
1 + 1 is non empty V24() ordinal natural V32() ext-real positive non negative finite cardinal Element of REAL
(1 + 1) * q is Element of the carrier of r
((1 + 1) * q) + ((- 1) * p) is Element of the carrier of r
1 * q is Element of the carrier of r
(1 * q) + (1 * q) is Element of the carrier of r
((1 * q) + (1 * q)) + ((- 1) * p) is Element of the carrier of r
((1 * q) + (1 * q)) + (- p) is Element of the carrier of r
(1 * q) + q is Element of the carrier of r
((1 * q) + q) + (- p) is Element of the carrier of r
q + q is Element of the carrier of r
(q + q) + (- p) is Element of the carrier of r
(q + q) - p is Element of the carrier of r
q - p is Element of the carrier of r
(q - p) + q is Element of the carrier of r
q + LI is Element of K19( the carrier of r)
pA is Element of the carrier of r
p + pA is Element of the carrier of r
u is Element of the carrier of r
q + u is Element of the carrier of r
(q + u) - p is Element of the carrier of r
u - p is Element of the carrier of r
q + (u - p) is Element of the carrier of r
p - q is Element of the carrier of r
u - (p - q) is Element of the carrier of r
- (p - q) is Element of the carrier of r
u + (- (p - q)) is Element of the carrier of r
q + (- p) is Element of the carrier of r
u + (q + (- p)) is Element of the carrier of r
u + (q - p) is Element of the carrier of r
LA is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() finite-dimensional Subspace of LI
the carrier of LA is non empty set
pA is set
K19( the carrier of LA) is non empty set
(- p) + p is Element of the carrier of r
pA is finite Element of K19( the carrier of LA)
((- p) + V) \ {(0. r)} is Element of K19( the carrier of r)
card {(0. r)} is non empty V24() ordinal natural V32() V33() V34() ext-real positive non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
dim LI is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
card (qI \ {(0. r)}) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
card qI is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(card qI) - 1 is V24() V32() ext-real Element of REAL
(((- p) + V) \ {(0. r)}) \/ {(0. r)} is Element of K19( the carrier of r)
Lin ((((- p) + V) \ {(0. r)}) \/ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
Lin (((- p) + V) \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() Subspace of r
pA \ {(0. r)} is finite Element of K19( the carrier of LA)
Lin (pA \ {(0. r)}) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() finite-dimensional Subspace of LA
dim LA is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of NAT
card (pA \ {(0. r)}) is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
(card V) - 1 is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is finite Element of K19( the carrier of r)
(r,V) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : V c= b₁ } is set
v is finite Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
card V is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
card v is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
{} r is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty proper V24() ordinal natural V32() ext-real non positive non negative finite finite-yielding V44() cardinal {} -element V55() V56() V57() V58() V65() V66() V67() V68() V69() V70() V71() (r) Element of K19( the carrier of r)
w is (r) Element of K19( the carrier of r)
(r,w) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : w c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : w c= b₁ } is set
p is finite Element of K19( the carrier of r)
card p is V24() ordinal natural V32() V33() V34() ext-real non negative finite cardinal V65() V66() V67() V68() V69() V70() Element of omega
r is V24() V32() ext-real Element of REAL
1 - r is V24() V32() ext-real Element of REAL
V is V24() V32() ext-real Element of REAL
v is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of v is non empty set
w is Element of the carrier of v
p is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
p . w is V24() V32() ext-real Element of REAL
r * p is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
I is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
I . w is V24() V32() ext-real Element of REAL
(1 - r) * I is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
(r * p) + ((1 - r) * I) is Relation-like the carrier of v -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of v
((r * p) + ((1 - r) * I)) . w is V24() V32() ext-real Element of REAL
(I . w) - V is V24() V32() ext-real Element of REAL
(I . w) - (p . w) is V24() V32() ext-real Element of REAL
((I . w) - V) / ((I . w) - (p . w)) is V24() V32() ext-real Element of REAL
(r * p) . w is V24() V32() ext-real Element of REAL
((1 - r) * I) . w is V24() V32() ext-real Element of REAL
((r * p) . w) + (((1 - r) * I) . w) is V24() V32() ext-real Element of REAL
r * (p . w) is V24() V32() ext-real Element of REAL
(r * (p . w)) + (((1 - r) * I) . w) is V24() V32() ext-real Element of REAL
- r is V24() V32() ext-real Element of REAL
(- r) + 1 is V24() V32() ext-real Element of REAL
((- r) + 1) * (I . w) is V24() V32() ext-real Element of REAL
(r * (p . w)) + (((- r) + 1) * (I . w)) is V24() V32() ext-real Element of REAL
(p . w) - (I . w) is V24() V32() ext-real Element of REAL
r * ((p . w) - (I . w)) is V24() V32() ext-real Element of REAL
(r * ((p . w) - (I . w))) + (I . w) is V24() V32() ext-real Element of REAL
r * ((I . w) - (p . w)) is V24() V32() ext-real Element of REAL
((I . w) - V) * 1 is V24() V32() ext-real Element of REAL
r / 1 is V24() V32() ext-real Element of REAL
- ((p . w) - (I . w)) is V24() V32() ext-real Element of REAL
((I . w) - V) / (- ((p . w) - (I . w))) is V24() V32() ext-real Element of REAL
(((I . w) - V) / (- ((p . w) - (I . w)))) * ((p . w) - (I . w)) is V24() V32() ext-real Element of REAL
((((I . w) - V) / (- ((p . w) - (I . w)))) * ((p . w) - (I . w))) + (I . w) is V24() V32() ext-real Element of REAL
- ((I . w) - V) is V24() V32() ext-real Element of REAL
(- ((I . w) - V)) / ((p . w) - (I . w)) is V24() V32() ext-real Element of REAL
((- ((I . w) - V)) / ((p . w) - (I . w))) * ((p . w) - (I . w)) is V24() V32() ext-real Element of REAL
(((- ((I . w) - V)) / ((p . w) - (I . w))) * ((p . w) - (I . w))) + (I . w) is V24() V32() ext-real Element of REAL
(- ((I . w) - V)) + (I . w) is V24() V32() ext-real Element of REAL
r is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of r is non empty set
K19( the carrier of r) is non empty set
V is Element of the carrier of r
{V} is non empty trivial finite 1 -element (r) Element of K19( the carrier of r)
v is Element of K19( the carrier of r)
v \/ {V} is Element of K19( the carrier of r)
(r,v) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v c= b₁ } is set
(r,(v \/ {V})) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v \/ {V} c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v \/ {V} c= b₁ } is set
(r,(v \/ {V})) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : v \/ {V} c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : v \/ {V} c= b₁ } is set
p is (r) Element of K19( the carrier of r)
(r,p) is Affine Element of K19( the carrier of r)
{ b₁ where b₁ is Affine Element of K19( the carrier of r) : p c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of r) : p c= b₁ } is set
(v \/ {V}) \ {V} is Element of K19( the carrier of r)
r is V24() V32() ext-real Element of REAL
1 - r is V24() V32() ext-real Element of REAL
V is V24() V32() ext-real Element of REAL
1 - V is V24() V32() ext-real Element of REAL
v is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of v is non empty set
K19( the carrier of v) is non empty set
w is Element of the carrier of v
r * w is Element of the carrier of v
V * w is Element of the carrier of v
p is Element of the carrier of v
(1 - r) * p is Element of the carrier of v
(r * w) + ((1 - r) * p) is Element of the carrier of v
I is Element of the carrier of v
(1 - V) * I is Element of the carrier of v
(V * w) + ((1 - V) * I) is Element of the carrier of v
A is Element of K19( the carrier of v)
(v,A) is Affine Element of K19( the carrier of v)
{ b₁ where b₁ is Affine Element of K19( the carrier of v) : A c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of v) : A c= b₁ } is set
0. v is V84(v) Element of the carrier of v
the ZeroF of v is Element of the carrier of v
(r * w) + (0. v) is Element of the carrier of v
((1 - r) * p) - ((1 - r) * p) is Element of the carrier of v
(r * w) + (((1 - r) * p) - ((1 - r) * p)) is Element of the carrier of v
((V * w) + ((1 - V) * I)) - ((1 - r) * p) is Element of the carrier of v
((1 - V) * I) - ((1 - r) * p) is Element of the carrier of v
(((1 - V) * I) - ((1 - r) * p)) + (V * w) is Element of the carrier of v
(r * w) - (V * w) is Element of the carrier of v
r - V is V24() V32() ext-real Element of REAL
(r - V) * w is Element of the carrier of v
1 / (r - V) is V24() V32() ext-real Element of REAL
(1 / (r - V)) * (1 - V) is V24() V32() ext-real Element of REAL
r - 1 is V24() V32() ext-real Element of REAL
(r - V) - (r - 1) is V24() V32() ext-real Element of REAL
((r - V) - (r - 1)) / (r - V) is V24() V32() ext-real Element of REAL
(r - V) / (r - V) is V24() V32() ext-real Element of REAL
(r - 1) / (r - V) is V24() V32() ext-real Element of REAL
((r - V) / (r - V)) - ((r - 1) / (r - V)) is V24() V32() ext-real Element of REAL
1 - ((r - 1) / (r - V)) is V24() V32() ext-real Element of REAL
(1 / (r - V)) * (1 - r) is V24() V32() ext-real Element of REAL
- ((1 / (r - V)) * (1 - r)) is V24() V32() ext-real Element of REAL
(1 - r) / (r - V) is V24() V32() ext-real Element of REAL
- ((1 - r) / (r - V)) is V24() V32() ext-real Element of REAL
- (1 - r) is V24() V32() ext-real Element of REAL
(- (1 - r)) / (r - V) is V24() V32() ext-real Element of REAL
(r - V) * (1 / (r - V)) is V24() V32() ext-real Element of REAL
(1 / (r - V)) * (r - V) is V24() V32() ext-real Element of REAL
((1 / (r - V)) * (r - V)) * w is Element of the carrier of v
(1 / (r - V)) * ((r - V) * w) is Element of the carrier of v
(1 / (r - V)) * ((1 - V) * I) is Element of the carrier of v
(1 / (r - V)) * ((1 - r) * p) is Element of the carrier of v
((1 / (r - V)) * ((1 - V) * I)) - ((1 / (r - V)) * ((1 - r) * p)) is Element of the carrier of v
((1 / (r - V)) * (1 - V)) * I is Element of the carrier of v
(((1 / (r - V)) * (1 - V)) * I) - ((1 / (r - V)) * ((1 - r) * p)) is Element of the carrier of v
((1 / (r - V)) * (1 - r)) * p is Element of the carrier of v
(((1 / (r - V)) * (1 - V)) * I) - (((1 / (r - V)) * (1 - r)) * p) is Element of the carrier of v
- (((1 / (r - V)) * (1 - r)) * p) is Element of the carrier of v
(((1 / (r - V)) * (1 - V)) * I) + (- (((1 / (r - V)) * (1 - r)) * p)) is Element of the carrier of v
(1 - ((r - 1) / (r - V))) * I is Element of the carrier of v
((r - 1) / (r - V)) * p is Element of the carrier of v
((1 - ((r - 1) / (r - V))) * I) + (((r - 1) / (r - V)) * p) is Element of the carrier of v
(1 - r) * I is Element of the carrier of v
r is V24() V32() ext-real Element of REAL
1 - r is V24() V32() ext-real Element of REAL
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V135() RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
v is Element of the carrier of V
{v} is non empty trivial finite 1 -element (V) Element of K19( the carrier of V)
r * v is Element of the carrier of V
w is Element of the carrier of V
p is Element of the carrier of V
(1 - r) * p is Element of the carrier of V
(r * v) + ((1 - r) * p) is Element of the carrier of V
I is (V) Element of K19( the carrier of V)
(V,I) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : I c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : I c= b₁ } is set
I \ {v} is Element of K19( the carrier of V)
(V,(I \ {v})) is Affine Element of K19( the carrier of V)
{ b₁ where b₁ is Affine Element of K19( the carrier of V) : I \ {v} c= b₁ } is set
meet { b₁ where b₁ is Affine Element of K19( the carrier of V) : I \ {v} c= b₁ } is set
(V,I,w) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of I
(V,I,w) . v is V24() V32() ext-real Element of REAL
conv I is convex Element of K19( the carrier of V)
Convex-Family I is non empty Element of K19(K19( the carrier of V))
K19(K19( the carrier of V)) is non empty set
meet (Convex-Family I) is Element of K19( the carrier of V)
(V,(I \ {v}),p) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of I \ {v}
Carrier (V,(I \ {v}),p) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (V,(I \ {v}),p) . b₁ = 0 } is set
(V,(I \ {v}),p) . v is V24() V32() ext-real Element of REAL
(V,I,p) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of I
(1 - r) * (V,I,p) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(V,I,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of I
r * (V,I,v) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
((1 - r) * (V,I,p)) + (r * (V,I,v)) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V55() V56() V57() Linear_Combination of V
(((1 - r) * (V,I,p)) + (r * (V,I,v))) . v is V24() V32() ext-real Element of REAL
((1 - r) * (V,I,p)) . v is V24() V32() ext-real Element of REAL
(r * (V,I,v)) . v is V24() V32() ext-real Element of REAL
(((1 - r) * (V,I,p)) . v) + ((r * (V,I,v)) . v) is V24() V32() ext-real Element of REAL
(V,I,v) . v is V24() V32() ext-real Element of REAL
r * ((V,I,v) . v) is V24() V32() ext-real Element of REAL
(((1 - r) * (V,I,p)) . v) + (r * ((V,I,v) . v)) is V24() V32() ext-real Element of REAL
(V,I,p) . v is V24() V32() ext-real Element of REAL
(1 - r) * ((V,I,p) . v) is V24() V32() ext-real Element of REAL
((1 - r) * ((V,I,p) . v)) + (r * ((V,I,v) . v)) is V24() V32() ext-real Element of REAL
r * 1 is V24() V32() ext-real Element of REAL
((1 - r) * ((V,I,p) . v)) + (r * 1) is V24() V32() ext-real Element of REAL
(1 - r) * ((V,(I \ {v}),p) . v) is V24() V32() ext-real Element of REAL
((1 - r) * ((V,(I \ {v}),p) . v)) + (r * 1) is V24() V32() ext-real Element of REAL