:: MODCAT_1 semantic presentation

begin


definition
let R be Ring;
mode LeftMod_DOMAIN of R ->  non empty set  means :Def1: :: MODCAT_1:def 1
 for x being Element of it holds x is strict LeftMod of R;
existence
 ex b1 being non empty set st
for x being Element of b1 holds x is strict LeftMod of R
proof
set D = {(TrivialLMod R)};
take  {(TrivialLMod R)} ; ::_thesis: for x being Element of {(TrivialLMod R)} holds x is strict LeftMod of R
thus  for x being Element of {(TrivialLMod R)} holds x is strict LeftMod of R by TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def_1_:_
 for R being Ring
for b2 being non empty set holds
( b2 is LeftMod_DOMAIN of R iff for x being Element of b2 holds x is strict LeftMod of R );

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
:: original: Element
redefine mode Element of V ->  LeftMod of R;
coherence
 for b1 being Element of V holds b1 is LeftMod of R by Def1;
end;

registration
let R be Ring;
let V be LeftMod_DOMAIN of R;
cluster non empty right_complementable V96() V97() V98() strict V149(R) V150(R) V151(R) V152(R) for Element of V;
existence
 ex b1 being Element of V st b1 is strict
proof
set e = the Element of V;
take  the Element of V ; ::_thesis: the Element of V is strict
thus  the Element of V is strict by Def1; ::_thesis: verum
end;
end;

definition
let R be Ring;
mode LModMorphism_DOMAIN of R ->  non empty set  means :Def2: :: MODCAT_1:def 2
 for x being Element of it holds x is strict LModMorphism of R;
existence
 ex b1 being non empty set st
for x being Element of b1 holds x is strict LModMorphism of R
proof
set G = the LeftMod of R;
take  {(ID the LeftMod of R)} ; ::_thesis: for x being Element of {(ID the LeftMod of R)} holds x is strict LModMorphism of R
let x be Element of {(ID the LeftMod of R)}; ::_thesis: x is strict LModMorphism of R
thus  x is strict LModMorphism of R by TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines LModMorphism_DOMAIN MODCAT_1:def_2_:_
 for R being Ring
for b2 being non empty set holds
( b2 is LModMorphism_DOMAIN of R iff for x being Element of b2 holds x is strict LModMorphism of R );

definition
let R be Ring;
let M be LModMorphism_DOMAIN of R;
:: original: Element
redefine mode Element of M ->  LModMorphism of R;
coherence
 for b1 being Element of M holds b1 is LModMorphism of R by Def2;
end;

registration
let R be Ring;
let M be LModMorphism_DOMAIN of R;
cluster strict LModMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proof
set e = the Element of M;
take  the Element of M ; ::_thesis: the Element of M is strict
thus  the Element of M is strict by Def2; ::_thesis: verum
end;
end;

theorem Th1: :: MODCAT_1:1
for R being Ring
for f being strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R
proof
let R be Ring; ::_thesis: for f being strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R
let f be strict LModMorphism of R; ::_thesis: {f} is LModMorphism_DOMAIN of R
 for x being Element of {f} holds x is strict LModMorphism of R by TARSKI:def_1;
hence  {f} is LModMorphism_DOMAIN of R by Def2; ::_thesis: verum
end;

definition
let R be Ring;
let G, H be LeftMod of R;
mode LModMorphism_DOMAIN of G,H ->  LModMorphism_DOMAIN of R means :Def3: :: MODCAT_1:def 3
 for x being Element of it holds x is strict Morphism of G,H;
existence
 ex b1 being LModMorphism_DOMAIN of R st
for x being Element of b1 holds x is strict Morphism of G,H
proof
reconsider D = {(ZERO (G,H))} as LModMorphism_DOMAIN of R by Th1;
take  D ; ::_thesis: for x being Element of D holds x is strict Morphism of G,H
thus  for x being Element of D holds x is strict Morphism of G,H by TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def_3_:_
 for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of R holds
( b4 is LModMorphism_DOMAIN of G,H iff for x being Element of b4 holds x is strict Morphism of G,H );

