:: 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

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

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

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

C is set

{ (b

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

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

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

(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

e is set

f is Element of the carrier of V

{ (b

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

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

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

{ H

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

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 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

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

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

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 is set

C is Element of the carrier of V

{ (b

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 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

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

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

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

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

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 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

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

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

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

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

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

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

{v} is non empty Element of K10( the carrier of V)

(V,M,{v}) is Element of K10( the carrier of V)

{ (b

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

{ (V,M,{b

union { (V,M,{b

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

(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

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

union { (V,M,{b

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

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

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

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

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

union { (V,M,{b

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

( not b

K10( the carrier of V) is non empty set

{ b

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

( not b

{ b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

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

( not b

C is Element of the carrier of V

{ b

( not b

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

( not b

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

( not b

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

( not b

B is Element of the carrier of V

C is Element of the carrier of V

{ b

( not b

r is set

{ b

( not b

B is Element of the carrier of V

C is Element of the carrier of V

{ b

( not b

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

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

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

||.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

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

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

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 /