begin
:: deftheorem Def1 defines linearly-closed RLSUB_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem
theorem
theorem
:: deftheorem Def2 defines Subspace RLSUB_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th17:
theorem Th18:
theorem
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
Lm1:
for V being RealLinearSpace
for V1 being Subset of
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th25:
theorem
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem Th43:
:: deftheorem Def3 defines (0). RLSUB_1:def 3 :
:: deftheorem defines (Omega). RLSUB_1:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th48:
theorem Th49:
theorem
theorem
theorem
theorem
canceled;
theorem
:: deftheorem defines + RLSUB_1:def 5 :
Lm2:
for V being RealLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
:: deftheorem Def6 defines Coset RLSUB_1:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th58:
theorem Th59:
theorem
theorem Th61:
Lm3:
for V being RealLinearSpace
for v being VECTOR of
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
theorem Th62:
theorem Th63:
theorem
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem
theorem Th70:
theorem Th71:
theorem Th72:
theorem
theorem Th74:
theorem Th75:
theorem
theorem Th77:
theorem
theorem Th79:
theorem
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th94:
theorem
theorem
theorem
theorem