:: RUSUB_2 semantic presentation

K93() is V33() V34() V35() V39() set

K97() is V33() V34() V35() V36() V37() V38() V39() Element of bool K93()

bool K93() is non empty set

K92() is V33() V34() V35() V36() V37() V38() V39() set

bool K92() is non empty set

bool K97() is non empty set

[:K97(),K93():] is Relation-like set

bool [:K97(),K93():] is non empty set

{} is set

the Relation-like non-empty empty-yielding empty V33() V34() V35() V36() V37() V38() V39() set is Relation-like non-empty empty-yielding empty V33() V34() V35() V36() V37() V38() V39() set

1 is non empty V30() V31() V32() V33() V34() V35() V36() V37() V38() Element of K97()

0 is V30() V31() V32() V33() V34() V35() V36() V37() V38() Element of K97()

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

{ (b

bool the carrier of V is non empty set

the carrier of W1 is non empty set

the carrier of W2 is non empty set

B is set

C is Element of the carrier of V

AC is Element of the carrier of V

C + AC is Element of the carrier of V

0. V is V56(V) Element of the carrier of V

(0. V) + (0. V) is Element of the carrier of V

B is Element of bool the carrier of V

W3 is Element of bool the carrier of V

S is Element of bool the carrier of V

{ (b

C is set

AC is Element of the carrier of V

BC is Element of the carrier of V

AC + BC is Element of the carrier of V

C is set

AC is Element of the carrier of V

BC is Element of the carrier of V

AC + BC is Element of the carrier of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W3 is non empty set

S is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of S is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W2 is non empty set

the carrier of W1 /\ the carrier of W2 is set

the carrier of V is non empty set

0. V is V56(V) Element of the carrier of V

the carrier of V /\ the carrier of V is set

bool the carrier of V is non empty set

B is Element of bool the carrier of V

C is Element of bool the carrier of V

AC is Element of bool the carrier of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W3 is non empty set

S is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of S is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is set

the carrier of (V,W1,W2) is non empty set

{ (b

S is Element of the carrier of V

A is Element of the carrier of V

S + A is Element of the carrier of V

S is Element of the carrier of V

A is Element of the carrier of V

S + A is Element of the carrier of V

{ (b

the carrier of (V,W1,W2) is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is Element of the carrier of V

0. V is V56(V) Element of the carrier of V

W3 + (0. V) is Element of the carrier of V

0. V is V56(V) Element of the carrier of V

(0. V) + W3 is Element of the carrier of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is set

the carrier of (V,W1,W2) is non empty set

the carrier of W1 is non empty set

the carrier of W2 is non empty set

the carrier of W1 /\ the carrier of W2 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

{ (b

{ (b

A 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

the carrier of (V,W1,W2) is non empty set

A is set

B is Element of the carrier of V

C is Element of the carrier of V

B + C is Element of the carrier of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,W2) is non empty set

W3 is set

the carrier of V is non empty set

{ (b

A is Element of the carrier of W1

B is Element of the carrier of V

0. V is V56(V) Element of the carrier of V

B + (0. V) is Element of the carrier of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W2 is non empty set

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,W2) is non empty set

W3 is set

the carrier of V is non empty set

{ (b

S is Element of the carrier of V

A is Element of the carrier of V

S + A is Element of the carrier of V

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

{ (b

{ (b

{ (b

{ (b

the carrier of (V,W1,(V,W2,W3)) is non empty set

AC is set

BC is Element of the carrier of V

L is Element of the carrier of V

BC + L is Element of the carrier of V

the carrier of (V,W1,W2) is non empty set

B9 is Element of the carrier of V

B is Element of the carrier of V

B9 + B is Element of the carrier of V

B + L is Element of the carrier of V

the carrier of (V,W2,W3) is non empty set

B9 + (B + L) is Element of the carrier of V

AC is set

BC is Element of the carrier of V

L is Element of the carrier of V

BC + L is Element of the carrier of V

the carrier of (V,W2,W3) is non empty set

B9 is Element of the carrier of V

B is Element of the carrier of V

B9 + B is Element of the carrier of V

BC + B9 is Element of the carrier of V

the carrier of (V,W1,W2) is non empty set

(BC + B9) + B is Element of the carrier of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

the carrier of (V,W1,W2) is non empty set

the carrier of W2 is non empty set

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W2,W1) is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

the carrier of W2 is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(0). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,((0). V),W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,((0). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of ((0). V) is non empty set

the carrier of W1 is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(0). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,((0). V),((Omega). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like 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 [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]

[:K93(), the carrier of V:] is Relation-like set

[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set

bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set

the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined K93() -valued Function-like V18([: the carrier of V, the carrier of V:],K93()) Element of bool [:[: the carrier of V, the carrier of V:],K93():]

[:[: the carrier of V, the carrier of V:],K93():] is Relation-like set

bool [:[: the carrier of V, the carrier of V:],K93():] is non empty set

UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

(V,((Omega). V),((0). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like 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 [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]

[:K93(), the carrier of V:] is Relation-like set

[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set

bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set

the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined K93() -valued Function-like V18([: the carrier of V, the carrier of V:],K93()) Element of bool [:[: the carrier of V, the carrier of V:],K93():]

[:[: the carrier of V, the carrier of V:],K93():] is Relation-like set

bool [:[: the carrier of V, the carrier of V:],K93():] is non empty set

UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,((Omega). V),W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,((Omega). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) is non empty set

the carrier of W1 is non empty set

the carrier of ((Omega). V) is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,((Omega). V),((Omega). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

the carrier of W1 /\ the carrier of W1 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,W2) is non empty set

the carrier of W2 is non empty set

the carrier of W1 is non empty set

the carrier of W2 /\ the carrier of W1 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

the carrier of W2 is non empty set

the carrier of W3 is non empty set

the carrier of (V,W1,(V,W2,W3)) is non empty set

the carrier of (V,W2,W3) is non empty set

the carrier of W1 /\ the carrier of (V,W2,W3) is set

the carrier of W2 /\ the carrier of W3 is set

the carrier of W1 /\ ( the carrier of W2 /\ the carrier of W3) is set

the carrier of W1 /\ the carrier of W2 is set

( the carrier of W1 /\ the carrier of W2) /\ the carrier of W3 is set

the carrier of (V,W1,W2) is non empty set

the carrier of (V,W1,W2) /\ the carrier of W3 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,W2) is non empty set

the carrier of W1 is non empty set

the carrier of W2 is non empty set

the carrier of W1 /\ the carrier of W2 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,W2) is non empty set

the carrier of W1 is non empty set

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W2,W1) is non empty set

the carrier of W2 is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W2 is non empty set

the carrier of W1 is non empty set

the carrier of (V,W2,W1) is non empty set

the carrier of W2 /\ the carrier of W1 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(0). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,((0). V),W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,((0). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

0. V is V56(V) Element of the carrier of V

the carrier of V is non empty set

the carrier of W1 is non empty set

{(0. V)} is Element of bool the carrier of V

bool the carrier of V is non empty set

{(0. V)} /\ the carrier of W1 is Element of bool the carrier of V

the carrier of (V,((0). V),W1) is non empty set

the carrier of ((0). V) is non empty set

the carrier of ((0). V) /\ the carrier of W1 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(0). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,((0). V),((Omega). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(Omega). W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of W1

(0). W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of W1

(W1,((Omega). W1),((0). W1)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of W1

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,((Omega). V),W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,((Omega). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like 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 [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]

[:K93(), the carrier of V:] is Relation-like set

[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set

bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set

the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined K93() -valued Function-like V18([: the carrier of V, the carrier of V:],K93()) Element of bool [:[: the carrier of V, the carrier of V:],K93():]

[:[: the carrier of V, the carrier of V:],K93():] is Relation-like set

bool [:[: the carrier of V, the carrier of V:],K93():] is non empty set

UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

the carrier of (V,((Omega). V),W1) is non empty set

the carrier of W1 is non empty set

the carrier of V /\ the carrier of W1 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,((Omega). V),((Omega). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,W2) is non empty set

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,W2) is non empty set

the carrier of W1 is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,(V,W1,W2),W2) is non empty set

the carrier of W2 is non empty set

W3 is set

the carrier of V is non empty set

{ (b

S is Element of the carrier of V

A is Element of the carrier of V

S + A is Element of the carrier of V

W3 is set

(V,W2,(V,W1,W2)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W2,(V,W1,W2)) is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W1,W2)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W1,(V,W1,W2)) is non empty set

the carrier of W1 is non empty set

W3 is set

the carrier of (V,W1,W2) is non empty set

the carrier of W1 /\ the carrier of (V,W1,W2) is set

W3 is set

the carrier of V is non empty set

S is Element of the carrier of V

0. V is V56(V) Element of the carrier of V

S + (0. V) is Element of the carrier of V

{ (b

the carrier of (V,W1,W2) is non empty set

the carrier of W1 /\ the carrier of (V,W1,W2) is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W2,W1)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,(V,W1,W2),(V,W2,W3)) is non empty set

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W2,(V,W1,W3)) is non empty set

S is set

the carrier of V is non empty set

{ (b

A is Element of the carrier of V

B is Element of the carrier of V

A + B is Element of the carrier of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W2,(V,W1,W3)) is non empty set

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,(V,W1,W2),(V,W2,W3)) is non empty set

S is set

the carrier of W2 is non empty set

the carrier of (V,W1,W3) is non empty set

the carrier of W2 /\ the carrier of (V,W1,W3) is set

the carrier of V is non empty set

{ (b

A is Element of the carrier of V

B is Element of the carrier of V

A + B is Element of the carrier of V

B + A is Element of the carrier of V

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

- A is Element of the carrier of V

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

A - A is Element of the carrier of V

K187(V,A,(- A)) is Element of the carrier of V

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

0. V is V56(V) Element of the carrier of V

B + (0. V) is Element of the carrier of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W2,(V,W1,W3)) is non empty set

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,(V,W1,W2),(V,W2,W3)) is non empty set

S is set

the carrier of V is non empty set

{ (b

A is Element of the carrier of V

B is Element of the carrier of V

A + B is Element of the carrier of V

{ (b

the carrier of (V,W2,W3) is non empty set

{ (b

the carrier of (V,W1,W2) is non empty set

the carrier of (V,W1,W2) /\ the carrier of (V,W2,W3) is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,W2,(V,W1,W3)) is non empty set

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of (V,(V,W1,W2),(V,W2,W3)) is non empty set

the carrier of V is non empty set

bool the carrier of V is non empty set

the carrier of W2 is non empty set

S is Element of bool the carrier of V

the carrier of W1 is non empty set

A is set

the carrier of (V,W1,W2) is non empty set

the carrier of (V,W2,W3) is non empty set

the carrier of (V,W1,W2) /\ the carrier of (V,W2,W3) 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

0. V is V56(V) Element of the carrier of V

(B + C) + (0. V) is Element of the carrier of V

{ (b

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,(V,W1,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W3,(V,W1,W2)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W3,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W3),(V,W3,W2)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W3,W2)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W3),(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W3,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W3),(V,W3,W2)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W3),W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,(V,W1,W3),W3),W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W3,W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W3,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,(V,W3,W3)),W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W3),W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W3,W2)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,(V,W2,W3)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,W1,W2),W3) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of W2 is non empty set

the carrier of W1 \/ the carrier of W2 is set

A is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of A is non empty set

C is set

the carrier of V is non empty set

AC is Element of the carrier of W2

bool the carrier of V is non empty set

L is Element of bool the carrier of V

B9 is set

B is Element of the carrier of W1

x is Element of bool the carrier of V

v is Element of the carrier of V

BC is Element of the carrier of V

v + BC is Element of the carrier of V

(v + BC) - BC is Element of the carrier of V

- BC is Element of the carrier of V

K187(V,(v + BC),(- BC)) is Element of the carrier of V

BC - BC is Element of the carrier of V

K187(V,BC,(- BC)) is Element of the carrier of V

v + (BC - BC) is Element of the carrier of V

0. V is V56(V) Element of the carrier of V

v + (0. V) is Element of the carrier of V

x is Element of bool the carrier of V

BC + v is Element of the carrier of V

(BC + v) - v is Element of the carrier of V

- v is Element of the carrier of V

K187(V,(BC + v),(- v)) is Element of the carrier of V

v - v is Element of the carrier of V

K187(V,v,(- v)) is Element of the carrier of V

BC + (v - v) is Element of the carrier of V

BC + (0. V) is Element of the carrier of V

A is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of A is non empty set

B is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

the carrier of B is non empty set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W1 is set

W3 is set

A is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is set

the carrier of A is non empty set

S is set

B is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of B is non empty set

W2 is Relation-like Function-like set

W3 is set

S is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of S is non empty set

A is set

[W3,A] is set

{W3,A} is set

{W3} is set

{{W3,A},{W3}} is set

S is set

[W3,S] is set

{W3,S} is set

{W3} is set

{{W3,S},{W3}} is set

dom W2 is set

rng W2 is set

W3 is set

S is set

W2 . S is set

[S,W3] is set

{S,W3} is set

{S} is set

{{S,W3},{S}} is set

A is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of A is non empty set

S is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of S is non empty set

A is set

[A,W3] is set

{A,W3} is set

{A} is set

{{A,W3},{A}} is set

W2 . A is set

W1 is set

W2 is set

W3 is set

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

(V) is set

the non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like UNITSTR

(V) is non empty set

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like 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 [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]

[:K93(), the carrier of V:] is Relation-like set

[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set

bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set

the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined K93() -valued Function-like V18([: the carrier of V, the carrier of V:],K93()) Element of bool [:[: the carrier of V, the carrier of V:],K93():]

[:[: the carrier of V, the carrier of V:],K93():] is Relation-like set

bool [:[: the carrier of V, the carrier of V:],K93():] is non empty set

UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W2 is Element of the carrier of V

(Omega). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like 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 [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]

[:K93(), the carrier of V:] is Relation-like set

[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set

bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set

the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined K93() -valued Function-like V18([: the carrier of V, the carrier of V:],K93()) Element of bool [:[: the carrier of V, the carrier of V:],K93():]

[:[: the carrier of V, the carrier of V:],K93():] is Relation-like set

bool [:[: the carrier of V, the carrier of V:],K93():] is non empty set

UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is Element of the carrier of V

W3 is Element of the carrier of V

S is Element of the carrier of V

A is Element of the carrier of V

S + A is Element of the carrier of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(0). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V) is non empty set

W2 is set

(V,W1,((0). V)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

W3 is non empty set

[:W3,W3:] is Relation-like non empty set

bool [:W3,W3:] is non empty set

S is Relation-like W3 -defined W3 -valued Element of bool [:W3,W3:]

A is Element of W3

B is Element of W3

[A,B] is set

{A,B} is set

{A} is set

{{A,B},{A}} is set

C is Element of W3

[B,C] is set

{B,C} is set

{B} is set

{{B,C},{B}} is set

AC is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

BC is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

L is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

B9 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

[A,C] is set

{A,C} is set

{{A,C},{A}} is set

A is set

the Element of W3 is Element of W3

AC is Element of W3

C is Element of W3

[AC,C] is Element of [:W3,W3:]

{AC,C} is set

{AC} is set

{{AC,C},{AC}} is set

B is set

C is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,C) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of C is non empty set

AC is set

B is Relation-like Function-like set

dom B is set

rng B is set

union (rng B) is set

AC is set

BC is set

L is set

B . L is set

B9 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of B9 is non empty set

the carrier of V is non empty set

the Element of rng B is Element of rng B

BC is set

B . BC is set

bool the carrier of V is non empty set

L is Element of bool the carrier of V

B9 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of B9 is non empty set

B9 is Element of the carrier of V

B is Element of the carrier of V

B9 + B is Element of the carrier of V

v is set

x is set

B . x is set

C is set

u is set

B . u is set

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W1 is non empty set

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of W2 is non empty set

y1 is Element of W3

y2 is Element of W3

[y1,y2] is Element of [:W3,W3:]

{y1,y2} is set

{y1} is set

{{y1,y2},{y1}} is set

c

c

B . y2 is set

y2 is Element of W3

y1 is Element of W3

[y2,y1] is Element of [:W3,W3:]

{y2,y1} is set

{y2} is set

{{y2,y1},{y2}} is set

c

c

B . y1 is set

y1 is Element of W3

y2 is Element of W3

[y1,y2] is Element of [:W3,W3:]

{y1,y2} is set

{y1} is set

{{y1,y2},{y1}} is set

[y2,y1] is Element of [:W3,W3:]

{y2,y1} is set

{y2} is set

{{y2,y1},{y2}} is set

B9 is V31() V32() Element of K93()

B is Element of the carrier of V

B9 * B is Element of the carrier of V

the Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]

[:K93(), the carrier of V:] is Relation-like set

[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set

bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set

the Mult of V . (B9,B) is set

v is set

x is set

B . x is set

C is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of C is non empty set

B9 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of B9 is non empty set

(V,W1,B9) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

B is Element of the carrier of V

v is set

x is set

B . x is set

C is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of C is non empty set

u is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,u) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of ((0). V) is non empty set

0. V is V56(V) Element of the carrier of V

{(0. V)} is Element of bool the carrier of V

B is Element of W3

x is Element of W3

B . x is set

C is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of C is non empty set

u is Element of the carrier of V

v is Element of W3

[x,v] is Element of [:W3,W3:]

{x,v} is set

{x} is set

{{x,v},{x}} is set

B is Element of W3

A is Element of W3

A is Element of W3

B is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

[A,A] is set

{A,A} is set

{A} is set

{{A,A},{A}} is set

A is Element of W3

B is Element of W3

[A,B] is set

{A,B} is set

{A} is set

{{A,B},{A}} is set

[B,A] is set

{B,A} is set

{B} is set

{{B,A},{B}} is set

C is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

AC is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

BC is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

L is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

A is Element of W3

B is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W1,B) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like 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 [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]

[:K93(), the carrier of V:] is Relation-like set

[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set

bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set

the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined K93() -valued Function-like V18([: the carrier of V, the carrier of V:],K93()) Element of bool [:[: the carrier of V, the carrier of V:],K93():]

[:[: the carrier of V, the carrier of V:],K93():] is Relation-like set

bool [:[: the carrier of V, the carrier of V:],K93():] is non empty set

UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) is non empty strict UNITSTR

(V,B,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

C is Element of the carrier of V

0. V is V56(V) Element of the carrier of V

(0. V) + C is Element of the carrier of V

{ (b

1 * C is Element of the carrier of V

the Mult of V . (1,C) is set

BC is set

L is V31() V32() Element of K93()

L * C is Element of the carrier of V

the Mult of V . (L,C) is set

bool the carrier of V is non empty set

BC is Element of bool the carrier of V

L is Element of the carrier of V

B9 is Element of the carrier of V

L + B9 is Element of the carrier of V

B is V31() V32() Element of K93()

B * C is Element of the carrier of V

the Mult of V . (B,C) is set

v is V31() V32() Element of K93()

v * C is Element of the carrier of V

the Mult of V . (v,C) is set

B + v is V31() V32() Element of K93()

(B + v) * C is Element of the carrier of V

the Mult of V . ((B + v),C) is set

L is V31() V32() Element of K93()

B9 is Element of the carrier of V

L * B9 is Element of the carrier of V

the Mult of V . (L,B9) is set

B is V31() V32() Element of K93()

B * C is Element of the carrier of V

the Mult of V . (B,C) is set

L * B is V31() V32() Element of K93()

(L * B) * C is Element of the carrier of V

the Mult of V . ((L * B),C) is set

L is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of L is non empty set

(V,W1,B) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,L,(V,W1,B)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

B9 is Element of the carrier of V

B is V31() V32() Element of K93()

B * C is Element of the carrier of V

the Mult of V . (B,C) is set

B " is V31() V32() Element of K93()

(B ") * (B * C) is Element of the carrier of V

the Mult of V . ((B "),(B * C)) is set

(B ") * B is V31() V32() Element of K93()

((B ") * B) * C is Element of the carrier of V

the Mult of V . (((B ") * B),C) is set

the carrier of ((0). V) is non empty set

{(0. V)} is Element of bool the carrier of V

(V,L,B) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,(V,L,B),W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

B9 is Element of the carrier of V

B is Element of the carrier of V

v is Element of the carrier of V

B + v is Element of the carrier of V

B9 - v is Element of the carrier of V

- v is Element of the carrier of V

K187(V,B9,(- v)) is Element of the carrier of V

(V,W1,(V,L,B)) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

B9 is Element of W3

[A,B9] is Element of [:W3,W3:]

{A,B9} is set

{A} is set

{{A,B9},{A}} is set

(V,B,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W1 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

W2 is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like Subspace of V

(V,W1,W2) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(0). V is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

(V,W2,W1) is non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like Subspace of V

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty