:: RLVECT_3 semantic presentation

REAL is non empty non trivial non finite set

bool REAL is non empty set

bool NAT is non empty set
bool NAT is non empty set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set

- 1 is V22() V23() V24() Element of REAL

the carrier of V is non empty set
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set

B (#) (A ^ B) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

(B (#) A) ^ (B (#) B) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len ((B (#) A) ^ (B (#) B)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT

(len (B (#) A)) + (len (B (#) B)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT

(len A) + (len (B (#) B)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT

dom ((B (#) A) ^ (B (#) B)) is set
dom (B (#) A) is set
dom A is set
dom (A ^ B) is set
A /. l is Element of the carrier of V
A . l is set
(A ^ B) . l is set
(A ^ B) /. l is Element of the carrier of V
((B (#) A) ^ (B (#) B)) . l is set
(B (#) A) . l is set
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V
dom (B (#) B) is set
dom (A ^ B) is set

(len (B (#) A)) + x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT

(len (B (#) A)) + x is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom B is set
B /. x is Element of the carrier of V
B . x is set
(A ^ B) . l is set
(A ^ B) /. l is Element of the carrier of V
((B (#) A) ^ (B (#) B)) . l is set
(B (#) B) . x is set
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V
dom (B (#) A) is set
dom (B (#) B) is set
((B (#) A) ^ (B (#) B)) . l is set
(A ^ B) /. l is Element of the carrier of V
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V
((B (#) A) ^ (B (#) B)) . l is set
(A ^ B) /. l is Element of the carrier of V
B . ((A ^ B) /. l) is V22() V23() V24() Element of REAL
(B . ((A ^ B) /. l)) * ((A ^ B) /. l) is Element of the carrier of V

the carrier of V is non empty set

Sum A is Element of the carrier of V

Sum (A + B) is Element of the carrier of V
Sum B is Element of the carrier of V
(Sum A) + (Sum B) is Element of the carrier of V
Carrier (A + B) is finite Element of bool the carrier of V
bool the carrier of V is non empty set
{ b1 where b1 is Element of the carrier of V : not (A + B) . b1 = 0 } is set

rng B is set
(A + B) (#) B is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((A + B) (#) B) is Element of the carrier of V
Carrier A is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0 } is set
(Carrier (A + B)) \/ () is finite Element of bool the carrier of V
Carrier B is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0 } is set
((Carrier (A + B)) \/ ()) \/ () is finite Element of bool the carrier of V
(((Carrier (A + B)) \/ ()) \/ ()) \ (Carrier (A + B)) is finite Element of bool the carrier of V

rng l is set

() \/ () is finite Element of bool the carrier of V
(Carrier (A + B)) \/ (() \/ ()) is finite Element of bool the carrier of V
rng x is set
(rng B) /\ (rng x) is set
the Element of (rng B) /\ (rng x) is Element of (rng B) /\ (rng x)

(A + B) (#) x is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len ((A + B) (#) x) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT

dom x is set
x /. f is Element of the carrier of V
x . f is set
dom ((A + B) (#) x) is set
((A + B) (#) x) . f is set
(A + B) . (x /. f) is V22() V23() V24() Element of REAL
((A + B) . (x /. f)) * (x /. f) is Element of the carrier of V
0 * (x /. f) is Element of the carrier of V
Sum ((A + B) (#) x) is Element of the carrier of V
Sum x is Element of the carrier of V
0 * (Sum x) is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
(A + B) (#) (B ^ x) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(((Carrier (A + B)) \/ ()) \/ ()) \ () is finite Element of bool the carrier of V

rng g is set

Sum (A (#) g) is Element of the carrier of V

rng g is set

Sum ((A + B) (#) (B ^ x)) is Element of the carrier of V
((A + B) (#) B) ^ ((A + B) (#) x) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum (((A + B) (#) B) ^ ((A + B) (#) x)) is Element of the carrier of V
(Sum ((A + B) (#) B)) + (0. V) is Element of the carrier of V
(((Carrier (A + B)) \/ ()) \/ ()) \ () is finite Element of bool the carrier of V

rng g is set

Sum (B (#) g) is Element of the carrier of V

rng v is set

rng q is set
(rng g) /\ (rng q) is set
the Element of (rng g) /\ (rng q) is Element of (rng g) /\ (rng q)
B (#) (g ^ q) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
(Carrier (A + B)) \/ () is finite Element of bool the carrier of V
() \/ ((Carrier (A + B)) \/ ()) is finite Element of bool the carrier of V
rng (g ^ g) is set
rng g is set
(rng g) \/ (rng g) is set
() \/ (((Carrier (A + B)) \/ ()) \/ ()) is finite Element of bool the carrier of V

dom q is set
q /. g is Element of the carrier of V
q . g is set
dom (B (#) q) is set
(B (#) q) . g is set
B . (q /. g) is V22() V23() V24() Element of REAL
(B . (q /. g)) * (q /. g) is Element of the carrier of V
0 * (q /. g) is Element of the carrier of V
Sum (B (#) q) is Element of the carrier of V
Sum q is Element of the carrier of V
0 * (Sum q) is Element of the carrier of V
Sum (B (#) (g ^ q)) is Element of the carrier of V
(B (#) g) ^ (B (#) q) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((B (#) g) ^ (B (#) q)) is Element of the carrier of V
(Sum (B (#) g)) + (0. V) is Element of the carrier of V
A (#) (g ^ g) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

dom P is set
Seg (len (B ^ x)) is Element of bool NAT

dom g is set
g /. P is Element of the carrier of V
g . P is set
dom (A (#) g) is set
(A (#) g) . P is set
A . (g /. P) is V22() V23() V24() Element of REAL
(A . (g /. P)) * (g /. P) is Element of the carrier of V
0 * (g /. P) is Element of the carrier of V
Sum (A (#) g) is Element of the carrier of V
Sum g is Element of the carrier of V
0 * (Sum g) is Element of the carrier of V
Sum (A (#) (g ^ g)) is Element of the carrier of V
(A (#) g) ^ (A (#) g) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum ((A (#) g) ^ (A (#) g)) is Element of the carrier of V
(Sum (A (#) g)) + (0. V) is Element of the carrier of V
rng (B ^ x) is set
(rng B) \/ (rng x) is set
(Carrier (A + B)) \/ (((Carrier (A + B)) \/ ()) \/ ()) is finite Element of bool the carrier of V
(rng g) /\ (rng g) is set
the Element of (rng g) /\ (rng g) is Element of (rng g) /\ (rng g)

P is set
dom (g ^ g) is set

(g ^ g) . P is set
P . P is set
(B ^ x) . (P . P) is set
(B ^ x) <- ((g ^ g) . P) is set
(B ^ x) . ((B ^ x) <- ((g ^ g) . P)) is set
(g ^ g) . P is set
P . P is set
(B ^ x) . (P . P) is set
rng P is set
P is set
P is set
P . P is set

(g ^ g) . Fp is set
P . Fp is set
(B ^ x) <- ((g ^ g) . Fp) is set
dom (B ^ x) is set
P is set
P . P is set
dom (B ^ x) is set
Seg (len P) is Element of bool NAT
Seg (len P) is Element of bool NAT
P (#) (B ^ x) is Relation-like Function-like set
(B ^ x) " is Relation-like Function-like set
(g ^ g) (#) ((B ^ x) ") is Relation-like Function-like set
P is set
dom ((B ^ x) ") is set
rng ((g ^ g) (#) ((B ^ x) ")) is set
rng ((B ^ x) ") is set
(B ^ x) (#) ((B ^ x) ") is Relation-like Function-like set
P (#) ((B ^ x) (#) ((B ^ x) ")) is Relation-like Function-like set
id (dom (B ^ x)) is Relation-like dom (B ^ x) -defined dom (B ^ x) -valued Function-like one-to-one total Element of bool [:(dom (B ^ x)),(dom (B ^ x)):]
[:(dom (B ^ x)),(dom (B ^ x)):] is set
bool [:(dom (B ^ x)),(dom (B ^ x)):] is non empty set
P (#) (id (dom (B ^ x))) is Relation-like Function-like set
[:(Seg (len (B ^ x))),(Seg (len (B ^ x))):] is set
bool [:(Seg (len (B ^ x))),(Seg (len (B ^ x))):] is non empty set
P is Relation-like Seg (len (B ^ x)) -defined Seg (len (B ^ x)) -valued Function-like quasi_total Element of bool [:(Seg (len (B ^ x))),(Seg (len (B ^ x))):]
len ((A + B) (#) (B ^ x)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom ((A + B) (#) (B ^ x)) is set
P is Relation-like Seg (len (B ^ x)) -defined Seg (len (B ^ x)) -valued Function-like quasi_total bijective Element of bool [:(Seg (len (B ^ x))),(Seg (len (B ^ x))):]
((A + B) (#) (B ^ x)) * P is Relation-like Seg (len (B ^ x)) -defined the carrier of V -valued Function-like Element of bool [:(Seg (len (B ^ x))), the carrier of V:]
[:(Seg (len (B ^ x))), the carrier of V:] is set
bool [:(Seg (len (B ^ x))), the carrier of V:] is non empty set
len (A (#) (g ^ g)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT

dom R is set
Seg (len (g ^ q)) is Element of bool NAT
rng (g ^ q) is set
(rng g) \/ (rng q) is set
() \/ (((Carrier (A + B)) \/ ()) \/ ()) is finite Element of bool the carrier of V
R is set

(g ^ g) . R is set
R . R is set
(g ^ q) . (R . R) is set
(g ^ q) <- ((g ^ g) . R) is set
(g ^ q) . ((g ^ q) <- ((g ^ g) . R)) is set
(g ^ g) . R is set
R . R is set
(g ^ q) . (R . R) is set
rng R is set
R is set
R is set
R . R is set

(g ^ g) . Hp is set
R . Hp is set
(g ^ q) <- ((g ^ g) . Hp) is set
dom (g ^ q) is set
R is set
R . R is set
dom (g ^ q) is set
Seg (len R) is Element of bool NAT
Seg (len R) is Element of bool NAT
R (#) (g ^ q) is Relation-like Function-like set
(g ^ q) " is Relation-like Function-like set
(g ^ g) (#) ((g ^ q) ") is Relation-like Function-like set
R is set
dom ((g ^ q) ") is set
rng ((g ^ g) (#) ((g ^ q) ")) is set
rng ((g ^ q) ") is set
(g ^ q) (#) ((g ^ q) ") is Relation-like Function-like set
R (#) ((g ^ q) (#) ((g ^ q) ")) is Relation-like Function-like set
id (dom (g ^ q)) is Relation-like dom (g ^ q) -defined dom (g ^ q) -valued Function-like one-to-one total Element of bool [:(dom (g ^ q)),(dom (g ^ q)):]
[:(dom (g ^ q)),(dom (g ^ q)):] is set
bool [:(dom (g ^ q)),(dom (g ^ q)):] is non empty set
R (#) (id (dom (g ^ q))) is Relation-like Function-like set
[:(Seg (len (g ^ q))),(Seg (len (g ^ q))):] is set
bool [:(Seg (len (g ^ q))),(Seg (len (g ^ q))):] is non empty set
R is Relation-like Seg (len (g ^ q)) -defined Seg (len (g ^ q)) -valued Function-like quasi_total Element of bool [:(Seg (len (g ^ q))),(Seg (len (g ^ q))):]
len (B (#) (g ^ q)) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom (B (#) (g ^ q)) is set
R is Relation-like Seg (len (g ^ q)) -defined Seg (len (g ^ q)) -valued Function-like quasi_total bijective Element of bool [:(Seg (len (g ^ q))),(Seg (len (g ^ q))):]
(B (#) (g ^ q)) * R is Relation-like Seg (len (g ^ q)) -defined the carrier of V -valued Function-like Element of bool [:(Seg (len (g ^ q))), the carrier of V:]
[:(Seg (len (g ^ q))), the carrier of V:] is set
bool [:(Seg (len (g ^ q))), the carrier of V:] is non empty set

dom I is set
Seg (len (g ^ g)) is Element of bool NAT

I . I is set
(A (#) (g ^ g)) /. I is Element of the carrier of V
Hp /. I is Element of the carrier of V
((A (#) (g ^ g)) /. I) + (Hp /. I) is Element of the carrier of V
rng I is set
I is set
x is set
I . x is set

I . k is set
(A (#) (g ^ g)) /. k is Element of the carrier of V
Hp /. k is Element of the carrier of V
((A (#) (g ^ g)) /. k) + (Hp /. k) is Element of the carrier of V

x is set
dom I is set
dom Hp is set

dom R is set
R . k is set
(g ^ g) /. k is Element of the carrier of V

(g ^ q) . j is set
(g ^ g) . k is set
(B (#) (g ^ q)) . j is set
B . ((g ^ g) /. k) is V22() V23() V24() Element of REAL
(B . ((g ^ g) /. k)) * ((g ^ g) /. k) is Element of the carrier of V
dom P is set
P . k is set
dom Fp is set
Fp . k is set
((A + B) (#) (B ^ x)) . (P . k) is set
Hp /. k is Element of the carrier of V
((B (#) (g ^ q)) * R) . k is set
(B (#) (g ^ q)) . (R . k) is set
dom (A (#) (g ^ g)) is set

(B ^ x) . l is set
((A + B) (#) (B ^ x)) . l is set
(A + B) . ((g ^ g) /. k) is V22() V23() V24() Element of REAL
((A + B) . ((g ^ g) /. k)) * ((g ^ g) /. k) is Element of the carrier of V
A . ((g ^ g) /. k) is V22() V23() V24() Element of REAL
(A . ((g ^ g) /. k)) + (B . ((g ^ g) /. k)) is V22() V23() V24() Element of REAL
((A . ((g ^ g) /. k)) + (B . ((g ^ g) /. k))) * ((g ^ g) /. k) is Element of the carrier of V
(A . ((g ^ g) /. k)) * ((g ^ g) /. k) is Element of the carrier of V
((A . ((g ^ g) /. k)) * ((g ^ g) /. k)) + ((B . ((g ^ g) /. k)) * ((g ^ g) /. k)) is Element of the carrier of V
(A (#) (g ^ g)) /. k is Element of the carrier of V
(A (#) (g ^ g)) . k is set
I . x is set
Fp . x is set
Seg (len (B (#) (g ^ q))) is Element of bool NAT
Sum Hp is Element of the carrier of V
Seg (len ((A + B) (#) (B ^ x))) is Element of bool NAT
Sum Fp is Element of the carrier of V
Seg (len I) is Element of bool NAT
V is V22() V23() V24() Element of REAL

the carrier of A is non empty set

Sum (V * B) is Element of the carrier of A
Sum B is Element of the carrier of A
V * (Sum B) is Element of the carrier of A
Carrier (V * B) is finite Element of bool the carrier of A
bool the carrier of A is non empty set
{ b1 where b1 is Element of the carrier of A : not (V * B) . b1 = 0 } is set

rng c5 is set
(V * B) (#) c5 is Relation-like NAT -defined the carrier of A -valued Function-like FinSequence-like FinSequence of the carrier of A
Sum ((V * B) (#) c5) is Element of the carrier of A
Carrier B is finite Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not B . b1 = 0 } is set

rng l is set

Sum (B (#) l) is Element of the carrier of A

dom x is set
rng x is set
Seg (len c5) is Element of bool NAT
f is set
f is set
x . f is set

dom l is set
l . f is set
x . f is set
c5 <- (l . f) is set
dom c5 is set
f is set
dom l is set
x . f is set
dom c5 is set
Seg (len x) is Element of bool NAT
Seg (len x) is Element of bool NAT
f is set

l . f is set
x . f is set
c5 . (x . f) is set
c5 <- (l . f) is set
c5 . (c5 <- (l . f)) is set
l . f is set
x . f is set
c5 . (x . f) is set

f is set
dom (c5 ") is set
rng (l (#) (c5 ")) is set
rng (c5 ") is set
c5 (#) (c5 ") is Relation-like Function-like set
x (#) (c5 (#) (c5 ")) is Relation-like Function-like set
id (dom c5) is Relation-like dom c5 -defined dom c5 -valued Function-like one-to-one total Element of bool [:(dom c5),(dom c5):]
[:(dom c5),(dom c5):] is set
bool [:(dom c5),(dom c5):] is non empty set
x (#) (id (dom c5)) is Relation-like Function-like set
[:(Seg (len c5)),(Seg (len c5)):] is set
bool [:(Seg (len c5)),(Seg (len c5)):] is non empty set
f is Relation-like Seg (len c5) -defined Seg (len c5) -valued Function-like quasi_total Element of bool [:(Seg (len c5)),(Seg (len c5)):]
len ((V * B) (#) c5) is epsilon-transitive epsilon-connected ordinal natural V22() V23() V24() Element of NAT
dom ((V * B) (#) c5) is set
f is Relation-like Seg (len c5) -defined Seg (len c5) -valued Function-like quasi_total bijective Element of bool [:(Seg (len c5)),(Seg (len c5)):]
((V * B) (#) c5) * f is Relation-like Seg (len c5) -defined the carrier of A -valued Function-like Element of bool [:(Seg (len c5)), the carrier of A:]
[:(Seg (len c5)), the carrier of A:] is set
bool [:(Seg (len c5)), the carrier of A:] is non empty set
Seg (len ((V * B) (#) c5)) is Element of bool NAT

Sum f is Element of the carrier of A

dom (B (#) l) is set
g is Element of the carrier of A
(B (#) l) . g is set
l . g is set
c5 <- (l . g) is set

dom f is set
l /. g is Element of the carrier of A
f . g is set
c5 . (f . g) is set
c5 . g is set
c5 /. g is Element of the carrier of A
f . g is set
((V * B) (#) c5) . (f . g) is set
((V * B) (#) c5) . (c5 <- (l . g)) is set
(V * B) . (c5 /. g) is V22() V23() V24() Element of REAL
((V * B) . (c5 /. g)) * (c5 /. g) is Element of the carrier of A
B . (c5 /. g) is V22() V23() V24() Element of REAL
V * (B . (c5 /. g)) is V22() V23() V24() Element of REAL
(V * (B . (c5 /. g))) * (c5 /. g) is Element of the carrier of A
(B . (c5 /. g)) * (c5 /. g) is Element of the carrier of A
V * ((B . (c5 /. g)) * (c5 /. g)) is Element of the carrier of A
V * g is Element of the carrier of A
dom f is set

Sum () is Element of the carrier of A
0. A is V55(A) Element of the carrier of A

the carrier of V is non empty set

Sum (- A) is Element of the carrier of V
Sum A is Element of the carrier of V
- (Sum A) is Element of the carrier of V
(- 1) * (Sum A) is Element of the carrier of V

the carrier of V is non empty set

Sum A is Element of the carrier of V

Sum (A - B) is Element of the carrier of V
Sum B is Element of the carrier of V
(Sum A) - (Sum B) is Element of the carrier of V
Sum (- B) is Element of the carrier of V
(Sum A) + (Sum (- B)) is Element of the carrier of V
- (Sum B) is Element of the carrier of V
(Sum A) + (- (Sum B)) is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
B is Element of bool the carrier of V

Sum B is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0 } is set

Carrier c5 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not c5 . b1 = 0 } is set

the carrier of V is non empty set
bool the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
A is Element of bool the carrier of V
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set

B . (0. V) is V22() V23() V24() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

{(0. V)} is non empty finite Element of bool the carrier of V
c5 is non empty finite Element of bool the carrier of V
v is Element of the carrier of V
B . v is V22() V23() V24() Element of REAL
v is finite Element of bool the carrier of V

Carrier c5 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not c5 . b1 = 0 } is set
{(0. V)} is non empty finite Element of bool the carrier of V
v is set
l is Element of the carrier of V
c5 . l is V22() V23() V24() Element of REAL
v is set

Sum v is Element of the carrier of V
v . (0. V) is V22() V23() V24() Element of REAL
(v . (0. V)) * (0. V) is Element of the carrier of V

the carrier of V is non empty set

bool the carrier of V is non empty set

Sum A is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
Carrier A is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0 } is set

the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
A is Element of the carrier of V
{A} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set

Sum B is Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0 } is set
B . A is V22() V23() V24() Element of REAL
(B . A) * A is Element of the carrier of V
B is Element of the carrier of V
B . B is V22() V23() V24() Element of REAL

the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
{(0. V)} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set

the carrier of V is non empty set

the carrier of B is non empty set
A is Element of the carrier of V
0. V is V55(V) Element of the carrier of V
{A,(0. V)} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
0. B is V55(B) Element of the carrier of B
B is Element of the carrier of B
{(0. B),B} is non empty finite Element of bool the carrier of B
bool the carrier of B is non empty set

the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
B is V22() V23() V24() Element of REAL
B * B is Element of the carrier of V
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
c5 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of V,REAL:]
c5 . A is V22() V23() V24() Element of REAL
c5 . B is V22() V23() V24() Element of REAL
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
l is Element of the carrier of V

v . l is V22() V23() V24() Element of REAL

Carrier l is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0 } is set
x is set
f is Element of the carrier of V
l . f is V22() V23() V24() Element of REAL

Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
Sum x is Element of the carrier of V
(- 1) * (B * B) is Element of the carrier of V
((- 1) * (B * B)) + (B * B) is Element of the carrier of V
- (B * B) is Element of the carrier of V
(- (B * B)) + (B * B) is Element of the carrier of V
(B * B) - (B * B) is Element of the carrier of V
- ((B * B) - (B * B)) is Element of the carrier of V
- (0. V) is Element of the carrier of V
1 * B is Element of the carrier of V

Sum B is Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0 } is set
B . A is V22() V23() V24() Element of REAL
(B . A) * A is Element of the carrier of V
B . B is V22() V23() V24() Element of REAL
(B . B) * B is Element of the carrier of V
((B . A) * A) + ((B . B) * B) is Element of the carrier of V
the Element of Carrier B is Element of Carrier B
(B . A) " is V22() V23() V24() Element of REAL
((B . A) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V
((B . A) ") * ((B . A) * A) is Element of the carrier of V
((B . A) ") * ((B . B) * B) is Element of the carrier of V
(((B . A) ") * ((B . A) * A)) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V
((B . A) ") * (B . A) is V22() V23() V24() Element of REAL
(((B . A) ") * (B . A)) * A is Element of the carrier of V
((((B . A) ") * (B . A)) * A) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V
((B . A) ") * (B . B) is V22() V23() V24() Element of REAL
(((B . A) ") * (B . B)) * B is Element of the carrier of V
((((B . A) ") * (B . A)) * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
1 * A is Element of the carrier of V
(1 * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
A + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
- ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
(- 1) * ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
(- 1) * (((B . A) ") * (B . B)) is V22() V23() V24() Element of REAL
((- 1) * (((B . A) ") * (B . B))) * B is Element of the carrier of V
(B . B) " is V22() V23() V24() Element of REAL
((B . B) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V
((B . B) ") * ((B . A) * A) is Element of the carrier of V
((B . B) ") * ((B . B) * B) is Element of the carrier of V
(((B . B) ") * ((B . A) * A)) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V
((B . B) ") * (B . A) is V22() V23() V24() Element of REAL
(((B . B) ") * (B . A)) * A is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V
((B . B) ") * (B . B) is V22() V23() V24() Element of REAL
(((B . B) ") * (B . B)) * B is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + ((((B . B) ") * (B . B)) * B) is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + (1 * B) is Element of the carrier of V
0 * A is Element of the carrier of V
(0 * A) + B is Element of the carrier of V
(0. V) + B is Element of the carrier of V
v is Element of the carrier of V
B . v is V22() V23() V24() Element of REAL

the carrier of V is non empty set
0. V is V55(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
B is V22() V23() V24() Element of REAL
B * A is Element of the carrier of V
c5 is V22() V23() V24() Element of REAL
c5 * B is Element of the carrier of V
(B * A) + (c5 * B) is Element of the carrier of V
B " is V22() V23() V24() Element of REAL
(B ") * ((B * A) + (c5 * B)) is Element of the carrier of V
(B ") * (B * A) is Element of the carrier of V
(B ") * (c5 * B) is Element of the carrier of V
((B ") * (B * A)) + ((B ") * (c5 * B)) is Element of the carrier of V
(B ") * B is V22() V23() V24() Element of REAL
((B ") * B) * A is Element of the carrier of V
(((B ") * B) * A) + ((B ") * (c5 * B)) is Element of the carrier of V
(B ") * c5 is V22() V23() V24() Element of REAL
((B ") * c5) * B is Element of the carrier of V
(((B ") * B) * A) + (((B ") * c5) * B) is Element of the carrier of V
1 * A is Element of the carrier of V
(1 * A) + (((B ") * c5) * B) is Element of the carrier of V
A + (((B ") * c5) * B) is Element of the carrier of V
- (((B ") * c5) * B) is Element of the carrier of V
(- 1) * (((B ") * c5) * B) is Element of the carrier of V
(- 1) * ((B ") * c5) is V22() V23() V24() Element of REAL
((- 1) * ((B ") * c5)) * B is Element of the carrier of V
c5 " is V22() V23() V24() Element of REAL
(c5 ") * ((B * A) + (c5 * B)) is Element of the carrier of V
(c5 ") * (B * A) is Element of the carrier of V
(c5 ") * (c5 * B) is Element of the carrier of V
((c5 ") * (B * A)) + ((c5 ") * (c5 * B)) is Element of the carrier of V
(c5 ") * B is V22() V23() V24() Element of REAL
((c5 ") * B) * A is Element of the carrier of V
(((c5 ") * B) * A) + ((c5 ") * (c5 * B)) is Element of the carrier of V
(c5 ") * c5 is V22() V23() V24() Element of REAL
((c5 ") * c5) * B is Element of the carrier of V
(((c5 ") * B) * A) + (((c5 ") * c5) * B) is Element of the carrier of V
1 * B is Element of the carrier of V
(((c5 ") * B) * A) + (1 * B) is Element of the carrier of V
(((c5 ") * B) * A) + B is Element of the carrier of V
- (((c5 ") * B) * A) is Element of the carrier of V
(- 1) * (((c5 ") * B) * A) is Element of the carrier of V
(- 1) * ((c5 ") * B) is V22() V23() V24() Element of REAL
((- 1) * ((c5 ") * B)) * A is Element of the carrier of V
B is V22() V23() V24() Element of REAL
B * B is Element of the carrier of V
(0. V) + (B * B) is Element of the carrier of V
A - (B * B) is Element of the carrier of V
- (B * B) is Element of the carrier of V
A + (- (B * B)) is Element of the carrier of V
- B is Element of the carrier of V
B * (- B) is Element of the carrier of V
A + (B * (- B)) is Element of the carrier of V
- B is V22() V23() V24() Element of REAL
(- B) * B is Element of the carrier of V
A + ((- B) * B) is Element of the carrier of V
1 * A is Element of the carrier of V
(1 * A) + ((- B) * B) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
0 * A is Element of the carrier of V
(0 * A) + (0. V) is Element of the carrier of V
1 * B is Element of the carrier of V
(0 * A) + (1 * B) is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of A : verum } is set
B is set

Sum c5 is Element of the carrier of V

B is Element of bool the carrier of V
v is Element of the carrier of V
l is Element of the carrier of V
v + l is Element of the carrier of V

Sum x is Element of the carrier of V

Sum f is Element of the carrier of V

Sum f is Element of the carrier of V
v is V22() V23() V24() Element of REAL
l is Element of the carrier of V
v * l is Element of the carrier of V

Sum x is Element of the carrier of V

Sum f is Element of the carrier of V

Sum c5 is Element of the carrier of V
0. V is V55(V) Element of the carrier of V

the carrier of B is non empty set

the carrier of B is non empty set
V is set

the carrier of A is non empty set
bool the carrier of A is non empty set
B is Element of bool the carrier of A

the carrier of (A,B) is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of B : verum } is set

Sum B is Element of the carrier of A
{ (Sum b1) where b1 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Linear_Combination of B : verum } is set
the carrier of (A,B) is non empty set
V is set

the carrier of A is non empty set
bool the carrier of A is non empty set
B is Element of bool the carrier of A

[: the carrier of A,REAL:] is non empty set
bool [: the carrier of A,REAL:] is non empty set
B is Element of the carrier of A
c5 is Relation-like the carrier of A -defined REAL -valued Function-like quasi_total Element of bool [: the carrier of A,REAL:]
c5 . B is V22() V23() V24() Element of REAL
Funcs ( the carrier of A,REAL) is non empty FUNCTION_DOMAIN of the carrier of A, REAL

{B} is non empty finite Element of bool the carrier of A
l is non empty finite Element of bool the carrier of A
x is Element of the carrier of A
v . x is V22() V23() V24() Element of REAL
x is finite Element of bool the carrier of A

Carrier l is finite Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not l . b1 = 0 } is set
{B} is non empty finite Element of bool the carrier of A
x is set
f is Element of the carrier of A
l . f is V22() V23() V24() Element of REAL

Sum x is Element of the carrier of A
1 * B is Element of the carrier of A
Carrier x is finite Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not x . b1 = 0 } is set

Sum f is Element of the carrier of A
V is set

0. A is V55(A) Element of the carrier of A
the carrier of A is non empty set
the carrier of ((0). A) is non empty set
{(0. A)} is non empty finite Element of bool the carrier of A
bool the carrier of A is non empty set

the carrier of V is non empty set

bool the carrier of V is non empty set

B is Element of the carrier of V
the carrier of (V,({} the carrier of V)) is non empty set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total Linear_Combination of {} the carrier of V : verum } is set
0. V is V55(V) Element of the carrier of V

Sum B is Element of the carrier of V
0. V is V55(V) Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set

0. V is V55(V) Element of the carrier of V
{(0. V)} is non empty finite Element of bool the carrier of V
A is Element of bool the carrier of V

B is set
the Element of A is Element of A
B is set

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

the carrier of B is non empty set
B is Element of the carrier of V

Sum c5 is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) is non empty strict RLSStruct
the carrier of () is non empty set

the carrier of V is non empty set
c5 is Element of the carrier of V

the carrier of V is non empty set
c5 is Element of the carrier of V
v is Element of the carrier of V
l is Element of the carrier of V
v + l is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V

B is Element of the carrier of V

Sum c5 is Element of the carrier of V

Sum v is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V
A \/ B is Element of bool the carrier of V

B is Element of the carrier of V

Sum c5 is Element of the carrier of V
Carrier c5 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not c5 . b1 = 0 } is set
(Carrier c5) \ A is finite Element of bool the carrier of V
(Carrier c5) /\ A is finite Element of bool the carrier of V
x is set
[: the carrier of V,REAL:] is non empty set
bool [: the carrier of V,REAL:] is non empty set
f is Element of the carrier of V

f . f is V22() V23() V24() Element of REAL
c5 . x is set
x is set
c5 . x is set

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
f is finite Element of bool the carrier of V

f is Element of the carrier of V
f . f is V22() V23() V24() Element of REAL

Carrier f is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not f . b1 = 0 } is set
g is set
g is Element of the carrier of V
f . g is V22() V23() V24() Element of REAL
g is set
g is Element of the carrier of V

g . g is V22() V23() V24() Element of REAL
c5 . g is set
g is set
c5 . g is set

g is finite Element of bool the carrier of V

u is Element of the carrier of V
g . u is V22() V23() V24() Element of REAL
g is set

Carrier u is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not u . b1 = 0 } is set
g is set
v is Element of the carrier of V
u . v is V22() V23() V24() Element of REAL

v is Element of the carrier of V
c5 . v is V22() V23() V24() Element of REAL
(g + g) . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
(g . v) + (g . v) is V22() V23() V24() Element of REAL
(c5 . v) + (g . v) is V22() V23() V24() Element of REAL
(c5 . v) + 0 is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
(g . v) + (g . v) is V22() V23() V24() Element of REAL
0 + (g . v) is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
g . v is V22() V23() V24() Element of REAL
(g . v) + (g . v) is V22() V23() V24() Element of REAL
0 + (g . v) is V22() V23() V24() Element of REAL

Sum g is Element of the carrier of V
Sum g is Element of the carrier of V
(Sum g) + (Sum g) is Element of the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V

B is Element of bool the carrier of V
A /\ B is Element of bool the carrier of V

V is non empty set
union V is set

dom A is set
the Element of V is Element of V

the carrier of V is non empty set
bool the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of V:], the