theorem Th2: :: MODCAT_1:2
for D being non empty set
for R being Ring
for G, H being LeftMod of R holds
( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
proof
let D be non empty set ; ::_thesis: for R being Ring
for G, H being LeftMod of R holds
( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
let R be Ring; ::_thesis: for G, H being LeftMod of R holds
( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
let G, H be LeftMod of R; ::_thesis: ( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
thus  ( D is LModMorphism_DOMAIN of G,H implies for x being Element of D holds x is strict Morphism of G,H ) by Def3; ::_thesis: ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is LModMorphism_DOMAIN of G,H )
thus  ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is LModMorphism_DOMAIN of G,H ) ::_thesis: verum
proof
assume A1: for x being Element of D holds x is strict Morphism of G,H ; ::_thesis: D is LModMorphism_DOMAIN of G,H
then  for x being Element of D holds x is strict LModMorphism of R ;
then reconsider D9 = D as LModMorphism_DOMAIN of R by Def2;
 for x being Element of D9 holds x is strict Morphism of G,H by A1;
hence  D is LModMorphism_DOMAIN of G,H by Def3; ::_thesis: verum
end;
end;

theorem :: MODCAT_1:3
for R being Ring
for G, H being LeftMod of R
for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
proof
let R be Ring; ::_thesis: for G, H being LeftMod of R
for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
let G, H be LeftMod of R; ::_thesis: for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
let f be strict Morphism of G,H; ::_thesis: {f} is LModMorphism_DOMAIN of G,H
 for x being Element of {f} holds x is strict Morphism of G,H by TARSKI:def_1;
hence  {f} is LModMorphism_DOMAIN of G,H by Th2; ::_thesis: verum
end;

definition
let R be Ring;
let G, H be LeftMod of R;
func Morphs (G,H) ->  LModMorphism_DOMAIN of G,H means :Def4: :: MODCAT_1:def 4
 for x being set holds
( x in it iff x is strict Morphism of G,H );
existence
 ex b1 being LModMorphism_DOMAIN of G,H st
for x being set holds
( x in b1 iff x is strict Morphism of G,H )
proof
 ZeroMap (G,H) is Element of Funcs ( the carrier of G, the carrier of H) by FUNCT_2:8;
then reconsider f0 = ZeroMap (G,H) as Element of Maps (G,H) by GRCAT_1:def_21;
set D =  {  LModMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : ( f is additive & f is homogeneous )  }  ;
 LModMorphismStr(# G,H,f0 #) in  {  LModMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : ( f is additive & f is homogeneous )  }  ;
then reconsider D =  {  LModMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : ( f is additive & f is homogeneous )  }  as non empty set ;
A1: for x being set st x is strict Morphism of G,H holds
x in D
proof
let x be set ; ::_thesis: ( x is strict Morphism of G,H implies x in D )
assume  x is strict Morphism of G,H ; ::_thesis: x in D
then reconsider x = x as strict Morphism of G,H ;
 dom x = G by MOD_2:def_8;
then A2: the Dom of x = G by MOD_2:def_3;
A3: cod x = H by MOD_2:def_8;
then  the Cod of x = H by MOD_2:def_4;
then reconsider f = the Fun of x as Function of G,H by A2;
 f is Element of Funcs ( the carrier of G, the carrier of H) by FUNCT_2:8;
then reconsider g = f as Element of Maps (G,H) by GRCAT_1:def_21;
 ( the Fun of x is additive & the Fun of x is homogeneous & x = LModMorphismStr(# G,H,g #) ) by A3, A2, MOD_2:4, MOD_2:def_4;
hence  x in D ; ::_thesis: verum
end;
A4: for x being set st x in D holds
x is strict Morphism of G,H
proof
let x be set ; ::_thesis: ( x in D implies x is strict Morphism of G,H )
assume  x in D ; ::_thesis: x is strict Morphism of G,H
then  ex f being Element of Maps (G,H) st
( x = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) ;
hence  x is strict Morphism of G,H by MOD_2:6; ::_thesis: verum
end;
then  for x being Element of D holds x is strict Morphism of G,H ;
then reconsider D = D as LModMorphism_DOMAIN of G,H by Th2;
take  D ; ::_thesis: for x being set holds
( x in D iff x is strict Morphism of G,H )
thus  for x being set holds
( x in D iff x is strict Morphism of G,H ) by A4, A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being LModMorphism_DOMAIN of G,H st ( for x being set holds
( x in b1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff x is strict Morphism of G,H ) ) holds
b1 = b2
proof
let D1, D2 be LModMorphism_DOMAIN of G,H; ::_thesis: ( ( for x being set holds
( x in D1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in D2 iff x is strict Morphism of G,H ) ) implies D1 = D2 )
assume that
A5: for x being set holds
( x in D1 iff x is strict Morphism of G,H ) and
A6: for x being set holds
( x in D2 iff x is strict Morphism of G,H ) ; ::_thesis: D1 = D2
 for x being set holds
( x in D1 iff x in D2 )
proof
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
hereby  ::_thesis: ( x in D2 implies x in D1 )
assume  x in D1 ; ::_thesis: x in D2
then  x is strict Morphism of G,H by A5;
hence  x in D2 by A6; ::_thesis: verum
end;
assume  x in D2 ; ::_thesis: x in D1
then  x is strict Morphism of G,H by A6;
hence  x in D1 by A5; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Morphs MODCAT_1:def_4_:_
 for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism_DOMAIN of G,H holds
( b4 = Morphs (G,H) iff for x being set holds
( x in b4 iff x is strict Morphism of G,H ) );

definition
let R be Ring;
let G, H be LeftMod of R;
let M be LModMorphism_DOMAIN of G,H;
:: original: Element
redefine mode Element of M ->  Morphism of G,H;
coherence
 for b1 being Element of M holds b1 is Morphism of G,H by Def3;
end;

definition
let x, y be set ;
let R be Ring;
pred GO x,y,R means :Def5: :: MODCAT_1:def 5
 ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of R st
( y = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) );
end;

:: deftheorem Def5 defines GO MODCAT_1:def_5_:_
 for x, y being set
for R being Ring holds
( GO x,y,R iff ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of R st
( y = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) ) );

theorem Th4: :: MODCAT_1:4
for R being Ring
for x, y1, y2 being set st GO x,y1,R & GO x,y2,R holds
y1 = y2
proof
let R be Ring; ::_thesis: for x, y1, y2 being set st GO x,y1,R & GO x,y2,R holds
y1 = y2
let x, y1, y2 be set ; ::_thesis: ( GO x,y1,R & GO x,y2,R implies y1 = y2 )
assume that
A1: GO x,y1,R and
A2: GO x,y2,R ; ::_thesis: y1 = y2
consider a1, a2 being set  such that
A3: x = [a1,a2] and
A4: ex G being strict LeftMod of R st
( y1 = G & a1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & a2 = the lmult of G ) by A1, Def5;
consider G1 being strict LeftMod of R such that
A5: y1 = G1 and
A6: a1 = addLoopStr(# the carrier of G1, the addF of G1, the ZeroF of G1 #) and
A7: a2 = the lmult of G1 by A4;
consider b1, b2 being set  such that
A8: x = [b1,b2] and
A9: ex G being strict LeftMod of R st
( y2 = G & b1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & b2 = the lmult of G ) by A2, Def5;
consider G2 being strict LeftMod of R such that
A10: y2 = G2 and
A11: b1 = addLoopStr(# the carrier of G2, the addF of G2, the ZeroF of G2 #) and
A12: b2 = the lmult of G2 by A9;
 addLoopStr(# the carrier of G1, the addF of G1, the ZeroF of G1 #) = addLoopStr(# the carrier of G2, the addF of G2, the ZeroF of G2 #) by A3, A8, A6, A11, XTUPLE_0:1;
hence  y1 = y2 by A3, A8, A5, A7, A10, A12, XTUPLE_0:1; ::_thesis: verum
end;

theorem Th5: :: MODCAT_1:5
for R being Ring
for UN being Universe ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x, TrivialLMod R,R )
proof
let R be Ring; ::_thesis: for UN being Universe ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x, TrivialLMod R,R )
let UN be Universe; ::_thesis: ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x, TrivialLMod R,R )
set T = TrivialLMod R;
A1: TrivialLMod R = VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) by MOD_2:def_1;
then reconsider x1 = addLoopStr(# the carrier of (TrivialLMod R), the addF of (TrivialLMod R), the ZeroF of (TrivialLMod R) #) as Element of GroupObjects UN by GRCAT_1:29;
reconsider f1 = the lmult of (TrivialLMod R) as Function of [: the carrier of R,1:],1 by A1;
reconsider x2 = f1 as Element of Funcs ([: the carrier of R,1:],1) by FUNCT_2:8;
take x = [x1,x2]; ::_thesis: ( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x, TrivialLMod R,R )
thus  x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  ; ::_thesis: GO x, TrivialLMod R,R
thus  GO x, TrivialLMod R,R by Def5; ::_thesis: verum
end;

definition
let UN be Universe;
let R be Ring;
func LModObjects (UN,R) ->  set  means :Def6: :: MODCAT_1:def 6
 for y being set holds
( y in it iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) )
proof
defpred S1[ set , set ] means  GO $1,$2,R;
set N =  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  ;
A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by Th4;
consider Y being set  such that
A2: for y being set holds
( y in Y iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & S1[x,y] ) ) from TARSKI:sch_1(A1);
take  Y ; ::_thesis: for y being set holds
( y in Y iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) )
thus  for y being set holds
( y in Y iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) ) holds
b1 = b2
proof
set N =  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  ;
let Y1, Y2 be set ; ::_thesis: ( ( for y being set holds
( y in Y1 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) ) & ( for y being set holds
( y in Y2 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) ) implies Y1 = Y2 )
assume that
A3: for y being set holds
( y in Y1 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) and
A4: for y being set holds
( y in Y2 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) ; ::_thesis: Y1 = Y2
now__::_thesis:_for_y_being_set_holds_
(_y_in_Y1_iff_y_in_Y2_)
let y be set ; ::_thesis: ( y in Y1 iff y in Y2 )
 ( y in Y1 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) by A3;
