:: RMOD_2 semantic presentation

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Subset of c₂;
attr a₃ is lineary-closed means :Def1: :: RMOD_2:def 1
( ( for b₁, b₂ being Vector of a₂ st b₁ in a₃ & b₂ in a₃ holds
b₁ + b₂ in a₃ ) & ( for b₁ being Scalar of a₁
for b₂ being Vector of a₂ st b₂ in a₃ holds
b₂ * b₁ in a₃ ) );

end;

:: deftheorem Def1 defines lineary-closed RMOD_2:def 1 :

theorem Th1: :: RMOD_2:1

canceled;

theorem Th2: :: RMOD_2:2

canceled;

theorem Th3: :: RMOD_2:3

canceled;

theorem Th4: :: RMOD_2:4

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st b₃ <> {} & b₃ is lineary-closed holds
0. b₂ in b₃

proof end;

theorem Th5: :: RMOD_2:5

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st b₃ is lineary-closed holds
for b₄ being Vector of b₂ st b₄ in b₃ holds
- b₄ in b₃

proof end;

theorem Th6: :: RMOD_2:6

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st b₃ is lineary-closed holds
for b₄, b₅ being Vector of b₂ st b₄ in b₃ & b₅ in b₃ holds
b₄ - b₅ in b₃

proof end;

theorem Th7: :: RMOD_2:7

for b₁ being Ring
for b₂ being RightMod of b₁ holds {(0. b₂)} is lineary-closed

proof end;

theorem Th8: :: RMOD_2:8

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st the carrier of b₂ = b₃ holds
b₃ is lineary-closed

proof end;

theorem Th9: :: RMOD_2:9

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄, b₅ being Subset of b₂ st b₃ is lineary-closed & b₄ is lineary-closed & b₅ = { (b₆ + b₇) where B is Vector of b₂, B is Vector of b₂ : ( b₆ in b₃ & b₇ in b₄ ) } holds
b₅ is lineary-closed

proof end;

theorem Th10: :: RMOD_2:10

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Subset of b₂ st b₃ is lineary-closed & b₄ is lineary-closed holds
b₃ /\ b₄ is lineary-closed

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
mode Submodule of c₂ -> RightMod of a₁ means :Def2: :: RMOD_2:def 2
( the carrier of a₃ c= the carrier of a₂ & the Zero of a₃ = the Zero of a₂ & the add of a₃ = the add of a₂ | [:the carrier of a₃,the carrier of a₃:] & the rmult of a₃ = the rmult of a₂ | [:the carrier of a₃,the carrier of a₁:] );
existence

proof end;

end;

:: deftheorem Def2 defines Submodule RMOD_2:def 2 :

theorem Th11: :: RMOD_2:11

canceled;

theorem Th12: :: RMOD_2:12

canceled;

theorem Th13: :: RMOD_2:13

canceled;

theorem Th14: :: RMOD_2:14

canceled;

theorem Th15: :: RMOD_2:15

canceled;

theorem Th16: :: RMOD_2:16

for b₁ being set
for b₂ being Ring
for b₃ being RightMod of b₂
for b₄, b₅ being Submodule of b₃ st b₁ in b₄ & b₄ is Submodule of b₅ holds
b₁ in b₅

proof end;

theorem Th17: :: RMOD_2:17

for b₁ being set
for b₂ being Ring
for b₃ being RightMod of b₂
for b₄ being Submodule of b₃ st b₁ in b₄ holds
b₁ in b₃

proof end;

theorem Th18: :: RMOD_2:18

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂
for b₄ being Vector of b₃ holds b₄ is Vector of b₂

proof end;

theorem Th19: :: RMOD_2:19

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds 0. b₃ = 0. b₂ by Def2;

theorem Th20: :: RMOD_2:20

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Submodule of b₂ holds 0. b₃ = 0. b₄

proof end;

theorem Th21: :: RMOD_2:21

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂
for b₆, b₇ being Vector of b₅ st b₆ = b₃ & b₇ = b₄ holds
b₆ + b₇ = b₃ + b₄

proof end;

theorem Th22: :: RMOD_2:22

for b₁ being Ring
for b₂ being Scalar of b₁
for b₃ being RightMod of b₁
for b₄ being Vector of b₃
for b₅ being Submodule of b₃
for b₆ being Vector of b₅ st b₆ = b₄ holds
b₆ * b₂ = b₄ * b₂

proof end;

theorem Th23: :: RMOD_2:23

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂
for b₅ being Vector of b₄ st b₅ = b₃ holds
- b₃ = - b₅

proof end;

theorem Th24: :: RMOD_2:24

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂
for b₆, b₇ being Vector of b₅ st b₆ = b₃ & b₇ = b₄ holds
b₆ - b₇ = b₃ - b₄

proof end;

Lemma13: for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂
for b₄ being Submodule of b₂ st the carrier of b₄ = b₃ holds
b₃ is lineary-closed

proof end;

theorem Th25: :: RMOD_2:25

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds 0. b₂ in b₃

proof end;

theorem Th26: :: RMOD_2:26

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Submodule of b₂ holds 0. b₃ in b₄

proof end;

theorem Th27: :: RMOD_2:27

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds 0. b₃ in b₂

proof end;

theorem Th28: :: RMOD_2:28

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ st b₃ in b₅ & b₄ in b₅ holds
b₃ + b₄ in b₅

proof end;

theorem Th29: :: RMOD_2:29

for b₁ being Ring
for b₂ being Scalar of b₁
for b₃ being RightMod of b₁
for b₄ being Vector of b₃
for b₅ being Submodule of b₃ st b₄ in b₅ holds
b₄ * b₂ in b₅

proof end;

theorem Th30: :: RMOD_2:30

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ st b₃ in b₄ holds
- b₃ in b₄

proof end;

theorem Th31: :: RMOD_2:31

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ st b₃ in b₅ & b₄ in b₅ holds
b₃ - b₄ in b₅

proof end;

theorem Th32: :: RMOD_2:32

for b₁ being Ring
for b₂ being RightMod of b₁ holds b₂ is Submodule of b₂

proof end;

theorem Th33: :: RMOD_2:33

for b₁ being Ring
for b₂, b₃ being strict RightMod of b₁ st b₃ is Submodule of b₂ & b₂ is Submodule of b₃ holds
b₃ = b₂

proof end;

registration

let c₁ be Ring;
let c₂ be RightMod of c₁;
cluster strict Submodule of a₂;
existence

proof end;

end;

theorem Th34: :: RMOD_2:34

for b₁ being Ring
for b₂, b₃, b₄ being RightMod of b₁ st b₂ is Submodule of b₃ & b₃ is Submodule of b₄ holds
b₂ is Submodule of b₄

proof end;

theorem Th35: :: RMOD_2:35

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Submodule of b₂ st the carrier of b₃ c= the carrier of b₄ holds
b₃ is Submodule of b₄

proof end;

theorem Th36: :: RMOD_2:36

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Submodule of b₂ st ( for b₅ being Vector of b₂ st b₅ in b₃ holds
b₅ in b₄ ) holds
b₃ is Submodule of b₄

proof end;

theorem Th37: :: RMOD_2:37

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being strict Submodule of b₂ st the carrier of b₃ = the carrier of b₄ holds
b₃ = b₄

proof end;

theorem Th38: :: RMOD_2:38

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being strict Submodule of b₂ st ( for b₅ being Vector of b₂ holds
( b₅ in b₃ iff b₅ in b₄ ) ) holds
b₃ = b₄

proof end;

theorem Th39: :: RMOD_2:39

for b₁ being Ring
for b₂ being strict RightMod of b₁
for b₃ being strict Submodule of b₂ st the carrier of b₃ = the carrier of b₂ holds
b₃ = b₂

proof end;

theorem Th40: :: RMOD_2:40

for b₁ being Ring
for b₂ being strict RightMod of b₁
for b₃ being strict Submodule of b₂ st ( for b₄ being Vector of b₂ holds b₄ in b₃ ) holds
b₃ = b₂

proof end;

theorem Th41: :: RMOD_2:41

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂
for b₄ being Submodule of b₂ st the carrier of b₄ = b₃ holds
b₃ is lineary-closed by Lemma13;

theorem Th42: :: RMOD_2:42

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st b₃ <> {} & b₃ is lineary-closed holds
ex b₄ being strict Submodule of b₂ st b₃ = the carrier of b₄

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
func (0). c₂ -> strict Submodule of a₂ means :Def3: :: RMOD_2:def 3
the carrier of a₃ = {(0. a₂)};
correctness

proof end;

end;

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

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
func (Omega). c₂ -> strict Submodule of a₂ equals :: RMOD_2:def 4
RightModStr(# the carrier of a₂,the add of a₂,the Zero of a₂,the rmult of a₂ #);
coherence

proof end;

end;

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

theorem Th43: :: RMOD_2:43

canceled;

theorem Th44: :: RMOD_2:44

canceled;

theorem Th45: :: RMOD_2:45

canceled;

theorem Th46: :: RMOD_2:46

for b₁ being set
for b₂ being Ring
for b₃ being RightMod of b₂ holds
( b₁ in (0). b₃ iff b₁ = 0. b₃ )

proof end;

theorem Th47: :: RMOD_2:47

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds (0). b₃ = (0). b₂

proof end;

theorem Th48: :: RMOD_2:48

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Submodule of b₂ holds (0). b₃ = (0). b₄

proof end;

theorem Th49: :: RMOD_2:49

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds (0). b₃ is Submodule of b₂ by Th34;

theorem Th50: :: RMOD_2:50

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds (0). b₂ is Submodule of b₃

proof end;

theorem Th51: :: RMOD_2:51

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Submodule of b₂ holds (0). b₃ is Submodule of b₄

proof end;

theorem Th52: :: RMOD_2:52

canceled;

theorem Th53: :: RMOD_2:53

for b₁ being Ring
for b₂ being strict RightMod of b₁ holds b₂ is Submodule of (Omega). b₂ ;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Vector of c₂;
let c₄ be Submodule of c₂;
func c₃ + c₄ -> Subset of a₂ equals :: RMOD_2:def 5
{ (a₃ + b₁) where B is Vector of a₂ : b₁ in a₄ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines + RMOD_2:def 5 :

Lemma29: for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds (0. b₂) + b₃ = the carrier of b₃

proof end;

definition

let c₁ be Ring;
let c₂ be RightMod of c₁;
let c₃ be Submodule of c₂;
mode Coset of c₃ -> Subset of a₂ means :Def6: :: RMOD_2:def 6
ex b₁ being Vector of a₂ st a₄ = b₁ + a₃;
existence

proof end;

end;

:: deftheorem Def6 defines Coset RMOD_2:def 6 :

theorem Th54: :: RMOD_2:54

canceled;

theorem Th55: :: RMOD_2:55

canceled;

theorem Th56: :: RMOD_2:56

canceled;

theorem Th57: :: RMOD_2:57

for b₁ being set
for b₂ being Ring
for b₃ being RightMod of b₂
for b₄ being Vector of b₃
for b₅ being Submodule of b₃ holds
( b₁ in b₄ + b₅ iff ex b₆ being Vector of b₃ st
( b₆ in b₅ & b₁ = b₄ + b₆ ) )

proof end;

theorem Th58: :: RMOD_2:58

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ holds
( 0. b₂ in b₃ + b₄ iff b₃ in b₄ )

proof end;

theorem Th59: :: RMOD_2:59

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ holds b₃ in b₃ + b₄

proof end;

theorem Th60: :: RMOD_2:60

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds (0. b₂) + b₃ = the carrier of b₃ by Lemma29;

theorem Th61: :: RMOD_2:61

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂ holds b₃ + ((0). b₂) = {b₃}

proof end;

Lemma35: for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ holds
( b₃ in b₄ iff b₃ + b₄ = the carrier of b₄ )

proof end;

theorem Th62: :: RMOD_2:62

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂ holds b₃ + ((Omega). b₂) = the carrier of b₂

proof end;

theorem Th63: :: RMOD_2:63

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ holds
( 0. b₂ in b₃ + b₄ iff b₃ + b₄ = the carrier of b₄ )

proof end;

theorem Th64: :: RMOD_2:64

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ holds
( b₃ in b₄ iff b₃ + b₄ = the carrier of b₄ ) by Lemma35;

theorem Th65: :: RMOD_2:65

for b₁ being Ring
for b₂ being Scalar of b₁
for b₃ being RightMod of b₁
for b₄ being Vector of b₃
for b₅ being Submodule of b₃ st b₄ in b₅ holds
(b₄ * b₂) + b₅ = the carrier of b₅

proof end;

theorem Th66: :: RMOD_2:66

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( b₃ in b₅ iff b₄ + b₅ = (b₄ + b₃) + b₅ )

proof end;

theorem Th67: :: RMOD_2:67

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( b₃ in b₅ iff b₄ + b₅ = (b₄ - b₃) + b₅ )

proof end;

theorem Th68: :: RMOD_2:68

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( b₃ in b₄ + b₅ iff b₄ + b₅ = b₃ + b₅ )

proof end;

theorem Th69: :: RMOD_2:69

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄, b₅ being Vector of b₂
for b₆ being Submodule of b₂ st b₃ in b₄ + b₆ & b₃ in b₅ + b₆ holds
b₄ + b₆ = b₅ + b₆

proof end;

theorem Th70: :: RMOD_2:70

for b₁ being Ring
for b₂ being Scalar of b₁
for b₃ being RightMod of b₁
for b₄ being Vector of b₃
for b₅ being Submodule of b₃ st b₄ in b₅ holds
b₄ * b₂ in b₄ + b₅

proof end;

theorem Th71: :: RMOD_2:71

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ st b₃ in b₄ holds
- b₃ in b₃ + b₄

proof end;

theorem Th72: :: RMOD_2:72

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( b₃ + b₄ in b₄ + b₅ iff b₃ in b₅ )

proof end;

theorem Th73: :: RMOD_2:73

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( b₃ - b₄ in b₃ + b₅ iff b₄ in b₅ )

proof end;

theorem Th74: :: RMOD_2:74

canceled;

theorem Th75: :: RMOD_2:75

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( b₃ in b₄ + b₅ iff ex b₆ being Vector of b₂ st
( b₆ in b₅ & b₃ = b₄ - b₆ ) )

proof end;

theorem Th76: :: RMOD_2:76

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( ex b₆ being Vector of b₂ st
( b₃ in b₆ + b₅ & b₄ in b₆ + b₅ ) iff b₃ - b₄ in b₅ )

proof end;

theorem Th77: :: RMOD_2:77

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ st b₃ + b₅ = b₄ + b₅ holds
ex b₆ being Vector of b₂ st
( b₆ in b₅ & b₃ + b₆ = b₄ )

proof end;

theorem Th78: :: RMOD_2:78

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ st b₃ + b₅ = b₄ + b₅ holds
ex b₆ being Vector of b₂ st
( b₆ in b₅ & b₃ - b₆ = b₄ )

proof end;

theorem Th79: :: RMOD_2:79

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄, b₅ being strict Submodule of b₂ holds
( b₃ + b₄ = b₃ + b₅ iff b₄ = b₅ )

proof end;

theorem Th80: :: RMOD_2:80

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅, b₆ being strict Submodule of b₂ st b₃ + b₅ = b₄ + b₆ holds
b₅ = b₆

proof end;

theorem Th81: :: RMOD_2:81

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂ ex b₅ being Coset of b₄ st b₃ in b₅

proof end;

theorem Th82: :: RMOD_2:82

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂
for b₄ being Coset of b₃ holds
( b₄ is lineary-closed iff b₄ = the carrier of b₃ )

proof end;

theorem Th83: :: RMOD_2:83

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being strict Submodule of b₂
for b₅ being Coset of b₃
for b₆ being Coset of b₄ st b₅ = b₆ holds
b₃ = b₄

proof end;

theorem Th84: :: RMOD_2:84

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂ holds {b₃} is Coset of (0). b₂

proof end;

theorem Th85: :: RMOD_2:85

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st b₃ is Coset of (0). b₂ holds
ex b₄ being Vector of b₂ st b₃ = {b₄}

proof end;

theorem Th86: :: RMOD_2:86

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂ holds the carrier of b₃ is Coset of b₃

proof end;

theorem Th87: :: RMOD_2:87

for b₁ being Ring
for b₂ being RightMod of b₁ holds the carrier of b₂ is Coset of (Omega). b₂

proof end;

theorem Th88: :: RMOD_2:88

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Subset of b₂ st b₃ is Coset of (Omega). b₂ holds
b₃ = the carrier of b₂

proof end;

theorem Th89: :: RMOD_2:89

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Submodule of b₂
for b₄ being Coset of b₃ holds
( 0. b₂ in b₄ iff b₄ = the carrier of b₃ )

proof end;

theorem Th90: :: RMOD_2:90

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂
for b₅ being Coset of b₄ holds
( b₃ in b₅ iff b₅ = b₃ + b₄ )

proof end;

theorem Th91: :: RMOD_2:91

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂
for b₆ being Coset of b₅ st b₃ in b₆ & b₄ in b₆ holds
ex b₇ being Vector of b₂ st
( b₇ in b₅ & b₃ + b₇ = b₄ )

proof end;

theorem Th92: :: RMOD_2:92

proof end;

theorem Th93: :: RMOD_2:93

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃, b₄ being Vector of b₂
for b₅ being Submodule of b₂ holds
( ex b₆ being Coset of b₅ st
( b₃ in b₆ & b₄ in b₆ ) iff b₃ - b₄ in b₅ )

proof end;

theorem Th94: :: RMOD_2:94

for b₁ being Ring
for b₂ being RightMod of b₁
for b₃ being Vector of b₂
for b₄ being Submodule of b₂
for b₅, b₆ being Coset of b₄ st b₃ in b₅ & b₃ in b₆ holds
b₅ = b₆

proof end;