:: by Michal Muzalewski and Wojciech Skaba

::

:: Received October 22, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

:: deftheorem defines linearly-closed RMOD_2:def 1 :

for R being Ring

for V being RightMod of R

for V1 being Subset of V holds

( V1 is linearly-closed iff ( ( for v, u being Vector of V st v in V1 & u in V1 holds

v + u in V1 ) & ( for a being Scalar of R

for v being Vector of V st v in V1 holds

v * a in V1 ) ) );

for R being Ring

for V being RightMod of R

for V1 being Subset of V holds

( V1 is linearly-closed iff ( ( for v, u being Vector of V st v in V1 & u in V1 holds

v + u in V1 ) & ( for a being Scalar of R

for v being Vector of V st v in V1 holds

v * a in V1 ) ) );

theorem Th1: :: RMOD_2:1

for R being Ring

for V being RightMod of R

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1

for V being RightMod of R

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1

proof end;

theorem Th2: :: RMOD_2:2

for R being Ring

for V being RightMod of R

for V1 being Subset of V st V1 is linearly-closed holds

for v being Vector of V st v in V1 holds

- v in V1

for V being RightMod of R

for V1 being Subset of V st V1 is linearly-closed holds

for v being Vector of V st v in V1 holds

- v in V1

proof end;

theorem :: RMOD_2:3

for R being Ring

for V being RightMod of R

for V1 being Subset of V st V1 is linearly-closed holds

for v, u being Vector of V st v in V1 & u in V1 holds

v - u in V1

for V being RightMod of R

for V1 being Subset of V st V1 is linearly-closed holds

for v, u being Vector of V st v in V1 & u in V1 holds

v - u in V1

proof end;

theorem :: RMOD_2:5

theorem :: RMOD_2:6

for R being Ring

for V being RightMod of R

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is Vector of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

for V being RightMod of R

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is Vector of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

proof end;

theorem :: RMOD_2:7

for R being Ring

for V being RightMod of R

for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds

V1 /\ V2 is linearly-closed

for V being RightMod of R

for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds

V1 /\ V2 is linearly-closed

proof end;

definition

let R be Ring;

let V be RightMod of R;

ex b_{1} being RightMod of R st

( the carrier of b_{1} c= the carrier of V & 0. b_{1} = 0. V & the addF of b_{1} = the addF of V | [: the carrier of b_{1}, the carrier of b_{1}:] & the rmult of b_{1} = the rmult of V | [: the carrier of b_{1}, the carrier of R:] )

end;
let V be RightMod of R;

mode Submodule of V -> RightMod of R means :Def2: :: RMOD_2:def 2

( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V | [: the carrier of it, the carrier of it:] & the rmult of it = the rmult of V | [: the carrier of it, the carrier of R:] );

existence ( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V | [: the carrier of it, the carrier of it:] & the rmult of it = the rmult of V | [: the carrier of it, the carrier of R:] );

ex b

