begin
theorem Th1:
Lm1:
for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
Lm2:
for X, x being set st not x in X holds
X \ {x} = X
theorem Th2:
:: deftheorem Def1 defines finite-dimensional RUSUB_4:def 1 :
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem Th7:
begin
:: deftheorem RUSUB_4:def 2 :
canceled;
:: deftheorem Def3 defines dim RUSUB_4:def 3 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
theorem
theorem Th15:
theorem
theorem
begin
Lm3:
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st n <= dim V holds
ex W being strict Subspace of V st dim W = n
theorem
:: deftheorem Def4 defines Subspaces_of RUSUB_4:def 4 :
theorem
theorem
theorem
begin
:: deftheorem Def5 defines Affine RUSUB_4:def 5 :
theorem Th22:
theorem
:: deftheorem defines Up RUSUB_4:def 6 :
:: deftheorem defines Up RUSUB_4:def 7 :
theorem
theorem Th25:
:: deftheorem Def8 defines Subspace-like RUSUB_4:def 8 :
theorem Th26:
theorem
theorem
canceled;
theorem
theorem
:: deftheorem defines + RUSUB_4:def 9 :
theorem
canceled;
theorem
theorem Th33:
theorem
:: deftheorem defines + RUSUB_4:def 10 :
theorem Th35:
theorem Th36:
theorem
theorem
theorem