begin
Lm1:
for V being RealLinearSpace
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
Lm2:
for x being set
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V )
Lm3:
for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
Lm4:
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
Lm5:
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
Lm6:
for V being RealLinearSpace
for W1, W3, W2 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
Lm7:
for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M
:: Auxiliary theorems.
::