begin
:: deftheorem Def1 defines Subspace RUSUB_1:def 1 :
theorem
theorem Th2:
theorem Th3:
theorem
theorem
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
Lm1:
for V being RealUnitarySpace
for W being Subspace of V
for V1, V2 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem Th29:
begin
:: deftheorem Def2 defines (0). RUSUB_1:def 2 :
:: deftheorem defines (Omega). RUSUB_1:def 3 :
begin
theorem Th30:
theorem Th31:
theorem
theorem
theorem
theorem
begin
:: deftheorem defines + RUSUB_1:def 4 :
Lm2:
for V being RealUnitarySpace
for W being Subspace of V holds (0. V) + W = the carrier of W
:: deftheorem Def5 defines Coset RUSUB_1:def 5 :
begin
theorem Th36:
theorem Th37:
theorem
theorem Th39:
Lm3:
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff v + W = the carrier of W )
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem Th52:
theorem Th53:
theorem
theorem Th55:
theorem
theorem Th57:
theorem
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th72:
theorem
theorem
theorem
theorem