hence  ( y in Y1 iff y in Y2 ) by A4; ::_thesis: verum
end;
hence  Y1 = Y2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines LModObjects MODCAT_1:def_6_:_
 for UN being Universe
for R being Ring
for b3 being set holds
( b3 = LModObjects (UN,R) iff for y being set holds
( y in b3 iff ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x,y,R ) ) );

theorem Th6: :: MODCAT_1:6
for UN being Universe
for R being Ring holds TrivialLMod R in LModObjects (UN,R)
proof
let UN be Universe; ::_thesis: for R being Ring holds TrivialLMod R in LModObjects (UN,R)
let R be Ring; ::_thesis: TrivialLMod R in LModObjects (UN,R)
 ex x being set st
( x in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  & GO x, TrivialLMod R,R ) by Th5;
hence  TrivialLMod R in LModObjects (UN,R) by Def6; ::_thesis: verum
end;

registration
let UN be Universe;
let R be Ring;
cluster LModObjects (UN,R) ->  non empty ;
coherence
 not LModObjects (UN,R) is empty by Th6;
end;

theorem Th7: :: MODCAT_1:7
for UN being Universe
for R being Ring
for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R
proof
let UN be Universe; ::_thesis: for R being Ring
for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R
let R be Ring; ::_thesis: for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R
let x be Element of LModObjects (UN,R); ::_thesis: x is strict LeftMod of R
set N =  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  ;
consider u being set  such that
 u in  {  [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  and
A1: GO u,x,R by Def6;
 ex a1, a2 being set st
( u = [a1,a2] & ex G being strict LeftMod of R st
( x = G & a1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & a2 = the lmult of G ) ) by A1, Def5;
hence  x is strict LeftMod of R ; ::_thesis: verum
end;

definition
let UN be Universe;
let R be Ring;
:: original: LModObjects
redefine func LModObjects (UN,R) ->  LeftMod_DOMAIN of R;
coherence
 LModObjects (UN,R) is LeftMod_DOMAIN of R
proof
 for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R by Th7;
hence  LModObjects (UN,R) is LeftMod_DOMAIN of R by Def1; ::_thesis: verum
end;
end;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func Morphs V ->  LModMorphism_DOMAIN of R means :Def7: :: MODCAT_1:def 7
 for x being set holds
( x in it iff ex G, H being strict Element of V st x is strict Morphism of G,H );
existence
 ex b1 being LModMorphism_DOMAIN of R st
for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
proof
set G0 = the strict Element of V;
set M = Morphs ( the strict Element of V, the strict Element of V);
set S =  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  ;
 ( ZERO ( the strict Element of V, the strict Element of V) is Element of Morphs ( the strict Element of V, the strict Element of V) & Morphs ( the strict Element of V, the strict Element of V) in  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  ) by Def4;
then reconsider T = union  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  as non empty set by TARSKI:def_4;
A1: for x being set holds
( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H )
proof
let x be set ; ::_thesis: ( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H )
thus  ( x in T implies ex G, H being strict Element of V st x is strict Morphism of G,H ) ::_thesis: ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T )
proof
assume  x in T ; ::_thesis: ex G, H being strict Element of V st x is strict Morphism of G,H
then consider Y being set  such that
A2: x in Y and
A3: Y in  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  by TARSKI:def_4;
consider G, H being strict Element of V such that
A4: Y = Morphs (G,H) by A3;
take  G ; ::_thesis: ex H being strict Element of V st x is strict Morphism of G,H
take  H ; ::_thesis: x is strict Morphism of G,H
thus  x is strict Morphism of G,H by A2, A4, Def4; ::_thesis: verum
end;
thus  ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T ) ::_thesis: verum
proof
given G, H being strict Element of V such that A5: x is strict Morphism of G,H ; ::_thesis: x in T
set M = Morphs (G,H);
A6: Morphs (G,H) in  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  ;
 x in Morphs (G,H) by A5, Def4;
