begin
:: deftheorem Def1 defines linearly-closed RMOD_2:def 1 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem
theorem
theorem
:: deftheorem Def2 defines Submodule RMOD_2: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 R being Ring
for V being RightMod of
for V1 being Subset of
for W being Submodule 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
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem Th42:
:: deftheorem Def3 defines (0). RMOD_2:def 3 :
:: deftheorem defines (Omega). RMOD_2:def 4 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th47:
theorem Th48:
theorem
theorem
theorem
theorem
canceled;
theorem
:: deftheorem defines + RMOD_2:def 5 :
Lm2:
for R being Ring
for V being RightMod of
for W being Submodule of V holds (0. V) + W = the carrier of W
:: deftheorem Def6 defines Coset RMOD_2:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem Th61:
Lm3:
for R being Ring
for V being RightMod of
for v being Vector of
for W being Submodule of V holds
( v in W iff v + W = the carrier of W )
theorem Th62:
theorem Th63:
theorem
theorem
theorem Th66:
theorem
theorem Th68:
theorem Th69:
theorem Th70:
theorem
theorem Th72:
theorem
theorem
canceled;
theorem
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th90:
theorem
theorem
theorem
theorem