( the carrier of b

proof end;

:: deftheorem Def2 defines Submodule RMOD_2:def 2 :

for R being Ring

for V, b_{3} being RightMod of R holds

( b_{3} is Submodule of V iff ( the carrier of b_{3} c= the carrier of V & 0. b_{3} = 0. V & the addF of b_{3} = the addF of V | [: the carrier of b_{3}, the carrier of b_{3}:] & the rmult of b_{3} = the rmult of V | [: the carrier of b_{3}, the carrier of R:] ) );

for R being Ring

for V, b

( b

theorem :: RMOD_2:8

for x being object

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds

x in W2

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V st x in W1 & W1 is Submodule of W2 holds

x in W2

proof end;

theorem Th9: :: RMOD_2:9

for x being object

for R being Ring

for V being RightMod of R

for W being Submodule of V st x in W holds

x in V

for R being Ring

for V being RightMod of R

for W being Submodule of V st x in W holds

x in V

proof end;

theorem Th10: :: RMOD_2:10

for R being Ring

for V being RightMod of R

for W being Submodule of V

for w being Vector of W holds w is Vector of V

for V being RightMod of R

for W being Submodule of V

for w being Vector of W holds w is Vector of V

proof end;

theorem :: RMOD_2:11

theorem Th13: :: RMOD_2:13

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for w1, w2 being Vector of W st w1 = v & w2 = u holds

w1 + w2 = v + u

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for w1, w2 being Vector of W st w1 = v & w2 = u holds

w1 + w2 = v + u

proof end;

theorem Th14: :: RMOD_2:14

for R being Ring

for a being Scalar of R

for V being RightMod of R

for v being Vector of V

for W being Submodule of V

for w being Vector of W st w = v holds

w * a = v * a

for a being Scalar of R

for V being RightMod of R

for v being Vector of V

for W being Submodule of V

for w being Vector of W st w = v holds

w * a = v * a

proof end;

theorem Th15: :: RMOD_2:15

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V

for w being Vector of W st w = v holds

- v = - w

for V being RightMod of R

for v being Vector of V

for W being Submodule of V

for w being Vector of W st w = v holds

- v = - w

proof end;

theorem Th16: :: RMOD_2:16

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for w1, w2 being Vector of W st w1 = v & w2 = u holds

w1 - w2 = v - u

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for w1, w2 being Vector of W st w1 = v & w2 = u holds

w1 - w2 = v - u

proof end;

Lm1: for R being Ring

for V being RightMod of R

for V1 being Subset of V

for W being Submodule of V st the carrier of W = V1 holds

V1 is linearly-closed

proof end;

theorem :: RMOD_2:19

theorem Th20: :: RMOD_2:20

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st u in W & v in W holds

u + v in W

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st u in W & v in W holds

u + v in W

proof end;

theorem Th21: :: RMOD_2:21

for R being Ring

for a being Scalar of R

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

v * a in W

for a being Scalar of R

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

v * a in W

proof end;

theorem Th22: :: RMOD_2:22

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

- v in W

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

- v in W

proof end;

theorem Th23: :: RMOD_2:23

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st u in W & v in W holds

u - v in W

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st u in W & v in W holds

u - v in W

proof end;

theorem Th25: :: RMOD_2:25

for R being Ring

for X, V being strict RightMod of R st V is Submodule of X & X is Submodule of V holds

V = X

for X, V being strict RightMod of R st V is Submodule of X & X is Submodule of V holds

V = X

proof end;

registration

let R be Ring;

let V be RightMod of R;

ex b_{1} being Submodule of V st b_{1} is strict

end;
let V be RightMod of R;

cluster non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like for Submodule of V;

existence ex b

proof end;

theorem Th26: :: RMOD_2:26

for R being Ring

for V, X, Y being RightMod of R st V is Submodule of X & X is Submodule of Y holds

V is Submodule of Y

for V, X, Y being RightMod of R st V is Submodule of X & X is Submodule of Y holds

V is Submodule of Y

proof end;

theorem Th27: :: RMOD_2:27

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds

W1 is Submodule of W2

for V being RightMod of R

for W1, W2 being Submodule of V st the carrier of W1 c= the carrier of W2 holds

W1 is Submodule of W2

proof end;

theorem :: RMOD_2:28

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds

v in W2 ) holds

W1 is Submodule of W2

for V being RightMod of R

for W1, W2 being Submodule of V st ( for v being Vector of V st v in W1 holds

v in W2 ) holds

W1 is Submodule of W2

proof end;

theorem Th29: :: RMOD_2:29

for R being Ring

for V being RightMod of R

for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds

W1 = W2

for V being RightMod of R

for W1, W2 being strict Submodule of V st the carrier of W1 = the carrier of W2 holds

W1 = W2

proof end;

theorem Th30: :: RMOD_2:30

for R being Ring

for V being RightMod of R

for W1, W2 being strict Submodule of V st ( for v being Vector of V holds

( v in W1 iff v in W2 ) ) holds

W1 = W2

for V being RightMod of R

for W1, W2 being strict Submodule of V st ( for v being Vector of V holds

( v in W1 iff v in W2 ) ) holds

W1 = W2

proof end;

theorem :: RMOD_2:31

for R being Ring

for V being strict RightMod of R

for W being strict Submodule of V st the carrier of W = the carrier of V holds

W = V

for V being strict RightMod of R

for W being strict Submodule of V st the carrier of W = the carrier of V holds

W = V

proof end;

theorem :: RMOD_2:32

for R being Ring

for V being strict RightMod of R

for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds

W = V

for V being strict RightMod of R

for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds

W = V

proof end;

theorem :: RMOD_2:33

theorem Th34: :: RMOD_2:34

for R being Ring

for V being RightMod of R

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Submodule of V st V1 = the carrier of W

for V being RightMod of R

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Submodule of V st V1 = the carrier of W

proof end;

definition

let R be Ring;

let V be RightMod of R;

correctness

existence

ex b_{1} being strict Submodule of V st the carrier of b_{1} = {(0. V)};

uniqueness

for b_{1}, b_{2} being strict Submodule of V st the carrier of b_{1} = {(0. V)} & the carrier of b_{2} = {(0. V)} holds

b_{1} = b_{2};

by Th4, Th29, Th34;

end;
let V be RightMod of R;

correctness

existence

ex b

uniqueness

for b

b

by Th4, Th29, Th34;

:: deftheorem Def3 defines (0). RMOD_2:def 3 :

for R being Ring

for V being RightMod of R

for b_{3} being strict Submodule of V holds

( b_{3} = (0). V iff the carrier of b_{3} = {(0. V)} );

for R being Ring

for V being RightMod of R

for b

( b

definition

let R be Ring;

let V be RightMod of R;

RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is strict Submodule of V

end;
let V be RightMod of R;

func (Omega). V -> strict Submodule of V equals :: RMOD_2:def 4

RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);

coherence RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);

RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is strict Submodule of V

proof end;

:: deftheorem defines (Omega). RMOD_2:def 4 :

for R being Ring

for V being RightMod of R holds (Omega). V = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);

for R being Ring

for V being RightMod of R holds (Omega). V = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);

theorem :: RMOD_2:38

theorem :: RMOD_2:39

for R being Ring

for V being RightMod of R

for W being Submodule of V holds (0). V is Submodule of W

for V being RightMod of R

for W being Submodule of V holds (0). V is Submodule of W

proof end;

theorem :: RMOD_2:40

for R being Ring

for V being RightMod of R

for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2

for V being RightMod of R

for W1, W2 being Submodule of V holds (0). W1 is Submodule of W2

proof end;

theorem :: RMOD_2:41

definition

let R be Ring;

let V be RightMod of R;

let v be Vector of V;

let W be Submodule of V;

coherence

{ (v + u) where u is Vector of V : u in W } is Subset of V

end;
let V be RightMod of R;

let v be Vector of V;

let W be Submodule of V;

coherence

{ (v + u) where u is Vector of V : u in W } is Subset of V

proof end;

:: deftheorem defines + RMOD_2:def 5 :

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds v + W = { (v + u) where u is Vector of V : u in W } ;

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds v + W = { (v + u) where u is Vector of V : u in W } ;

Lm2: for R being Ring

for V being RightMod of R

for W being Submodule of V holds (0. V) + W = the carrier of W

proof end;

definition

let R be Ring;

let V be RightMod of R;

let W be Submodule of V;

existence

ex b_{1} being Subset of V ex v being Vector of V st b_{1} = v + W

end;
let V be RightMod of R;

let W be Submodule of V;

existence

ex b

proof end;

:: deftheorem Def6 defines Coset RMOD_2:def 6 :

for R being Ring

for V being RightMod of R

for W being Submodule of V

for b_{4} being Subset of V holds