hence  x in T by A6, TARSKI:def_4; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_Element_of_T_holds_x_is_strict_LModMorphism_of_R
let x be Element of T; ::_thesis: x is strict LModMorphism of R
 ex G, H being strict Element of V st x is strict Morphism of G,H by A1;
hence  x is strict LModMorphism of R ; ::_thesis: verum
end;
then reconsider T9 = T as LModMorphism_DOMAIN of R by Def2;
take  T9 ; ::_thesis: for x being set holds
( x in T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
thus  for x being set holds
( x in T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being LModMorphism_DOMAIN of R st ( for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds
b1 = b2
proof
let D1, D2 be LModMorphism_DOMAIN of R; ::_thesis: ( ( for x being set holds
( x in D1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in D2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) implies D1 = D2 )
assume that
A7: for x being set holds
( x in D1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) and
A8: for x being set holds
( x in D2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_x_in_D1_iff_x_in_D2_)
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
 ( x in D1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) by A7;
hence  ( x in D1 iff x in D2 ) by A8; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Morphs MODCAT_1:def_7_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being LModMorphism_DOMAIN of R holds
( b3 = Morphs V iff for x being set holds
( x in b3 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
let F be Element of Morphs V;
func dom' F ->  Element of V equals :: MODCAT_1:def 8
 dom F;
coherence
 dom F is Element of V
proof
consider G, H being strict Element of V such that
A1: F is strict Morphism of G,H by Def7;
reconsider F9 = F as Morphism of G,H by A1;
 dom F9 = G by MOD_2:def_8;
hence  dom F is Element of V ; ::_thesis: verum
end;
func cod' F ->  Element of V equals :: MODCAT_1:def 9
 cod F;
coherence
 cod F is Element of V
proof
consider G, H being strict Element of V such that
A2: F is strict Morphism of G,H by Def7;
reconsider F9 = F as Morphism of G,H by A2;
 cod F9 = H by MOD_2:def_8;
hence  cod F is Element of V ; ::_thesis: verum
end;
end;

:: deftheorem  defines dom' MODCAT_1:def_8_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for F being Element of Morphs V holds dom' F = dom F;

:: deftheorem  defines cod' MODCAT_1:def_9_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for F being Element of Morphs V holds cod' F = cod F;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
let G be Element of V;
func ID G ->  strict Element of Morphs V equals :: MODCAT_1:def 10
 ID G;
coherence
 ID G is strict Element of Morphs V
proof
reconsider G = G as strict Element of V by Def1;
 ID G is strict Element of Morphs V by Def7;
hence  ID G is strict Element of Morphs V ; ::_thesis: verum
end;
end;

:: deftheorem  defines ID MODCAT_1:def_10_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for G being Element of V holds ID G = ID G;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func dom V ->  Function of (Morphs V),V means :Def11: :: MODCAT_1:def 11
 for f being Element of Morphs V holds it . f = dom' f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = dom' f
proof
deffunc H1( Element of Morphs V) ->  Element of V = dom' $1;
consider F being Function of (Morphs V),V such that
A1: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4();
take  F ; ::_thesis: for f being Element of Morphs V holds F . f = dom' f
thus  for f being Element of Morphs V holds F . f = dom' f by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom' f ) & ( for f being Element of Morphs V holds b2 . f = dom' f ) holds
b1 = b2
proof
let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = dom' f ) & ( for f being Element of Morphs V holds F2 . f = dom' f ) implies F1 = F2 )
assume that
A2: for f being Element of Morphs V holds F1 . f = dom' f and
A3: for f being Element of Morphs V holds F2 . f = dom' f ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f
let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f
 F1 . f = dom' f by A2;
hence  F1 . f = F2 . f by A3; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
func cod V ->  Function of (Morphs V),V means :Def12: :: MODCAT_1:def 12
 for f being Element of Morphs V holds it . f = cod' f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = cod' f
proof
deffunc H1( Element of Morphs V) ->  Element of V = cod' $1;
consider F being Function of (Morphs V),V such that
A4: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4();
take  F ; ::_thesis: for f being Element of Morphs V holds F . f = cod' f
thus  for f being Element of Morphs V holds F . f = cod' f by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod' f ) & ( for f being Element of Morphs V holds b2 . f = cod' f ) holds
b1 = b2
proof
let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = cod' f ) & ( for f being Element of Morphs V holds F2 . f = cod' f ) implies F1 = F2 )
assume that
A5: for f being Element of Morphs V holds F1 . f = cod' f and
A6: for f being Element of Morphs V holds F2 . f = cod' f ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f
let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f
 F1 . f = cod' f by A5;
hence  F1 . f = F2 . f by A6; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
canceled;
end;

:: deftheorem Def11 defines dom MODCAT_1:def_11_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of (Morphs V),V holds
( b3 = dom V iff for f being Element of Morphs V holds b3 . f = dom' f );

:: deftheorem Def12 defines cod MODCAT_1:def_12_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being Function of (Morphs V),V holds
( b3 = cod V iff for f being Element of Morphs V holds b3 . f = cod' f );

:: deftheorem  MODCAT_1:def_13_:_
canceled;

theorem Th8: :: MODCAT_1:8
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proof
let R be Ring; ::_thesis: for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
let V be LeftMod_DOMAIN of R; ::_thesis: for g, f being Element of Morphs V st dom' g = cod' f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom' $1 = cod' $2;
let g, f be Element of Morphs V; ::_thesis: ( dom' g = cod' f implies ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
consider G2, G3 being strict Element of V such that
A2: g is strict Morphism of G2,G3 by Def7;
consider G1, G29 being strict Element of V such that
A3: f is strict Morphism of G1,G29 by Def7;
A4: G29 = cod' f by A3, MOD_2:def_8;
 G2 = dom' g by A2, MOD_2:def_8;
hence  ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; ::_thesis: verum
end;

theorem Th9: :: MODCAT_1:9
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
g * f in Morphs V
proof
let R be Ring; ::_thesis: for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom' g = cod' f holds
g * f in Morphs V
let V be LeftMod_DOMAIN of R; ::_thesis: for g, f being Element of Morphs V st dom' g = cod' f holds
g * f in Morphs V
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom' $1 = cod' $2;
let g, f be Element of Morphs V; ::_thesis: ( dom' g = cod' f implies g * f in Morphs V )
assume  S1[g,f] ; ::_thesis: g * f in Morphs V
then consider G1, G2, G3 being strict Element of V such that
A1: g is Morphism of G2,G3 and
A2: f is Morphism of G1,G2 by Th8;
reconsider f9 = f as Morphism of G1,G2 by A2;
reconsider g9 = g as Morphism of G2,G3 by A1;
 g9 * f9 = g9 *' f9 by MOD_2:def_11;
hence  g * f in Morphs V by Def7; ::_thesis: verum
end;

theorem Th10: :: MODCAT_1:10
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
proof
let R be Ring; ::_thesis: for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
let V be LeftMod_DOMAIN of R; ::_thesis: for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
let g, f be Element of Morphs V; ::_thesis: ( dom g = cod f implies g * f in Morphs V )
assume  dom g = cod f ; ::_thesis: g * f in Morphs V
then  dom' g = cod' f ;
hence  g * f in Morphs V by Th9; ::_thesis: verum
end;

definition
let R be Ring;
let V be LeftMod_DOMAIN of R;
func comp V ->  PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def14: :: MODCAT_1:def 14
( ( for g, f being Element of Morphs V holds
( [g,f] in dom it iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom it holds
it . (g,f) = g * f ) );
existence
 ex b1 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) )
proof
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom' $1 = cod' $2;
deffunc H1( Element of Morphs V, Element of Morphs V) ->  LModMorphismStr over R = $1 * $2;
A1: for g, f being Element of Morphs V st S1[g,f] holds
H1(g,f) in Morphs V by Th9;
consider c being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) such that
A2: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff S1[g,f] ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = H1(g,f) ) ) from BINOP_1:sch_8(A1);
take  c ; ::_thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) )
thus  ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) holds
b1 = b2
proof
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom' $1 = cod' $2;
let c1, c2 be PartFunc of [:(Morphs V),(Morphs V):],(Morphs V); ::_thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ) implies c1 = c2 )
assume that
A3: for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff S1[g,f] ) and
A4: for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f and
A5: for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff S1[g,f] ) and
A6: for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ; ::_thesis: c1 = c2
set V0 = dom c1;
now__::_thesis:_for_x_being_set_st_x_in_dom_c1_holds_
x_in_dom_c2
let x be set ; ::_thesis: ( x in dom c1 implies x in dom c2 )
assume A8: x in dom c1 ; ::_thesis: x in dom c2
then consider g, f being Element of Morphs V such that
A9: x = [g,f] by SUBSET_1:43;
 S1[g,f] by A3, A8, A9;
hence  x in dom c2 by A5, A9; ::_thesis: verum
end;
then A10: dom c1 c= dom c2 by TARSKI:def_3;
A11: for x, y being set st [x,y] in dom c1 holds
c1 . (x,y) = c2 . (x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom c1 implies c1 . (x,y) = c2 . (x,y) )
assume A12: [x,y] in dom c1 ; ::_thesis: c1 . (x,y) = c2 . (x,y)
then reconsider x = x, y = y as Element of Morphs V by ZFMISC_1:87;
 c1 . (x,y) = x * y by A4, A12;
hence  c1 . (x,y) = c2 . (x,y) by A6, A10, A12; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_c2_holds_
x_in_dom_c1
let x be set ; ::_thesis: ( x in dom c2 implies x in dom c1 )
assume A14: x in dom c2 ; ::_thesis: x in dom c1
then consider g, f being Element of Morphs V such that
A15: x = [g,f] by SUBSET_1:43;
 S1[g,f] by A5, A14, A15;
hence  x in dom c1 by A3, A15; ::_thesis: verum
end;
then  dom c2 c= dom c1 by TARSKI:def_3;
then  dom c1 = dom c2 by A10, XBOOLE_0:def_10;
hence  c1 = c2 by A11, BINOP_1:20; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines comp MODCAT_1:def_14_:_
 for R being Ring
