begin
:: deftheorem Def1 defines Lin RUSUB_3:def 1 :
theorem Th1:
theorem Th2:
Lm1:
for V being RealUnitarySpace
for x being set holds
( x in (0). V iff x = 0. V )
theorem
theorem
theorem Th5:
theorem
Lm2:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
Lm3:
for V being RealUnitarySpace
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
Lm4:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
Lm5:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
theorem Th7:
theorem
theorem
theorem
theorem Th11:
theorem Th12:
begin
:: deftheorem Def2 defines Basis RUSUB_3:def 2 :
theorem
theorem
theorem Th15:
begin
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem
theorem Th25:
Lm6:
for X, x being set st not x in X holds
X \ {x} = X
theorem
theorem
theorem
begin
theorem Th29:
theorem
theorem
theorem Th32:
theorem
theorem
theorem Th35:
theorem
theorem
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem