:: RUSUB_5 semantic presentation

REAL is V19() V20() V21() V25() set
NAT is V19() V20() V21() V22() V23() V24() V25() Element of K10(REAL)
K10(REAL) is non empty set
COMPLEX is V19() V25() set
omega is V19() V20() V21() V22() V23() V24() V25() set
K10(omega) is non empty set
K10(NAT) is non empty set
K11(NAT,REAL) is set
K10(K11(NAT,REAL)) is non empty set
{} is empty V19() V20() V21() V22() V23() V24() V25() set
the empty V19() V20() V21() V22() V23() V24() V25() set is empty V19() V20() V21() V22() V23() V24() V25() set
1 is non empty natural V14() real ext-real positive non negative V19() V20() V21() V22() V23() V24() Element of NAT
0 is empty natural V14() real ext-real non positive non negative V19() V20() V21() V22() V23() V24() V25() Element of NAT
- 1 is V14() real ext-real non positive Element of REAL
2 is non empty natural V14() real ext-real positive non negative V19() V20() V21() V22() V23() V24() Element of NAT
V is non empty RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
V is non empty right_zeroed RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Affine Element of K10( the carrier of V)
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
M + {(0. V)} is Element of K10( the carrier of V)
v is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {(0. V)} ) } is set
r is Element of the carrier of V
B is Element of the carrier of V
r + B is Element of the carrier of V
v is set
r is Element of the carrier of V
r + (0. V) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {(0. V)} ) } is set
V is non empty right_complementable add-associative right_zeroed RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Affine Element of K10( the carrier of V)
v is Affine Element of K10( the carrier of V)
r is Element of the carrier of V
{r} is non empty Element of K10( the carrier of V)
v + {r} is Element of K10( the carrier of V)
- r is Element of the carrier of V
{(- r)} is non empty Element of K10( the carrier of V)
M + {(- r)} is Element of K10( the carrier of V)
C is set
a is Element of the carrier of V
a + r is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {r} ) } is set
r + (- r) is Element of the carrier of V
a + (r + (- r)) is Element of the carrier of V
(a + r) + (- r) is Element of the carrier of V
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
a + (0. V) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {(- r)} ) } is set
C is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {(- r)} ) } is set
a is Element of the carrier of V
e is Element of the carrier of V
a + e is Element of the carrier of V
f is Element of the carrier of V
a + (- r) is Element of the carrier of V
f + r is Element of the carrier of V
(- r) + r is Element of the carrier of V
a + ((- r) + r) is Element of the carrier of V
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
a + (0. V) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {r} ) } is set
u1 is Element of the carrier of V
v2 is Element of the carrier of V
u1 + v2 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Affine Element of K10( the carrier of V)
v is Affine Element of K10( the carrier of V)
r is Affine Element of K10( the carrier of V)
B is Element of the carrier of V
{B} is non empty Element of K10( the carrier of V)
v + {B} is Element of K10( the carrier of V)
C is Element of the carrier of V
{C} is non empty Element of K10( the carrier of V)
r + {C} is Element of K10( the carrier of V)
C + B is Element of the carrier of V
{(C + B)} is non empty Element of K10( the carrier of V)
r + {(C + B)} is Element of K10( the carrier of V)
e is set
f is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in r & b₂ in {(C + B)} ) } is set
u1 is Element of the carrier of V
v2 is Element of the carrier of V
u1 + v2 is Element of the carrier of V
u1 + (C + B) is Element of the carrier of V
u1 + C is Element of the carrier of V
(u1 + C) + B is Element of the carrier of V
f - B is Element of the carrier of V
- B is Element of the carrier of V
f + (- B) is Element of the carrier of V
B - B is Element of the carrier of V
B + (- B) is Element of the carrier of V
(u1 + C) + (B - B) is Element of the carrier of V
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
(u1 + C) + (0. V) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in r & b₂ in {C} ) } is set
(f - B) + B is Element of the carrier of V
f - (B - B) is Element of the carrier of V
- (B - B) is Element of the carrier of V
f + (- (B - B)) is Element of the carrier of V
f - (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
f + (- (0. V)) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {B} ) } is set
e is set
f is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {B} ) } is set
u1 is Element of the carrier of V
v2 is Element of the carrier of V
u1 + v2 is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in r & b₂ in {C} ) } is set
u3 is Element of the carrier of V
v3 is Element of the carrier of V
u3 + v3 is Element of the carrier of V
u3 + (C + B) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in r & b₂ in {(C + B)} ) } is set
V is non empty addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Element of K10( the carrier of V)
v is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
{ H₁(b₁,b₂) where b₁, b₂ is Element of the carrier of V : S₁[b₁,b₂] } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Affine Element of K10( the carrier of V)
v is Affine Element of K10( the carrier of V)
(V,M,v) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
r is Element of the carrier of V
B is Element of the carrier of V
C is V14() real ext-real Element of REAL
1 - C is V14() real ext-real Element of REAL
(1 - C) * r is Element of the carrier of V
C * B is Element of the carrier of V
((1 - C) * r) + (C * B) is Element of the carrier of V
a is Element of the carrier of V
e is Element of the carrier of V
a - e is Element of the carrier of V
- e is Element of the carrier of V
a + (- e) is Element of the carrier of V
f is Element of the carrier of V
u1 is Element of the carrier of V
f - u1 is Element of the carrier of V
- u1 is Element of the carrier of V
f + (- u1) is Element of the carrier of V
(1 - C) * a is Element of the carrier of V
(1 - C) * e is Element of the carrier of V
((1 - C) * a) - ((1 - C) * e) is Element of the carrier of V
- ((1 - C) * e) is Element of the carrier of V
((1 - C) * a) + (- ((1 - C) * e)) is Element of the carrier of V
C * (f - u1) is Element of the carrier of V
(((1 - C) * a) - ((1 - C) * e)) + (C * (f - u1)) is Element of the carrier of V
C * f is Element of the carrier of V
C * u1 is Element of the carrier of V
(C * f) - (C * u1) is Element of the carrier of V
- (C * u1) is Element of the carrier of V
(C * f) + (- (C * u1)) is Element of the carrier of V
(((1 - C) * a) - ((1 - C) * e)) + ((C * f) - (C * u1)) is Element of the carrier of V
((1 - C) * a) + (- ((1 - C) * e)) is Element of the carrier of V
(((1 - C) * a) + (- ((1 - C) * e))) + (C * f) is Element of the carrier of V
((((1 - C) * a) + (- ((1 - C) * e))) + (C * f)) - (C * u1) is Element of the carrier of V
((((1 - C) * a) + (- ((1 - C) * e))) + (C * f)) + (- (C * u1)) is Element of the carrier of V
((1 - C) * a) + (C * f) is Element of the carrier of V
(((1 - C) * a) + (C * f)) + (- ((1 - C) * e)) is Element of the carrier of V
((((1 - C) * a) + (C * f)) + (- ((1 - C) * e))) + (- (C * u1)) is Element of the carrier of V
(- ((1 - C) * e)) + (- (C * u1)) is Element of the carrier of V
(((1 - C) * a) + (C * f)) + ((- ((1 - C) * e)) + (- (C * u1))) is Element of the carrier of V
((1 - C) * e) + (C * u1) is Element of the carrier of V
(((1 - C) * a) + (C * f)) - (((1 - C) * e) + (C * u1)) is Element of the carrier of V
- (((1 - C) * e) + (C * u1)) is Element of the carrier of V
(((1 - C) * a) + (C * f)) + (- (((1 - C) * e) + (C * u1))) is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Element of K10( the carrier of V)
v is Element of K10( the carrier of V)
M + v is Element of K10( the carrier of V)
r is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
B is Element of the carrier of V
C is Element of the carrier of V
B + C is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Element of K10( the carrier of V)
v is non empty Element of K10( the carrier of V)
M + v is Element of K10( the carrier of V)
r is set
B is set
C is Element of the carrier of V
a is Element of the carrier of V
C + a is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
V is non empty addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Element of K10( the carrier of V)
v is Element of K10( the carrier of V)
(V,M,v) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
r is set
B is Element of the carrier of V
C is Element of the carrier of V
B - C is Element of the carrier of V
- C is Element of the carrier of V
B + (- C) is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Element of K10( the carrier of V)
v is non empty Element of K10( the carrier of V)
(V,M,v) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
r is set
B is set
C is Element of the carrier of V
a is Element of the carrier of V
C - a is Element of the carrier of V
- a is Element of the carrier of V
C + (- a) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V125() addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is Element of K10( the carrier of V)
v is Element of K10( the carrier of V)
r is Element of the carrier of V
{r} is non empty Element of K10( the carrier of V)
v + {r} is Element of K10( the carrier of V)
(V,M,{r}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {r} ) } is set
B is set
C is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {r} ) } is set
a is Element of the carrier of V
e is Element of the carrier of V
a + e is Element of the carrier of V
C - e is Element of the carrier of V
- e is Element of the carrier of V
C + (- e) is Element of the carrier of V
e - e is Element of the carrier of V
e + (- e) is Element of the carrier of V
a + (e - e) is Element of the carrier of V
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
a + (0. V) is Element of the carrier of V
C - r is Element of the carrier of V
- r is Element of the carrier of V
C + (- r) is Element of the carrier of V
f is Element of the carrier of V
u1 is Element of the carrier of V
f - u1 is Element of the carrier of V
- u1 is Element of the carrier of V
f + (- u1) is Element of the carrier of V
(C - r) + r is Element of the carrier of V
r - r is Element of the carrier of V
r + (- r) is Element of the carrier of V
f - (r - r) is Element of the carrier of V
- (r - r) is Element of the carrier of V
f + (- (r - r)) is Element of the carrier of V
f - (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
f + (- (0. V)) is Element of the carrier of V
C - (r - r) is Element of the carrier of V
C + (- (r - r)) is Element of the carrier of V
C - (0. V) is Element of the carrier of V
C + (- (0. V)) is Element of the carrier of V
B is set
C is Element of the carrier of V
C - r is Element of the carrier of V
- r is Element of the carrier of V
C + (- r) is Element of the carrier of V
a is Element of the carrier of V
a + r is Element of the carrier of V
r - r is Element of the carrier of V
r + (- r) is Element of the carrier of V
C - (r - r) is Element of the carrier of V
- (r - r) is Element of the carrier of V
C + (- (r - r)) is Element of the carrier of V
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
C - (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
C + (- (0. V)) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {r} ) } is set
B is set
C is Element of the carrier of V
a is Element of the carrier of V
e is Element of the carrier of V
a - e is Element of the carrier of V
- e is Element of the carrier of V
a + (- e) is Element of the carrier of V
C + e is Element of the carrier of V
e - e is Element of the carrier of V
e + (- e) is Element of the carrier of V
a - (e - e) is Element of the carrier of V
- (e - e) is Element of the carrier of V
a + (- (e - e)) is Element of the carrier of V
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
a - (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
a + (- (0. V)) is Element of the carrier of V
C + r is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {r} ) } is set
f is Element of the carrier of V
u1 is Element of the carrier of V
f + u1 is Element of the carrier of V
B is set
C is Element of the carrier of V
C + r is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {r} ) } is set
a is Element of the carrier of V
a - r is Element of the carrier of V
- r is Element of the carrier of V
a + (- r) is Element of the carrier of V
r - r is Element of the carrier of V
r + (- r) is Element of the carrier of V
C + (r - r) is Element of the carrier of V
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
C + (0. V) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V125() addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
v is Element of K10( the carrier of V)
M is Element of K10( the carrier of V)
M + v is Element of K10( the carrier of V)
r is Element of the carrier of V
{r} is non empty Element of K10( the carrier of V)
M + {r} is Element of K10( the carrier of V)
B is set
C is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {r} ) } is set
a is Element of the carrier of V
e is Element of the carrier of V
a + e is Element of the carrier of V
a + r is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed V125() addLoopStr
the carrier of V is non empty set
K10( the carrier of V) is non empty set
v is Element of K10( the carrier of V)
M is Element of K10( the carrier of V)
(V,M,v) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in v ) } is set
r is Element of the carrier of V
{r} is non empty Element of K10( the carrier of V)
(V,M,{r}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {r} ) } is set
B is set
C is Element of the carrier of V
a is Element of the carrier of V
e is Element of the carrier of V
a - e is Element of the carrier of V
- e is Element of the carrier of V
a + (- e) is Element of the carrier of V
a - r is Element of the carrier of V
- r is Element of the carrier of V
a + (- r) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
M is non empty Element of K10( the carrier of V)
(V,M,M) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in M ) } is set
v is set
r is Element of the carrier of V
r - r is Element of the carrier of V
- r is Element of the carrier of V
r + (- r) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Affine Element of K10( the carrier of V)
v is Element of the carrier of V
{v} is non empty Element of K10( the carrier of V)
M + {v} is Element of K10( the carrier of V)
r is set
B is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {v} ) } is set
C is Element of the carrier of V
a is Element of the carrier of V
C + a is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
v is non empty Affine Element of K10( the carrier of V)
r is non empty Affine Element of K10( the carrier of V)
M is non empty Affine Element of K10( the carrier of V)
B is Element of the carrier of V
{B} is non empty Element of K10( the carrier of V)
v + {B} is Element of K10( the carrier of V)
C is Element of the carrier of V
{C} is non empty Element of K10( the carrier of V)
r + {C} is Element of K10( the carrier of V)
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in {B} ) } is set
a is Element of the carrier of V
e is Element of the carrier of V
a + e is Element of the carrier of V
a + B is Element of the carrier of V
- B is Element of the carrier of V
- (- B) is Element of the carrier of V
(- 1) * (- B) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in r & b₂ in {C} ) } is set
f is Element of the carrier of V
u1 is Element of the carrier of V
f + u1 is Element of the carrier of V
f + C is Element of the carrier of V
- C is Element of the carrier of V
- (- C) is Element of the carrier of V
(- 1) * (- C) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
M is non empty Affine Element of K10( the carrier of V)
v is Element of the carrier of V
{v} is non empty Element of K10( the carrier of V)
(V,M,{v}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {v} ) } is set
v - v is Element of the carrier of V
- v is Element of the carrier of V
v + (- v) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Affine Element of K10( the carrier of V)
v is Element of the carrier of V
{v} is non empty Element of K10( the carrier of V)
(V,M,{v}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {v} ) } is set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
r is non empty Affine Element of K10( the carrier of V)
r + {v} is Element of K10( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Affine Element of K10( the carrier of V)
v is Element of the carrier of V
r is Element of the carrier of V
{r} is non empty Element of K10( the carrier of V)
(V,M,{r}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {r} ) } is set
{v} is non empty Element of K10( the carrier of V)
(V,M,{v}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {v} ) } is set
B is non empty Affine Element of K10( the carrier of V)
C is non empty Affine Element of K10( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Affine Element of K10( the carrier of V)
(V,M,M) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in M ) } is set
{ (V,M,{b₁}) where b₁ is Element of the carrier of V : b₁ in M } is set
union { (V,M,{b₁}) where b₁ is Element of the carrier of V : b₁ in M } is set
v is set
r is Element of the carrier of V
B is Element of the carrier of V
C is Element of the carrier of V
B - C is Element of the carrier of V
- C is Element of the carrier of V
B + (- C) is Element of the carrier of V
{C} is non empty Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {C} ) } is set
(V,M,{C}) is Element of K10( the carrier of V)
v is set
r is set
B is Element of the carrier of V
{B} is non empty Element of K10( the carrier of V)
(V,M,{B}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {B} ) } is set
C is Element of the carrier of V
a is Element of the carrier of V
C - a is Element of the carrier of V
- a is Element of the carrier of V
C + (- a) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Affine Element of K10( the carrier of V)
{ (V,M,{b₁}) where b₁ is Element of the carrier of V : b₁ in M } is set
union { (V,M,{b₁}) where b₁ is Element of the carrier of V : b₁ in M } is set
v is Element of the carrier of V
{v} is non empty Element of K10( the carrier of V)
(V,M,{v}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {v} ) } is set
r is set
B is set
C is Element of the carrier of V
{C} is non empty Element of K10( the carrier of V)
(V,M,{C}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {C} ) } 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 V125() RLSStruct
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Affine Element of K10( the carrier of V)
(V,M,M) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in M ) } is set
r is set
v is non empty Affine Element of K10( the carrier of V)
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
B is Element of the carrier of V
{B} is non empty Element of K10( the carrier of V)
(V,M,{B}) is Element of K10( the carrier of V)
{ (b₁ - b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in {B} ) } is set
C is non empty Affine Element of K10( the carrier of V)
C + {B} is Element of K10( the carrier of V)
{ (V,M,{b₁}) where b₁ is Element of the carrier of V : b₁ in M } is set
union { (V,M,{b₁}) where b₁ is Element of the carrier of V : b₁ in M } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like Subspace of V
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
K10( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : S₁[b₁] } is set
v is Element of K10( the carrier of V)
r is Element of the carrier of V
B is Element of the carrier of V
r + B is Element of the carrier of V
C is Element of the carrier of V
a is Element of the carrier of V
C .|. B is V14() real ext-real Element of REAL
a is Element of the carrier of V
C .|. r is V14() real ext-real Element of REAL
C .|. (r + B) is V14() real ext-real Element of REAL
0 + 0 is empty V14() real ext-real non positive non negative V19() V20() V21() V22() V23() V24() V25() Element of REAL
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
r is Element of the carrier of V
r .|. (0. V) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
B is Element of the carrier of V
r * B is Element of the carrier of V
C is Element of the carrier of V
a is Element of the carrier of V
C .|. (r * B) is V14() real ext-real Element of REAL
C .|. B is V14() real ext-real Element of REAL
r * (C .|. B) is V14() real ext-real Element of REAL
r * 0 is V14() real 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 V125() strict RealUnitarySpace-like Subspace of V
the carrier of v 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 V125() strict RealUnitarySpace-like Subspace of V
the carrier of r is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Element of K10( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
{ b₁ where b₁ is Element of the carrier of V : S₁[b₁] } is set
v is Element of K10( the carrier of V)
r is Element of the carrier of V
B is Element of the carrier of V
r + B is Element of the carrier of V
C is Element of the carrier of V
a is Element of the carrier of V
C .|. B is V14() real ext-real Element of REAL
a is Element of the carrier of V
C .|. r is V14() real ext-real Element of REAL
C .|. (r + B) is V14() real ext-real Element of REAL
0 + 0 is empty V14() real ext-real non positive non negative V19() V20() V21() V22() V23() V24() V25() Element of REAL
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
r is Element of the carrier of V
r .|. (0. V) is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
B is Element of the carrier of V
r * B is Element of the carrier of V
C is Element of the carrier of V
a is Element of the carrier of V
C .|. (r * B) is V14() real ext-real Element of REAL
C .|. B is V14() real ext-real Element of REAL
r * (C .|. B) is V14() real ext-real Element of REAL
r * 0 is V14() real 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 V125() strict RealUnitarySpace-like Subspace of V
the carrier of v 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 V125() strict RealUnitarySpace-like Subspace of V
the carrier of r is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
0. V is V59(V) Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like Subspace of V
(V,M) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
v is Element of the carrier of V
v .|. (0. V) is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
the carrier of (V,M) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(0). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(V,((0). V)) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of ((Omega). V) is non empty set
the carrier of (V,((0). V)) is non empty set
M is set
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V31() V40(K11( the carrier of V, the carrier of V), the carrier of V) Element of K10(K11(K11( the carrier of V, the carrier of V), the carrier of V))
K11( the carrier of V, the carrier of V) is non empty set
K11(K11( the carrier of V, the carrier of V), the carrier of V) is non empty set
K10(K11(K11( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V31() V40(K11(REAL, the carrier of V), the carrier of V) Element of K10(K11(K11(REAL, the carrier of V), the carrier of V))
K11(REAL, the carrier of V) is set
K11(K11(REAL, the carrier of V), the carrier of V) is set
K10(K11(K11(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V31() V40(K11( the carrier of V, the carrier of V), REAL ) Element of K10(K11(K11( the carrier of V, the carrier of V),REAL))
K11(K11( the carrier of V, the carrier of V),REAL) is set
K10(K11(K11( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
v is Element of the carrier of V
r is Element of the carrier of V
the carrier of ((0). V) is non empty set
0. V is V59(V) Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
r .|. v is V14() real ext-real Element of REAL
(0. V) .|. v is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in (0). V or b₂,b₁ are_orthogonal ) } is set
M is set
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V31() V40(K11( the carrier of V, the carrier of V), the carrier of V) Element of K10(K11(K11( the carrier of V, the carrier of V), the carrier of V))
K11( the carrier of V, the carrier of V) is non empty set
K11(K11( the carrier of V, the carrier of V), the carrier of V) is non empty set
K10(K11(K11( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V31() V40(K11(REAL, the carrier of V), the carrier of V) Element of K10(K11(K11(REAL, the carrier of V), the carrier of V))
K11(REAL, the carrier of V) is set
K11(K11(REAL, the carrier of V), the carrier of V) is set
K10(K11(K11(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V31() V40(K11( the carrier of V, the carrier of V), REAL ) Element of K10(K11(K11( the carrier of V, the carrier of V),REAL))
K11(K11( the carrier of V, the carrier of V),REAL) is set
K10(K11(K11( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(V,((Omega). V)) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(0). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,((Omega). V)) is non empty set
the carrier of ((0). V) is non empty set
M is set
the carrier of V is non empty set
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in (Omega). V or b₂,b₁ are_orthogonal ) } is set
r is Element of the carrier of V
the ZeroF of V is Element of the carrier of V
the addF of V is V31() V40(K11( the carrier of V, the carrier of V), the carrier of V) Element of K10(K11(K11( the carrier of V, the carrier of V), the carrier of V))
K11( the carrier of V, the carrier of V) is non empty set
K11(K11( the carrier of V, the carrier of V), the carrier of V) is non empty set
K10(K11(K11( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V31() V40(K11(REAL, the carrier of V), the carrier of V) Element of K10(K11(K11(REAL, the carrier of V), the carrier of V))
K11(REAL, the carrier of V) is set
K11(K11(REAL, the carrier of V), the carrier of V) is set
K10(K11(K11(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V31() V40(K11( the carrier of V, the carrier of V), REAL ) Element of K10(K11(K11( the carrier of V, the carrier of V),REAL))
K11(K11( the carrier of V, the carrier of V),REAL) is set
K10(K11(K11( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
v is Element of the carrier of V
r is Element of the carrier of V
v .|. v is V14() real ext-real Element of REAL
0. V is V59(V) Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
M is set
the carrier of V is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
v is Element of the carrier of V
r is Element of the carrier of V
r .|. v is V14() real ext-real Element of REAL
r .|. (0. V) is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in (Omega). V or b₂,b₁ are_orthogonal ) } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like Subspace of V
(V,M) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
v is Element of the carrier of V
the carrier of (V,M) is non empty set
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
r is Element of the carrier of V
v .|. v is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Element of K10( the carrier of V)
(V,M) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(V,(V,M)) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,(V,M)) is non empty set
v is set
r is Element of the carrier of V
B is Element of the carrier of V
the carrier of (V,M) is non empty set
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
C is Element of the carrier of V
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in (V,M) or b₂,b₁ are_orthogonal ) } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Element of K10( the carrier of V)
v is non empty Element of K10( the carrier of V)
(V,v) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,v) is non empty set
(V,M) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,M) is non empty set
r is set
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in v or b₂,b₁ are_orthogonal ) } is set
C is Element of the carrier of V
B is Element of the carrier of V
C is Element of the carrier of V
a is Element of the carrier of V
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like Subspace of V
the carrier of M is non empty set
(V,M) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
v is non empty Element of K10( the carrier of V)
(V,v) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,M) is non empty set
the carrier of (V,v) is non empty set
r is set
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
B is Element of the carrier of V
C is Element of the carrier of V
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in v or b₂,b₁ are_orthogonal ) } is set
r is set
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in v or b₂,b₁ are_orthogonal ) } is set
B is Element of the carrier of V
C is Element of the carrier of V
{ b₁ where b₁ is Element of the carrier of V : for b₂ being Element of the carrier of V holds
( not b₂ in M or b₂,b₁ are_orthogonal ) } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
M is non empty Element of K10( the carrier of V)
(V,M) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(V,(V,M)) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(V,(V,(V,M))) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,M) is non empty set
r is Element of K10( the carrier of V)
the carrier of (V,(V,M)) is non empty set
a is Element of K10( the carrier of V)
B is non empty Element of K10( the carrier of V)
(V,B) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
(V,(V,B)) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,(V,B)) is non empty set
the carrier of (V,(V,(V,M))) is non empty set
e is non empty Element of K10( the carrier of V)
(V,e) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (V,e) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
v is Element of the carrier of V
M + v is Element of the carrier of V
||.(M + v).|| is V14() real ext-real Element of REAL
||.(M + v).|| ^2 is V14() real ext-real Element of REAL
K46(||.(M + v).||,||.(M + v).||) is V14() real ext-real set
||.M.|| is V14() real ext-real Element of REAL
||.M.|| ^2 is V14() real ext-real Element of REAL
K46(||.M.||,||.M.||) is V14() real ext-real set
M .|. v is V14() real ext-real Element of REAL
2 * (M .|. v) is V14() real ext-real Element of REAL
(||.M.|| ^2) + (2 * (M .|. v)) is V14() real ext-real Element of REAL
||.v.|| is V14() real ext-real Element of REAL
||.v.|| ^2 is V14() real ext-real Element of REAL
K46(||.v.||,||.v.||) is V14() real ext-real set
((||.M.|| ^2) + (2 * (M .|. v))) + (||.v.|| ^2) is V14() real ext-real Element of REAL
M - v is Element of the carrier of V
- v is Element of the carrier of V
M + (- v) is Element of the carrier of V
||.(M - v).|| is V14() real ext-real Element of REAL
||.(M - v).|| ^2 is V14() real ext-real Element of REAL
K46(||.(M - v).||,||.(M - v).||) is V14() real ext-real set
(||.M.|| ^2) - (2 * (M .|. v)) is V14() real ext-real Element of REAL
((||.M.|| ^2) - (2 * (M .|. v))) + (||.v.|| ^2) is V14() real ext-real Element of REAL
M .|. M is V14() real ext-real Element of REAL
(M + v) .|. (M + v) is V14() real ext-real Element of REAL
sqrt ((M + v) .|. (M + v)) is V14() real ext-real Element of REAL
sqrt (||.(M + v).|| ^2) is V14() real ext-real Element of REAL
v .|. v is V14() real ext-real Element of REAL
(M .|. M) + (2 * (M .|. v)) is V14() real ext-real Element of REAL
((M .|. M) + (2 * (M .|. v))) + (v .|. v) is V14() real ext-real Element of REAL
sqrt (M .|. M) is V14() real ext-real Element of REAL
(sqrt (M .|. M)) ^2 is V14() real ext-real Element of REAL
K46((sqrt (M .|. M)),(sqrt (M .|. M))) is V14() real ext-real set
((sqrt (M .|. M)) ^2) + (2 * (M .|. v)) is V14() real ext-real Element of REAL
(((sqrt (M .|. M)) ^2) + (2 * (M .|. v))) + (v .|. v) is V14() real ext-real Element of REAL
((||.M.|| ^2) + (2 * (M .|. v))) + (v .|. v) is V14() real ext-real Element of REAL
sqrt (v .|. v) is V14() real ext-real Element of REAL
(sqrt (v .|. v)) ^2 is V14() real ext-real Element of REAL
K46((sqrt (v .|. v)),(sqrt (v .|. v))) is V14() real ext-real set
((||.M.|| ^2) + (2 * (M .|. v))) + ((sqrt (v .|. v)) ^2) is V14() real ext-real Element of REAL
(M - v) .|. (M - v) is V14() real ext-real Element of REAL
sqrt ((M - v) .|. (M - v)) is V14() real ext-real Element of REAL
sqrt (||.(M - v).|| ^2) is V14() real ext-real Element of REAL
(M .|. M) - (2 * (M .|. v)) is V14() real ext-real Element of REAL
((M .|. M) - (2 * (M .|. v))) + (v .|. v) is V14() real ext-real Element of REAL
((sqrt (M .|. M)) ^2) - (2 * (M .|. v)) is V14() real ext-real Element of REAL
(((sqrt (M .|. M)) ^2) - (2 * (M .|. v))) + (v .|. v) is V14() real ext-real Element of REAL
((||.M.|| ^2) - (2 * (M .|. v))) + (v .|. v) is V14() real ext-real Element of REAL
((||.M.|| ^2) - (2 * (M .|. v))) + ((sqrt (v .|. v)) ^2) is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
v is Element of the carrier of V
M + v is Element of the carrier of V
||.(M + v).|| is V14() real ext-real Element of REAL
||.(M + v).|| ^2 is V14() real ext-real Element of REAL
K46(||.(M + v).||,||.(M + v).||) is V14() real ext-real set
||.M.|| is V14() real ext-real Element of REAL
||.M.|| ^2 is V14() real ext-real Element of REAL
K46(||.M.||,||.M.||) is V14() real ext-real set
||.v.|| is V14() real ext-real Element of REAL
||.v.|| ^2 is V14() real ext-real Element of REAL
K46(||.v.||,||.v.||) is V14() real ext-real set
(||.M.|| ^2) + (||.v.|| ^2) is V14() real ext-real Element of REAL
M .|. v is V14() real ext-real Element of REAL
2 * (M .|. v) is V14() real ext-real Element of REAL
(||.M.|| ^2) + (2 * (M .|. v)) is V14() real ext-real Element of REAL
((||.M.|| ^2) + (2 * (M .|. v))) + (||.v.|| ^2) is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
v is Element of the carrier of V
M + v is Element of the carrier of V
||.(M + v).|| is V14() real ext-real Element of REAL
||.(M + v).|| ^2 is V14() real ext-real Element of REAL
K46(||.(M + v).||,||.(M + v).||) is V14() real ext-real set
M - v is Element of the carrier of V
- v is Element of the carrier of V
M + (- v) is Element of the carrier of V
||.(M - v).|| is V14() real ext-real Element of REAL
||.(M - v).|| ^2 is V14() real ext-real Element of REAL
K46(||.(M - v).||,||.(M - v).||) is V14() real ext-real set
(||.(M + v).|| ^2) + (||.(M - v).|| ^2) is V14() real ext-real Element of REAL
||.M.|| is V14() real ext-real Element of REAL
||.M.|| ^2 is V14() real ext-real Element of REAL
K46(||.M.||,||.M.||) is V14() real ext-real set
2 * (||.M.|| ^2) is V14() real ext-real Element of REAL
||.v.|| is V14() real ext-real Element of REAL
||.v.|| ^2 is V14() real ext-real Element of REAL
K46(||.v.||,||.v.||) is V14() real ext-real set
2 * (||.v.|| ^2) is V14() real ext-real Element of REAL
(2 * (||.M.|| ^2)) + (2 * (||.v.|| ^2)) is V14() real ext-real Element of REAL
M .|. v is V14() real ext-real Element of REAL
2 * (M .|. v) is V14() real ext-real Element of REAL
(||.M.|| ^2) + (2 * (M .|. v)) is V14() real ext-real Element of REAL
((||.M.|| ^2) + (2 * (M .|. v))) + (||.v.|| ^2) is V14() real ext-real Element of REAL
(((||.M.|| ^2) + (2 * (M .|. v))) + (||.v.|| ^2)) + (||.(M - v).|| ^2) is V14() real ext-real Element of REAL
(||.M.|| ^2) - (2 * (M .|. v)) is V14() real ext-real Element of REAL
((||.M.|| ^2) - (2 * (M .|. v))) + (||.v.|| ^2) is V14() real ext-real Element of REAL
(((||.M.|| ^2) + (2 * (M .|. v))) + (||.v.|| ^2)) + (((||.M.|| ^2) - (2 * (M .|. v))) + (||.v.|| ^2)) is V14() real ext-real Element of REAL
(||.M.|| ^2) + (||.M.|| ^2) is V14() real ext-real Element of REAL
((||.M.|| ^2) + (||.M.|| ^2)) + (2 * (||.v.|| ^2)) is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
{ b₁ where b₁ is Element of the carrier of V : b₁ .|. M = 0 } is set
r is set
B is Element of the carrier of V
B .|. M is V14() real ext-real Element of REAL
K10( the carrier of V) is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
(0. V) .|. M is V14() real ext-real Element of REAL
r is Element of K10( the carrier of V)
B is non empty Element of K10( the carrier of V)
C is Element of the carrier of V
a is Element of the carrier of V
e is V14() real ext-real Element of REAL
1 - e is V14() real ext-real Element of REAL
(1 - e) * C is Element of the carrier of V
e * a is Element of the carrier of V
((1 - e) * C) + (e * a) is Element of the carrier of V
f is Element of the carrier of V
f .|. M is V14() real ext-real Element of REAL
u1 is Element of the carrier of V
u1 .|. M is V14() real ext-real Element of REAL
(1 - e) * u1 is Element of the carrier of V
e * f is Element of the carrier of V
((1 - e) * u1) + (e * f) is Element of the carrier of V
(((1 - e) * u1) + (e * f)) .|. M is V14() real ext-real Element of REAL
((1 - e) * u1) .|. M is V14() real ext-real Element of REAL
(e * f) .|. M is V14() real ext-real Element of REAL
(((1 - e) * u1) .|. M) + ((e * f) .|. M) is V14() real ext-real Element of REAL
(1 - e) * (u1 .|. M) is V14() real ext-real Element of REAL
((1 - e) * (u1 .|. M)) + ((e * f) .|. M) is V14() real ext-real Element of REAL
e * 0 is V14() real ext-real Element of REAL
C is non empty Affine Element of K10( the carrier of V)
Lin C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() strict RealUnitarySpace-like Subspace of V
the carrier of (Lin C) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
M is Element of K10(K10( the carrier of V))
M is Element of K10(K10( the carrier of V))
v is Element of K10(K10( the carrier of V))
r is Element of K10( the carrier of V)
B is Element of the carrier of V
B is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
r is V14() real ext-real Element of REAL
Ball (M,v) is Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
Ball (M,r) is Element of K10( the carrier of V)
B is Element of the carrier of V
dist (M,B) is V14() real ext-real Element of REAL
v + r is V14() real ext-real Element of REAL
(dist (M,B)) + v is V14() real ext-real Element of REAL
(v + r) - v is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
Ball (M,v) is Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
v is Element of the carrier of V
M is Element of the carrier of V
r is V14() real ext-real Element of REAL
Ball (M,r) is Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
dist (M,v) is V14() real ext-real Element of REAL
r - (dist (M,v)) is V14() real ext-real Element of REAL
Ball (v,(r - (dist (M,v)))) is Element of K10( the carrier of V)
C is Element of the carrier of V
dist (v,C) is V14() real ext-real Element of REAL
(dist (M,v)) + (dist (v,C)) is V14() real ext-real Element of REAL
dist (M,C) is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
v is Element of the carrier of V
M is Element of the carrier of V
r is Element of the carrier of V
B is V14() real ext-real Element of REAL
Ball (M,B) is Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
C is V14() real ext-real Element of REAL
Ball (r,C) is Element of K10( the carrier of V)
(Ball (M,B)) /\ (Ball (r,C)) is Element of K10( the carrier of V)
a is V14() real ext-real Element of REAL
Ball (v,a) is Element of K10( the carrier of V)
e is V14() real ext-real Element of REAL
Ball (v,e) is Element of K10( the carrier of V)
min (a,e) is V14() real ext-real Element of REAL
f is V14() real ext-real Element of REAL
Ball (v,f) is Element of K10( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
Ball (M,v) is Element of K10( the carrier of V)
r is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
M is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
(V) is Element of K10(K10( the carrier of V))
K10(K10( the carrier of V)) is non empty set
M is Element of K10( the carrier of V)
v is Element of K10( the carrier of V)
M /\ v is Element of K10( the carrier of V)
r is Element of the carrier of V
B is V14() real ext-real Element of REAL
Ball (r,B) is Element of K10( the carrier of V)
C is V14() real ext-real Element of REAL
Ball (r,C) is Element of K10( the carrier of V)
min (B,C) is V14() real ext-real Element of REAL
a is V14() real ext-real Element of REAL
Ball (r,a) is Element of K10( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
(V) is Element of K10(K10( the carrier of V))
M is Element of K10(K10( the carrier of V))
union M is Element of K10( the carrier of V)
v is Element of the carrier of V
r is set
B is Element of K10( the carrier of V)
C is V14() real ext-real Element of REAL
Ball (v,C) is Element of K10( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of TopStruct(# the carrier of V,(V) #) is non empty set
K10( the carrier of TopStruct(# the carrier of V,(V) #)) is non empty set
the topology of TopStruct(# the carrier of V,(V) #) is Element of K10(K10( the carrier of TopStruct(# the carrier of V,(V) #)))
K10(K10( the carrier of TopStruct(# the carrier of V,(V) #))) is non empty set
v is Element of K10( the carrier of TopStruct(# the carrier of V,(V) #))
r is Element of K10( the carrier of TopStruct(# the carrier of V,(V) #))
v /\ r is Element of K10( the carrier of TopStruct(# the carrier of V,(V) #))
v is Element of K10(K10( the carrier of TopStruct(# the carrier of V,(V) #)))
union v is Element of K10( the carrier of TopStruct(# the carrier of V,(V) #))
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is TopSpace-like TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is non empty TopSpace-like TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of (V) is non empty set
K10( the carrier of (V)) is non empty set
[#] V is non empty non proper Element of K10( the carrier of V)
M is Element of K10( the carrier of (V))
[#] (V) is non empty non proper open closed Element of K10( the carrier of (V))
the carrier of TopStruct(# the carrier of V,(V) #) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is non empty TopSpace-like TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of (V) is non empty set
K10( the carrier of (V)) is non empty set
M is Element of K10( the carrier of (V))
{} V is empty proper V19() V20() V21() V22() V23() V24() V25() Element of K10( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
Sphere (M,v) is Element of K10( the carrier of V)
r is set
{ b₁ where b₁ is Element of the carrier of V : ||.(M - b₁).|| = v } is set
B is Element of the carrier of V
M - B is Element of the carrier of V
- B is Element of the carrier of V
M + (- B) is Element of the carrier of V
||.(M - B).|| is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
Sphere (M,v) is Element of K10( the carrier of V)
NonZero V is Element of K10( the carrier of V)
[#] V is non empty non proper Element of K10( the carrier of V)
{(0. V)} is non empty set
([#] V) \ {(0. V)} is Element of K10( the carrier of V)
r is set
B is Element of the carrier of V
r is Element of the carrier of V
r is Element of the carrier of V
||.r.|| is V14() real ext-real Element of REAL
1 / ||.r.|| is V14() real ext-real Element of REAL
v * (1 / ||.r.||) is V14() real ext-real Element of REAL
(v * (1 / ||.r.||)) * r is Element of the carrier of V
M - ((v * (1 / ||.r.||)) * r) is Element of the carrier of V
- ((v * (1 / ||.r.||)) * r) is Element of the carrier of V
M + (- ((v * (1 / ||.r.||)) * r)) is Element of the carrier of V
||.(M - ((v * (1 / ||.r.||)) * r)).|| is V14() real ext-real Element of REAL
||.(- ((v * (1 / ||.r.||)) * r)).|| is V14() real ext-real Element of REAL
||.((v * (1 / ||.r.||)) * r).|| is V14() real ext-real Element of REAL
abs (v * (1 / ||.r.||)) is V14() real ext-real Element of REAL
(abs (v * (1 / ||.r.||))) * ||.r.|| is V14() real ext-real Element of REAL
(v * (1 / ||.r.||)) * ||.r.|| is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : ||.(M - b₁).|| = v } is set
||.M.|| is V14() real ext-real Element of REAL
v / ||.M.|| is V14() real ext-real Element of REAL
1 - (v / ||.M.||) is V14() real ext-real Element of REAL
(1 - (v / ||.M.||)) * M is Element of the carrier of V
M - ((1 - (v / ||.M.||)) * M) is Element of the carrier of V
- ((1 - (v / ||.M.||)) * M) is Element of the carrier of V
M + (- ((1 - (v / ||.M.||)) * M)) is Element of the carrier of V
||.(M - ((1 - (v / ||.M.||)) * M)).|| is V14() real ext-real Element of REAL
1 * M is Element of the carrier of V
(1 * M) - ((1 - (v / ||.M.||)) * M) is Element of the carrier of V
(1 * M) + (- ((1 - (v / ||.M.||)) * M)) is Element of the carrier of V
||.((1 * M) - ((1 - (v / ||.M.||)) * M)).|| is V14() real ext-real Element of REAL
1 - (1 - (v / ||.M.||)) is V14() real ext-real Element of REAL
(1 - (1 - (v / ||.M.||))) * M is Element of the carrier of V
||.((1 - (1 - (v / ||.M.||))) * M).|| is V14() real ext-real Element of REAL
abs (v / ||.M.||) is V14() real ext-real Element of REAL
(abs (v / ||.M.||)) * ||.M.|| is V14() real ext-real Element of REAL
(v / ||.M.||) * ||.M.|| is V14() real ext-real Element of REAL
||.M.|| / ||.M.|| is V14() real ext-real Element of REAL
v / (||.M.|| / ||.M.||) is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : ||.(M - b₁).|| = v } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
Ball (M,v) is Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
r is set
{ b₁ where b₁ is Element of the carrier of V : not v <= ||.(M - b₁).|| } is set
B is Element of the carrier of V
M - B is Element of the carrier of V
- B is Element of the carrier of V
M + (- B) is Element of the carrier of V
||.(M - B).|| is V14() real 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 V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
Ball (M,v) is Element of K10( the carrier of V)
r is Element of the carrier of V
M - r is Element of the carrier of V
- r is Element of the carrier of V
M + (- r) is Element of the carrier of V
||.(M - r).|| is V14() real ext-real Element of REAL
(0. V) - (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
(0. V) + (- (0. V)) is Element of the carrier of V
||.((0. V) - (0. V)).|| is V14() real ext-real Element of REAL
||.(0. V).|| is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : not v <= ||.(M - b₁).|| } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
0. V is V59(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
M is Element of the carrier of V
v is V14() real ext-real Element of REAL
Ball (M,v) is Element of K10( the carrier of V)
r is V14() real ext-real set
NonZero V is Element of K10( the carrier of V)
[#] V is non empty non proper Element of K10( the carrier of V)
{(0. V)} is non empty set
([#] V) \ {(0. V)} is Element of K10( the carrier of V)
C is set
a is Element of the carrier of V
||.a.|| is V14() real ext-real Element of REAL
B is V14() real ext-real Element of REAL
B / ||.a.|| is V14() real ext-real Element of REAL
(B / ||.a.||) * a is Element of the carrier of V
f is Element of the carrier of V
||.f.|| is V14() real ext-real Element of REAL
abs (B / ||.a.||) is V14() real ext-real Element of REAL
(abs (B / ||.a.||)) * ||.a.|| is V14() real ext-real Element of REAL
(B / ||.a.||) * ||.a.|| is V14() real ext-real Element of REAL
||.a.|| / ||.a.|| is V14() real ext-real Element of REAL
B / (||.a.|| / ||.a.||) is V14() real ext-real Element of REAL
C is Element of the carrier of V
||.C.|| is V14() real ext-real Element of REAL
C is Element of the carrier of V
||.C.|| is V14() real ext-real Element of REAL
M - C is Element of the carrier of V
- C is Element of the carrier of V
M + (- C) is Element of the carrier of V
||.(M - C).|| is V14() real ext-real Element of REAL
||.(- C).|| is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : not v <= ||.(M - b₁).|| } is set
||.M.|| is V14() real ext-real Element of REAL
B is V14() real ext-real Element of REAL
B / ||.M.|| is V14() real ext-real Element of REAL
1 - (B / ||.M.||) is V14() real ext-real Element of REAL
(1 - (B / ||.M.||)) * M is Element of the carrier of V
M - ((1 - (B / ||.M.||)) * M) is Element of the carrier of V
- ((1 - (B / ||.M.||)) * M) is Element of the carrier of V
M + (- ((1 - (B / ||.M.||)) * M)) is Element of the carrier of V
||.(M - ((1 - (B / ||.M.||)) * M)).|| is V14() real ext-real Element of REAL
1 * M is Element of the carrier of V
(1 * M) - ((1 - (B / ||.M.||)) * M) is Element of the carrier of V
(1 * M) + (- ((1 - (B / ||.M.||)) * M)) is Element of the carrier of V
||.((1 * M) - ((1 - (B / ||.M.||)) * M)).|| is V14() real ext-real Element of REAL
1 - (1 - (B / ||.M.||)) is V14() real ext-real Element of REAL
(1 - (1 - (B / ||.M.||))) * M is Element of the carrier of V
||.((1 - (1 - (B / ||.M.||))) * M).|| is V14() real ext-real Element of REAL
abs (B / ||.M.||) is V14() real ext-real Element of REAL
(abs (B / ||.M.||)) * ||.M.|| is V14() real ext-real Element of REAL
(B / ||.M.||) * ||.M.|| is V14() real ext-real Element of REAL
||.M.|| / ||.M.|| is V14() real ext-real Element of REAL
B / (||.M.|| / ||.M.||) is V14() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : not v <= ||.(M - b₁).|| } is set
C is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
(V) is non empty TopSpace-like TopStruct
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of (V) is non empty set
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(M) is non empty TopSpace-like TopStruct
the carrier of M is non empty set
(M) is Element of K10(K10( the carrier of M))
K10( the carrier of M) is non empty set
K10(K10( the carrier of M)) is non empty set
TopStruct(# the carrier of M,(M) #) is non empty strict TopStruct
the topology of (M) is non empty Element of K10(K10( the carrier of (M)))
the carrier of (M) is non empty set
K10( the carrier of (M)) is non empty set
K10(K10( the carrier of (M))) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is non empty TopSpace-like TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of (V) is non empty set
K10( the carrier of (V)) is non empty set
M is Element of K10( the carrier of (V))
v is V14() real ext-real Element of REAL
r is Element of the carrier of V
Ball (r,v) is Element of K10( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is non empty TopSpace-like TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of (V) is non empty set
K10( the carrier of (V)) is non empty set
M is Element of K10( the carrier of (V))
the topology of (V) is non empty Element of K10(K10( the carrier of (V)))
K10(K10( the carrier of (V))) is non empty set
v is Element of the carrier of V
the topology of (V) is non empty Element of K10(K10( the carrier of (V)))
K10(K10( the carrier of (V))) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
M is Element of the carrier of V
v is Element of the carrier of V
r is V14() real ext-real Element of REAL
Ball (M,r) is Element of K10( the carrier of V)
K10( the carrier of V) is non empty set
B is V14() real ext-real Element of REAL
Ball (v,B) is Element of K10( the carrier of V)
(Ball (M,r)) \/ (Ball (v,B)) is Element of K10( the carrier of V)
abs r is V14() real ext-real Element of REAL
abs B is V14() real ext-real Element of REAL
(abs r) + (abs B) is V14() real ext-real Element of REAL
dist (M,v) is V14() real ext-real Element of REAL
((abs r) + (abs B)) + (dist (M,v)) is V14() real ext-real Element of REAL
C is Element of the carrier of V
a is V14() real ext-real Element of REAL
Ball (C,a) is Element of K10( the carrier of V)
e is set
f is Element of the carrier of V
dist (C,f) is V14() real ext-real Element of REAL
r + 0 is V14() real ext-real Element of REAL
r - r is V14() real ext-real Element of REAL
(dist (C,f)) - a is V14() real ext-real Element of REAL
0 + a is V14() real ext-real Element of REAL
((dist (C,f)) - a) + a is V14() real ext-real Element of REAL
f is Element of the carrier of V
dist (v,f) is V14() real ext-real Element of REAL
B - B is V14() real ext-real Element of REAL
(dist (v,f)) - (abs B) is V14() real ext-real Element of REAL
0 + (abs B) is V14() real ext-real Element of REAL
((dist (v,f)) - (abs B)) + (abs B) is V14() real ext-real Element of REAL
(dist (M,v)) + (dist (v,f)) is V14() real ext-real Element of REAL
((dist (M,v)) + (dist (v,f))) - (dist (v,f)) is V14() real ext-real Element of REAL
dist (C,f) is V14() real ext-real Element of REAL
(dist (C,f)) - (abs B) is V14() real ext-real Element of REAL
(dist (M,v)) - 0 is V14() real ext-real Element of REAL
((dist (C,f)) - (abs B)) - (abs r) is V14() real ext-real Element of REAL
(dist (C,f)) - ((abs r) + (abs B)) is V14() real ext-real Element of REAL
((dist (C,f)) - ((abs r) + (abs B))) + ((abs r) + (abs B)) is V14() real ext-real Element of REAL
f is Element of the carrier of V
f is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is non empty TopSpace-like TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of (V) is non empty set
K10( the carrier of (V)) is non empty set
M is Element of K10( the carrier of (V))
v is Element of the carrier of V
r is V14() real ext-real Element of REAL
cl_Ball (v,r) is Element of K10( the carrier of V)
M ` is Element of K10( the carrier of (V))
the carrier of (V) \ M is set
B is set
C is Element of the carrier of V
dist (C,v) is V14() real ext-real Element of REAL
(dist (C,v)) - r is V14() real ext-real Element of REAL
Ball (C,((dist (C,v)) - r)) is Element of K10( the carrier of V)
a is Element of K10( the carrier of (V))
e is set
f is Element of the carrier of V
dist (C,f) is V14() real ext-real Element of REAL
dist (f,v) is V14() real ext-real Element of REAL
(dist (C,f)) + (dist (f,v)) is V14() real ext-real Element of REAL
((dist (C,f)) + (dist (f,v))) - r is V14() real ext-real Element of REAL
(((dist (C,f)) + (dist (f,v))) - r) - (dist (C,f)) is V14() real ext-real Element of REAL
(dist (C,f)) - (dist (C,f)) is V14() real ext-real Element of REAL
((dist (C,f)) - (dist (C,f))) + (dist (f,v)) is V14() real ext-real Element of REAL
(((dist (C,f)) - (dist (C,f))) + (dist (f,v))) - r is V14() real ext-real Element of REAL
dist (v,C) is V14() real ext-real Element of REAL
r - r is V14() real ext-real Element of REAL
C is Element of K10( the carrier of (V))
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V125() RealUnitarySpace-like UNITSTR
(V) is non empty TopSpace-like TopStruct
the carrier of V is non empty set
(V) is Element of K10(K10( the carrier of V))
K10( the carrier of V) is non empty set
K10(K10( the carrier of V)) is non empty set
TopStruct(# the carrier of V,(V) #) is non empty strict TopStruct
the carrier of (V) is non empty set
K10( the carrier of (V)) is non empty set
M is Element of K10( the carrier of (V))
v is Element of the carrier of V
r is V14() real ext-real Element of REAL
Sphere (v,r) is Element of K10( the carrier of V)
cl_Ball (v,r) is Element of K10( the carrier of V)
Ball (v,r) is Element of K10( the carrier of V)
M ` is Element of K10( the carrier of (V))
the carrier of (V) \ M is set
B is Element of K10( the carrier of (V))
B ` is Element of K10( the carrier of (V))
the carrier of (V) \ B is set
C is Element of K10( the carrier of (V))
(B `) \/ C is Element of K10( the carrier of (V))
a is set
e is Element of the carrier of V
dist (e,v) is V14() real ext-real Element of REAL
(cl_Ball (v,r)) ` is Element of K10( the carrier of V)
the carrier of V \ (cl_Ball (v,r)) is set
a is set
e is Element of the carrier of V
dist (e,v) is V14() real ext-real Element of REAL