for V being LeftMod_DOMAIN of R
for b3 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b3 = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b3 iff dom' g = cod' f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b3 holds
b3 . (g,f) = g * f ) ) );

theorem Th11: :: MODCAT_1:11
for R being Ring
for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V holds
( [g,f] in dom (comp V) iff dom g = cod f )
proof
let R be Ring; ::_thesis: for V being LeftMod_DOMAIN of R
for g, f being Element of Morphs V holds
( [g,f] in dom (comp V) iff dom g = cod f )
let V be LeftMod_DOMAIN of R; ::_thesis: for g, f being Element of Morphs V holds
( [g,f] in dom (comp V) iff dom g = cod f )
let g, f be Element of Morphs V; ::_thesis: ( [g,f] in dom (comp V) iff dom g = cod f )
 ( dom g = dom' g & cod f = cod' f ) ;
hence  ( [g,f] in dom (comp V) iff dom g = cod f ) by Def14; ::_thesis: verum
end;

definition
let UN be Universe;
let R be Ring;
func LModCat (UN,R) ->  strict CatStr  equals :: MODCAT_1:def 15
 CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);
coherence
 CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #) is strict CatStr ;
end;

:: deftheorem  defines LModCat MODCAT_1:def_15_:_
 for UN being Universe
for R being Ring holds LModCat (UN,R) = CatStr(# (LModObjects (UN,R)),(Morphs (LModObjects (UN,R))),(dom (LModObjects (UN,R))),(cod (LModObjects (UN,R))),(comp (LModObjects (UN,R))) #);

registration
let UN be Universe;
let R be Ring;
cluster LModCat (UN,R) ->  non empty non void strict ;
coherence
 ( not LModCat (UN,R) is void & not LModCat (UN,R) is empty ) ;
end;

theorem Th12: :: MODCAT_1:12
for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R)) holds
( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
proof
let UN be Universe; ::_thesis: for R being Ring
for f, g being Morphism of (LModCat (UN,R)) holds
( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
let R be Ring; ::_thesis: for f, g being Morphism of (LModCat (UN,R)) holds
( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
let f, g be Morphism of (LModCat (UN,R)); ::_thesis: ( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f )
reconsider f9 = f as Element of Morphs (LModObjects (UN,R)) ;
reconsider g9 = g as Element of Morphs (LModObjects (UN,R)) ;
A1: cod f = cod' f9 by Def12
.= cod f9 ;
A2: dom g = dom' g9 by Def11
.= dom g9 ;
A3: now__::_thesis:_(_dom_g_=_cod_f_implies_[g,f]_in_dom_the_Comp_of_(LModCat_(UN,R))_)
assume  dom g = cod f ; ::_thesis: [g,f] in dom the Comp of (LModCat (UN,R))
then  dom' g9 = cod' f9 by A2, A1;
hence  [g,f] in dom the Comp of (LModCat (UN,R)) by Def14; ::_thesis: verum
end;
now__::_thesis:_(_[g,f]_in_dom_the_Comp_of_(LModCat_(UN,R))_implies_dom_g_=_cod_f_)
assume  [g,f] in dom the Comp of (LModCat (UN,R)) ; ::_thesis: dom g = cod f
then  dom' g9 = cod' f9 by Def14
.= cod f9 ;
hence  dom g = cod f by A2, A1; ::_thesis: verum
end;
hence  ( [g,f] in dom the Comp of (LModCat (UN,R)) iff dom g = cod f ) by A3; ::_thesis: verum
end;

registration
let UN be Universe;
let R be Ring;
cluster  ->  strict for Element of Morphs (LModObjects (UN,R));
coherence
 for b1 being Element of Morphs (LModObjects (UN,R)) holds b1 is strict
proof
set V = LModObjects (UN,R);
let f be Element of Morphs (LModObjects (UN,R)); ::_thesis: f is strict
 ex G, H being strict Element of LModObjects (UN,R) st f is strict Morphism of G,H by Def7;
hence  f is strict ; ::_thesis: verum
end;
end;

theorem :: MODCAT_1:13
canceled;

theorem :: MODCAT_1:14
canceled;

theorem Th15: :: MODCAT_1:15
for UN being Universe
for R being Ring
for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
proof
let UN be Universe; ::_thesis: for R being Ring
for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let R be Ring; ::_thesis: for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
set X = Morphs (LModObjects (UN,R));
let f be Morphism of (LModCat (UN,R)); ::_thesis: for f9 being Element of Morphs (LModObjects (UN,R)) st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let f9 be Element of Morphs (LModObjects (UN,R)); ::_thesis: ( f = f9 implies ( dom f = dom f9 & cod f = cod f9 ) )
assume A1: f = f9 ; ::_thesis: ( dom f = dom f9 & cod f = cod f9 )
hence  dom f = dom' f9 by Def11
.= dom f9 ;
::_thesis: cod f = cod f9
thus  cod f = cod' f9 by A1, Def12
.= cod f9 ; ::_thesis: verum
end;

theorem Th16: :: MODCAT_1:16
for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R))
for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
proof
let UN be Universe; ::_thesis: for R being Ring
for f, g being Morphism of (LModCat (UN,R))
for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
let R be Ring; ::_thesis: for f, g being Morphism of (LModCat (UN,R))
for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
set X = Morphs (LModObjects (UN,R));
let f, g be Morphism of (LModCat (UN,R)); ::_thesis: for f9, g9 being Element of Morphs (LModObjects (UN,R)) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
let f9, g9 be Element of Morphs (LModObjects (UN,R)); ::_thesis: ( f = f9 & g = g9 implies ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) ) )
assume that
A1: f = f9 and
A2: g = g9 ; ::_thesis: ( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
A3: cod f = cod f9 by A1, Th15;
hence  ( dom g = cod f iff dom g9 = cod f9 ) by A2, Th15; ::_thesis: ( ( dom g = cod f implies [g9,f9] in dom (comp (LModObjects (UN,R))) ) & ( [g9,f9] in dom (comp (LModObjects (UN,R))) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
 dom g = dom g9 by A2, Th15;
hence A4: ( dom g = cod f iff [g9,f9] in dom (comp (LModObjects (UN,R))) ) by A3, Th11; ::_thesis: ( ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
thus  ( dom g = cod f implies g (*) f = g9 * f9 ) ::_thesis: ( ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
proof
assume A5: dom g = cod f ; ::_thesis: g (*) f = g9 * f9
then  [g,f] in dom the Comp of (LModCat (UN,R)) by Th12;
hence g (*) f = (comp (LModObjects (UN,R))) . (g9,f9) by A1, A2, CAT_1:def_1
.= g9 * f9 by A4, A5, Def14 ;
::_thesis: verum
end;
 dom f = dom f9 by A1, Th15;
hence  ( dom f = dom g iff dom f9 = dom g9 ) by A2, Th15; ::_thesis: ( cod f = cod g iff cod f9 = cod g9 )
 cod g = cod g9 by A2, Th15;
hence  ( cod f = cod g iff cod f9 = cod g9 ) by A1, Th15; ::_thesis: verum
end;

Lm1:  for UN being Universe
for R being Ring
for f, g being Morphism of (LModCat (UN,R)) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
proof
let UN be Universe; ::_thesis: for R being Ring
for f, g being Morphism of (LModCat (UN,R)) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
let R be Ring; ::_thesis: for f, g being Morphism of (LModCat (UN,R)) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
set X = Morphs (LModObjects (UN,R));
let f, g be Morphism of (LModCat (UN,R)); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A1: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider g9 = g as strict Element of Morphs (LModObjects (UN,R)) ;
reconsider f9 = f as strict Element of Morphs (LModObjects (UN,R)) ;
A2: dom g9 = cod f9 by A1, Th16;
then A3: ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by MOD_2:15;
reconsider gf = g9 * f9 as Element of Morphs (LModObjects (UN,R)) by A2, Th10;
 gf = g (*) f by A1, Th16;
hence  ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th16; ::_thesis: verum
end;

Lm2:  for UN being Universe
for R being Ring
for f, g, h being Morphism of (LModCat (UN,R)) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
proof
let UN be Universe; ::_thesis: for R being Ring
for f, g, h being Morphism of (LModCat (UN,R)) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
let R be Ring; ::_thesis: for f, g, h being Morphism of (LModCat (UN,R)) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
set X = Morphs (LModObjects (UN,R));
let f, g, h be Morphism of (LModCat (UN,R)); ::_thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
assume A1: ( dom h = cod g & dom g = cod f ) ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f
reconsider f9 = f, g9 = g, h9 = h as strict Element of Morphs (LModObjects (UN,R)) ;
A2: ( h9 * g9 = h (*) g & dom (h (*) g) = cod f ) by A1, Lm1, Th16;
A3: ( dom h9 = cod g9 & dom g9 = cod f9 ) by A1, Th16;
then reconsider gf = g9 * f9, hg = h9 * g9 as strict Element of Morphs (LModObjects (UN,R)) by Th10;
 ( g9 * f9 = g (*) f & dom h = cod (g (*) f) ) by A1, Lm1, Th16;
then h (*) (g (*) f) = h9 * gf by Th16
.= hg * f9 by A3, MOD_2:17
.= (h (*) g) (*) f by A2, Th16 ;
hence  h (*) (g (*) f) = (h (*) g) (*) f ; ::_thesis: verum
end;

registration
let UN be Universe;
let R be Ring;
cluster LModCat (UN,R) ->  strict Category-like transitive associative reflexive ;
coherence
 ( LModCat (UN,R) is Category-like & LModCat (UN,R) is transitive & LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )
proof
set C = LModCat (UN,R);
thus  LModCat (UN,R) is Category-like ::_thesis: ( LModCat (UN,R) is transitive & LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )
proof
let f be Morphism of (LModCat (UN,R)); :: according to CAT_1:def_6 ::_thesis: for b1 being Element of the carrier' of (LModCat (UN,R)) holds
( ( not [b1,f] in dom the Comp of (LModCat (UN,R)) or dom b1 = cod f ) & ( not dom b1 = cod f or [b1,f] in dom the Comp of (LModCat (UN,R)) ) )
thus  for b1 being Element of the carrier' of (LModCat (UN,R)) holds
( ( not [b1,f] in dom the Comp of (LModCat (UN,R)) or dom b1 = cod f ) & ( not dom b1 = cod f or [b1,f] in dom the Comp of (LModCat (UN,R)) ) ) by Th16; ::_thesis: verum
end;
thus  LModCat (UN,R) is transitive ::_thesis: ( LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )
proof
let f be Morphism of (LModCat (UN,R)); :: according to CAT_1:def_7 ::_thesis: for b1 being Element of the carrier' of (LModCat (UN,R)) holds
( not dom b1 = cod f or ( dom (b1 (*) f) = dom f & cod (b1 (*) f) = cod b1 ) )
thus  for b1 being Element of the carrier' of (LModCat (UN,R)) holds
( not dom b1 = cod f or ( dom (b1 (*) f) = dom f & cod (b1 (*) f) = cod b1 ) ) by Lm1; ::_thesis: verum
end;
thus  LModCat (UN,R) is associative ::_thesis: LModCat (UN,R) is reflexive
proof
let f be Morphism of (LModCat (UN,R)); :: according to CAT_1:def_8 ::_thesis: for b1, b2 being Element of the carrier' of (LModCat (UN,R)) holds
( not dom b2 = cod b1 or not dom b1 = cod f or b2 (*) (b1 (*) f) = (b2 (*) b1) (*) f )
thus  for b1, b2 being Element of the carrier' of (LModCat (UN,R)) holds
( not dom b2 = cod b1 or not dom b1 = cod f or b2 (*) (b1 (*) f) = (b2 (*) b1) (*) f ) by Lm2; ::_thesis: verum
end;
thus  LModCat (UN,R) is reflexive ::_thesis: verum
proof
let a be Element of (LModCat (UN,R)); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {}
reconsider G = a as Element of LModObjects (UN,R) ;
consider x being set  such that
 x in  {  [H,f] where H is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,1:],1) : verum  }  and
W2: GO x,G,R by Def6;
set ii = ID G;
consider x1, x2 being set  such that
 x = [x1,x2] and
W4: ex H being strict LeftMod of R st
( G = H & x1 = addLoopStr(# the carrier of H, the addF of H, the ZeroF of H #) & x2 = the lmult of H ) by W2, Def5;
reconsider G = G as strict Element of LModObjects (UN,R) by W4;
reconsider ii = ID G as Morphism of (LModCat (UN,R)) ;
reconsider ia = ii as LModMorphismStr over R ;
A: dom ii = dom ia by Th15
.= a by MOD_2:18 ;
cod ii = cod ia by Th15
.= a by MOD_2:18 ;
then  ii in Hom (a,a) by A;
hence  Hom (a,a) <> {} ; ::_thesis: verum
end;
end;
end;