( b_{4} is Coset of W iff ex v being Vector of V st b_{4} = v + W );

for R being Ring

for V being RightMod of R

for W being Submodule of V

for b

( b

theorem Th42: :: RMOD_2:42

for x being object

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds

( x in v + W iff ex u being Vector of V st

( u in W & x = v + u ) )

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds

( x in v + W iff ex u being Vector of V st

( u in W & x = v + u ) )

proof end;

theorem Th43: :: RMOD_2:43

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds

( 0. V in v + W iff v in W )

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds

( 0. V in v + W iff v in W )

proof end;

theorem Th44: :: RMOD_2:44

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds v in v + W

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds v in v + W

proof end;

theorem :: RMOD_2:45

Lm3: for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V holds

( v in W iff v + W = the carrier of W )

proof end;

theorem :: RMOD_2:49

theorem :: RMOD_2:50

theorem Th51: :: RMOD_2:51

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u in W iff v + W = (v + u) + W )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u in W iff v + W = (v + u) + W )

proof end;

theorem :: RMOD_2:52

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u in W iff v + W = (v - u) + W )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u in W iff v + W = (v - u) + W )

proof end;

theorem Th53: :: RMOD_2:53

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( v in u + W iff u + W = v + W )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( v in u + W iff u + W = v + W )

proof end;

theorem Th54: :: RMOD_2:54

for R being Ring

for V being RightMod of R

for u, v1, v2 being Vector of V

for W being Submodule of V st u in v1 + W & u in v2 + W holds

v1 + W = v2 + W

for V being RightMod of R

for u, v1, v2 being Vector of V

for W being Submodule of V st u in v1 + W & u in v2 + W holds

v1 + W = v2 + W

proof end;

theorem Th55: :: RMOD_2:55

for R being Ring

for a being Scalar of R

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

v * a in v + W

for a being Scalar of R

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

v * a in v + W

proof end;

theorem :: RMOD_2:56

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

- v in v + W

for V being RightMod of R

for v being Vector of V

for W being Submodule of V st v in W holds

- v in v + W

proof end;

theorem Th57: :: RMOD_2:57

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u + v in v + W iff u in W )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u + v in v + W iff u in W )

proof end;

theorem :: RMOD_2:58

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( v - u in v + W iff u in W )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( v - u in v + W iff u in W )

proof end;

theorem :: RMOD_2:59

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u in v + W iff ex v1 being Vector of V st

( v1 in W & u = v - v1 ) )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V holds

( u in v + W iff ex v1 being Vector of V st

( v1 in W & u = v - v1 ) )

proof end;

theorem Th60: :: RMOD_2:60

for R being Ring

for V being RightMod of R

for v1, v2 being Vector of V

for W being Submodule of V holds

( ex v being Vector of V st

( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )

for V being RightMod of R

for v1, v2 being Vector of V

for W being Submodule of V holds

( ex v being Vector of V st

( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )

proof end;

theorem Th61: :: RMOD_2:61

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st v + W = u + W holds

ex v1 being Vector of V st

( v1 in W & v + v1 = u )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st v + W = u + W holds

ex v1 being Vector of V st

( v1 in W & v + v1 = u )

proof end;

theorem Th62: :: RMOD_2:62

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st v + W = u + W holds

ex v1 being Vector of V st

( v1 in W & v - v1 = u )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V st v + W = u + W holds

ex v1 being Vector of V st

( v1 in W & v - v1 = u )

proof end;

theorem Th63: :: RMOD_2:63

for R being Ring

for V being RightMod of R

for v being Vector of V

for W1, W2 being strict Submodule of V holds

( v + W1 = v + W2 iff W1 = W2 )

for V being RightMod of R

for v being Vector of V

for W1, W2 being strict Submodule of V holds

( v + W1 = v + W2 iff W1 = W2 )

proof end;

theorem Th64: :: RMOD_2:64

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds

W1 = W2

for V being RightMod of R

for u, v being Vector of V

for W1, W2 being strict Submodule of V st v + W1 = u + W2 holds

W1 = W2

proof end;

theorem :: RMOD_2:65

for R being Ring

for V being RightMod of R

for v being Vector of V

for W being Submodule of V ex C being Coset of W st v in C

for V being RightMod of R

for v being Vector of V

for W being Submodule of V ex C being Coset of W st v in C

proof end;

theorem :: RMOD_2:66

for R being Ring

for V being RightMod of R

for W being Submodule of V

for C being Coset of W holds

( C is linearly-closed iff C = the carrier of W )

for V being RightMod of R

for W being Submodule of V

for C being Coset of W holds

( C is linearly-closed iff C = the carrier of W )

proof end;

theorem :: RMOD_2:67

for R being Ring

for V being RightMod of R

for W1, W2 being strict Submodule of V

for C1 being Coset of W1

for C2 being Coset of W2 st C1 = C2 holds

W1 = W2

for V being RightMod of R

for W1, W2 being strict Submodule of V

for C1 being Coset of W1

for C2 being Coset of W2 st C1 = C2 holds

W1 = W2

proof end;

theorem :: RMOD_2:69

for R being Ring

for V being RightMod of R

for V1 being Subset of V st V1 is Coset of (0). V holds

ex v being Vector of V st V1 = {v}

for V being RightMod of R

for V1 being Subset of V st V1 is Coset of (0). V holds

ex v being Vector of V st V1 = {v}

proof end;

theorem :: RMOD_2:70

for R being Ring

for V being RightMod of R

for W being Submodule of V holds the carrier of W is Coset of W

for V being RightMod of R

for W being Submodule of V holds the carrier of W is Coset of W

proof end;

theorem :: RMOD_2:72

for R being Ring

for V being RightMod of R

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

for V being RightMod of R

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

proof end;

theorem :: RMOD_2:73

for R being Ring

for V being RightMod of R

for W being Submodule of V

for C being Coset of W holds

( 0. V in C iff C = the carrier of W )

for V being RightMod of R

for W being Submodule of V

for C being Coset of W holds

( 0. V in C iff C = the carrier of W )

proof end;

theorem Th74: :: RMOD_2:74

for R being Ring

for V being RightMod of R

for u being Vector of V

for W being Submodule of V

for C being Coset of W holds

( u in C iff C = u + W )

for V being RightMod of R

for u being Vector of V

for W being Submodule of V

for C being Coset of W holds

( u in C iff C = u + W )

proof end;

theorem :: RMOD_2:75

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for C being Coset of W st u in C & v in C holds

ex v1 being Vector of V st

( v1 in W & u + v1 = v )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for C being Coset of W st u in C & v in C holds

ex v1 being Vector of V st

( v1 in W & u + v1 = v )

proof end;

theorem :: RMOD_2:76

for R being Ring

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for C being Coset of W st u in C & v in C holds

ex v1 being Vector of V st

( v1 in W & u - v1 = v )

for V being RightMod of R

for u, v being Vector of V

for W being Submodule of V

for C being Coset of W st u in C & v in C holds

ex v1 being Vector of V st

( v1 in W & u - v1 = v )

proof end;

theorem :: RMOD_2:77

for R being Ring

for V being RightMod of R

for v1, v2 being Vector of V

for W being Submodule of V holds

( ex C being Coset of W st

( v1 in C & v2 in C ) iff v1 - v2 in W )

for V being RightMod of R

for v1, v2 being Vector of V

for W being Submodule of V holds

( ex C being Coset of W st

( v1 in C & v2 in C ) iff v1 - v2 in W )

proof end;

theorem :: RMOD_2:78

for R being Ring

for V being RightMod of R

for u being Vector of V

for W being Submodule of V

for B, C being Coset of W st u in B & u in C holds

B = C

for V being RightMod of R

for u being Vector of V

for W being Submodule of V

for B, C being Coset of W st u in B & u in C holds

B = C

proof end;