:: MOD_2 semantic presentation

begin

       Lm1:  for R being Ring holds VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R
proof
let R be Ring; ::_thesis: VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R
set a = 0. Trivial-addLoopStr;
set G = VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #);
A1: for a, b being Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #)
for x, y being Element of Trivial-addLoopStr st x = a & b = y holds
a + b = x + y ;
A2: ( VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is Abelian & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is add-associative & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_zeroed & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_complementable )
proof
thus  VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is Abelian ::_thesis: ( VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is add-associative & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_zeroed & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_complementable )
proof
let a, b be Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); :: according to RLVECT_1:def_2 ::_thesis: a + b = b + a
reconsider x = a, y = b as Element of Trivial-addLoopStr ;
thus a + b = y + x by A1
.= b + a ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_3 ::_thesis: ( VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_zeroed & VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_complementable )
let a, b, c be Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); ::_thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element of Trivial-addLoopStr ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def_3
.= a + (b + c) ; ::_thesis: verum
end;
hereby  :: according to RLVECT_1:def_4 ::_thesis: VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is right_complementable
let a be Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); ::_thesis: a + (0. VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #)) = a
reconsider x = a as Element of Trivial-addLoopStr ;
thus a + (0. VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #)) = x + (0. Trivial-addLoopStr)
.= a by RLVECT_1:4 ; ::_thesis: verum
end;
let a be Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable
reconsider x = a as Element of Trivial-addLoopStr ;
consider b being Element of Trivial-addLoopStr such that
A3: x + b = 0. Trivial-addLoopStr by ALGSTR_0:def_11;
reconsider b9 = b as Element of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) ;
take  b9 ; :: according to ALGSTR_0:def_11 ::_thesis: a + b9 = 0. VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #)
thus  a + b9 = 0. VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) by A3; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Scalar_of_R
for_v,_w_being_Vector_of_VectSpStr(#_1,op2,op0,(pr2_(_the_carrier_of_R,1))_#)_holds_
(_x_*_(v_+_w)_=_(x_*_v)_+_(x_*_w)_&_(x_+_y)_*_v_=_(x_*_v)_+_(y_*_v)_&_(x_*_y)_*_v_=_x_*_(y_*_v)_&_(1._R)_*_v_=_v_)
let x, y be Scalar of R; ::_thesis: for v, w being Vector of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
let v, w be Vector of VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #); ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
A4: ( (x * y) * v = 0. Trivial-addLoopStr & (1. R) * v = 0. Trivial-addLoopStr ) by GRCAT_1:4;
 ( x * (v + w) = 0. Trivial-addLoopStr & (x + y) * v = 0. Trivial-addLoopStr ) by GRCAT_1:4;
hence  ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v ) by A4, GRCAT_1:4; ::_thesis: verum
end;
hence  VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R by A2, VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;

definition
let R be Ring;
func TrivialLMod R ->  strict LeftMod of R equals :: MOD_2:def 1
 VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #);
coherence
 VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #) is strict LeftMod of R by Lm1;
end;

:: deftheorem  defines TrivialLMod MOD_2:def_1_:_
 for R being Ring holds TrivialLMod R = VectSpStr(# 1,op2,op0,(pr2 ( the carrier of R,1)) #);

theorem :: MOD_2:1
for R being Ring
for x being Vector of (TrivialLMod R) holds x = 0. (TrivialLMod R) by GRCAT_1:4;

definition
let R be non empty multMagma ;
let G, H be non empty VectSpStr over R;
let f be Function of G,H;
attrf is homogeneous  means :Def2: :: MOD_2:def 2
 for a being Scalar of R
for x being Vector of G holds f . (a * x) = a * (f . x);
end;

:: deftheorem Def2 defines homogeneous MOD_2:def_2_:_
 for R being non empty multMagma
for G, H being non empty VectSpStr over R
for f being Function of G,H holds
( f is homogeneous iff for a being Scalar of R
for x being Vector of G holds f . (a * x) = a * (f . x) );

theorem Th2: :: MOD_2:2
for R being Ring
for G, H, S being non empty VectSpStr over R
for f being Function of G,H
for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
proof
let R be Ring; ::_thesis: for G, H, S being non empty VectSpStr over R
for f being Function of G,H
for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
let G, H, S be non empty VectSpStr over R; ::_thesis: for f being Function of G,H
for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
let f be Function of G,H; ::_thesis: for g being Function of H,S st f is homogeneous & g is homogeneous holds
g * f is homogeneous
let g be Function of H,S; ::_thesis: ( f is homogeneous & g is homogeneous implies g * f is homogeneous )
assume that
A1: f is homogeneous and
A2: g is homogeneous ; ::_thesis: g * f is homogeneous
set h = g * f;
let a be Scalar of R; :: according to MOD_2:def_2 ::_thesis: for x being Vector of G holds (g * f) . (a * x) = a * ((g * f) . x)
let x be Vector of G; ::_thesis: (g * f) . (a * x) = a * ((g * f) . x)
thus (g * f) . (a * x) = g . (f . (a * x)) by FUNCT_2:15
.= g . (a * (f . x)) by A1, Def2
.= a * (g . (f . x)) by A2, Def2
.= a * ((g * f) . x) by FUNCT_2:15 ; ::_thesis: verum
end;


registration
let R be Ring;
let G, H be LeftMod of R;
cluster ZeroMap (G,H) ->  homogeneous ;
coherence
 ZeroMap (G,H) is homogeneous
proof
let a be Scalar of R; :: according to MOD_2:def_2 ::_thesis: for x being Vector of G holds (ZeroMap (G,H)) . (a * x) = a * ((ZeroMap (G,H)) . x)
let x be Vector of G; ::_thesis: (ZeroMap (G,H)) . (a * x) = a * ((ZeroMap (G,H)) . x)
set f = ZeroMap (G,H);
 ( (ZeroMap (G,H)) . (a * x) = 0. H & (ZeroMap (G,H)) . x = 0. H ) by FUNCOP_1:7;
hence  (ZeroMap (G,H)) . (a * x) = a * ((ZeroMap (G,H)) . x) by VECTSP_1:14; ::_thesis: verum
end;
end;


definition
let R be Ring;
attrc2 is strict ;
struct LModMorphismStr over R -> ;
aggrLModMorphismStr(# Dom, Cod, Fun #) ->  LModMorphismStr over R;
sel Dom c2 ->  LeftMod of R;
sel Cod c2 ->  LeftMod of R;
sel Fun c2 ->  Function of the Dom of c2, the Cod of c2;
end;

definition
let R be Ring;
let f be LModMorphismStr over R;
func dom f ->  LeftMod of R equals :: MOD_2:def 3
 the Dom of f;
correctness
coherence
the Dom of f is LeftMod of R;
;
func cod f ->  LeftMod of R equals :: MOD_2:def 4
 the Cod of f;
correctness
coherence
the Cod of f is LeftMod of R;
;
end;

:: deftheorem  defines dom MOD_2:def_3_:_
 for R being Ring
for f being LModMorphismStr over R holds dom f = the Dom of f;

:: deftheorem  defines cod MOD_2:def_4_:_
 for R being Ring
for f being LModMorphismStr over R holds cod f = the Cod of f;

definition
let R be Ring;
let f be LModMorphismStr over R;
func fun f ->  Function of (dom f),(cod f) equals :: MOD_2:def 5
 the Fun of f;
coherence
 the Fun of f is Function of (dom f),(cod f) ;
end;

:: deftheorem  defines fun MOD_2:def_5_:_
 for R being Ring
for f being LModMorphismStr over R holds fun f = the Fun of f;

theorem :: MOD_2:3
for R being Ring
for G1, G2 being LeftMod of R
for f being LModMorphismStr over R
for f0 being Function of G1,G2 st f = LModMorphismStr(# G1,G2,f0 #) holds
( dom f = G1 & cod f = G2 & fun f = f0 ) ;

definition
let R be Ring;
let G, H be LeftMod of R;
func ZERO (G,H) ->  strict LModMorphismStr over R equals :: MOD_2:def 6
 LModMorphismStr(# G,H,(ZeroMap (G,H)) #);
correctness
coherence
LModMorphismStr(# G,H,(ZeroMap (G,H)) #) is strict LModMorphismStr over R;
;
end;

:: deftheorem  defines ZERO MOD_2:def_6_:_
 for R being Ring
for G, H being LeftMod of R holds ZERO (G,H) = LModMorphismStr(# G,H,(ZeroMap (G,H)) #);

definition
let R be Ring;
let IT be LModMorphismStr over R;
attrIT is LModMorphism-like  means :Def7: :: MOD_2:def 7
( fun IT is additive & fun IT is homogeneous );
end;

:: deftheorem Def7 defines LModMorphism-like MOD_2:def_7_:_
 for R being Ring
for IT being LModMorphismStr over R holds
( IT is LModMorphism-like iff ( fun IT is additive & fun IT is homogeneous ) );

registration
let R be Ring;
cluster strict LModMorphism-like for LModMorphismStr over R;
existence
 ex b1 being LModMorphismStr over R st
( b1 is strict & b1 is LModMorphism-like )
proof
set G = the LeftMod of R;
set z = ZERO ( the LeftMod of R, the LeftMod of R);
 ( fun (ZERO ( the LeftMod of R, the LeftMod of R)) is additive & fun (ZERO ( the LeftMod of R, the LeftMod of R)) is homogeneous ) ;
then  ZERO ( the LeftMod of R, the LeftMod of R) is LModMorphism-like by Def7;
hence  ex b1 being LModMorphismStr over R st
( b1 is strict & b1 is LModMorphism-like ) ; ::_thesis: verum
end;
end;

definition
let R be Ring;
mode LModMorphism of R is LModMorphism-like LModMorphismStr over R;
end;

theorem Th4: :: MOD_2:4
for R being Ring
for F being LModMorphism of R holds
( the Fun of F is additive & the Fun of F is homogeneous )
proof
let R be Ring; ::_thesis: for F being LModMorphism of R holds
( the Fun of F is additive & the Fun of F is homogeneous )
let F be LModMorphism of R; ::_thesis: ( the Fun of F is additive & the Fun of F is homogeneous )
 the Fun of F = fun F ;
hence  ( the Fun of F is additive & the Fun of F is homogeneous ) by Def7; ::_thesis: verum
end;

registration
let R be Ring;
let G, H be LeftMod of R;
cluster ZERO (G,H) ->  strict LModMorphism-like ;
coherence
 ZERO (G,H) is LModMorphism-like
proof
set z = ZERO (G,H);
 ( fun (ZERO (G,H)) is additive & fun (ZERO (G,H)) is homogeneous ) ;
hence  ZERO (G,H) is LModMorphism-like by Def7; ::_thesis: verum
end;
end;

definition
let R be Ring;
let G, H be LeftMod of R;
mode Morphism of G,H ->  LModMorphism of R means :Def8: :: MOD_2:def 8
( dom it = G & cod it = H );
existence
 ex b1 being LModMorphism of R st
( dom b1 = G & cod b1 = H )
proof
take  ZERO (G,H) ; ::_thesis: ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H )
thus  ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Morphism MOD_2:def_8_:_
 for R being Ring
for G, H being LeftMod of R
for b4 being LModMorphism of R holds
( b4 is Morphism of G,H iff ( dom b4 = G & cod b4 = H ) );

registration
let R be Ring;
let G, H be LeftMod of R;
cluster strict LModMorphism-like for Morphism of G,H;
existence
 ex b1 being Morphism of G,H st b1 is strict
proof
 ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ;
then reconsider z = ZERO (G,H) as Morphism of G,H by Def8;
take  z ; ::_thesis: z is strict
thus  z is strict ; ::_thesis: verum
end;
end;

theorem Th5: :: MOD_2:5
for R being Ring
for G, H being LeftMod of R
for f being LModMorphismStr over R st dom f = G & cod f = H & fun f is additive & fun f is homogeneous holds
f is Morphism of G,H
proof
let R be Ring; ::_thesis: for G, H being LeftMod of R
for f being LModMorphismStr over R st dom f = G & cod f = H & fun f is additive & fun f is homogeneous holds
f is Morphism of G,H
let G, H be LeftMod of R; ::_thesis: for f being LModMorphismStr over R st dom f = G & cod f = H & fun f is additive & fun f is homogeneous holds
f is Morphism of G,H
let f be LModMorphismStr over R; ::_thesis: ( dom f = G & cod f = H & fun f is additive & fun f is homogeneous implies f is Morphism of G,H )
assume that
A1: ( dom f = G & cod f = H ) and
A2: ( fun f is additive & fun f is homogeneous ) ; ::_thesis: f is Morphism of G,H
reconsider f9 = f as LModMorphism of R by A2, Def7;
 f9 is Morphism of G,H by A1, Def8;
hence  f is Morphism of G,H ; ::_thesis: verum
end;

theorem Th6: :: MOD_2:6
for R being Ring
for G, H being LeftMod of R
for f being Function of G,H st f is additive & f is homogeneous holds
LModMorphismStr(# G,H,f #) is strict Morphism of G,H
proof
let R be Ring; ::_thesis: for G, H being LeftMod of R
for f being Function of G,H st f is additive & f is homogeneous holds
LModMorphismStr(# G,H,f #) is strict Morphism of G,H
let G, H be LeftMod of R; ::_thesis: for f being Function of G,H st f is additive & f is homogeneous holds
LModMorphismStr(# G,H,f #) is strict Morphism of G,H
let f be Function of G,H; ::_thesis: ( f is additive & f is homogeneous implies LModMorphismStr(# G,H,f #) is strict Morphism of G,H )
assume A1: ( f is additive & f is homogeneous ) ; ::_thesis: LModMorphismStr(# G,H,f #) is strict Morphism of G,H
set F = LModMorphismStr(# G,H,f #);
 fun LModMorphismStr(# G,H,f #) = f ;
hence  LModMorphismStr(# G,H,f #) is strict Morphism of G,H by A1, Th5; ::_thesis: verum
end;

registration
let R be Ring;
let G be LeftMod of R;
cluster id G ->  homogeneous ;
coherence
 id G is homogeneous
proof
set f = id G;
let a be Scalar of R; :: according to MOD_2:def_2 ::_thesis: for x being Vector of G holds (id G) . (a * x) = a * ((id G) . x)
let x be Vector of G; ::_thesis: (id G) . (a * x) = a * ((id G) . x)
thus (id G) . (a * x) = a * x by FUNCT_1:18
.= a * ((id G) . x) by FUNCT_1:18 ; ::_thesis: verum
end;
end;

definition
let R be Ring;
let G be LeftMod of R;
func ID G ->  strict Morphism of G,G equals :: MOD_2:def 9
 LModMorphismStr(# G,G,(id G) #);
coherence
 LModMorphismStr(# G,G,(id G) #) is strict Morphism of G,G
proof
set i = LModMorphismStr(# G,G,(id G) #);
 fun LModMorphismStr(# G,G,(id G) #) = id G ;
hence  LModMorphismStr(# G,G,(id G) #) is strict Morphism of G,G by Th5; ::_thesis: verum
end;
end;

:: deftheorem  defines ID MOD_2:def_9_:_
 for R being Ring
for G being LeftMod of R holds ID G = LModMorphismStr(# G,G,(id G) #);

definition
let R be Ring;
let G, H be LeftMod of R;
:: original: ZERO
redefine func ZERO (G,H) ->  strict Morphism of G,H;
coherence
 ZERO (G,H) is strict Morphism of G,H
proof
set i = ZERO (G,H);
 fun (ZERO (G,H)) = ZeroMap (G,H) ;
hence  ZERO (G,H) is strict Morphism of G,H by Th5; ::_thesis: verum
end;
end;

theorem Th7: :: MOD_2:7
for R being Ring
for G, H being LeftMod of R
for F being Morphism of G,H ex f being Function of G,H st
( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
proof
let R be Ring; ::_thesis: for G, H being LeftMod of R
for F being Morphism of G,H ex f being Function of G,H st
( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
let G, H be LeftMod of R; ::_thesis: for F being Morphism of G,H ex f being Function of G,H st
( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
let F be Morphism of G,H; ::_thesis: ex f being Function of G,H st
( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
A1: the Cod of F = cod F
.= H by Def8 ;
A2: the Dom of F = dom F
.= G by Def8 ;
then reconsider f = the Fun of F as Function of G,H by A1;
take  f ; ::_thesis: ( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
thus  ( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by A2, A1, Th4; ::_thesis: verum
end;

theorem Th8: :: MOD_2:8
for R being Ring
for G, H being LeftMod of R
for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)
proof
let R be Ring; ::_thesis: for G, H being LeftMod of R
for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)
let G, H be LeftMod of R; ::_thesis: for F being strict Morphism of G,H ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)
let F be strict Morphism of G,H; ::_thesis: ex f being Function of G,H st F = LModMorphismStr(# G,H,f #)
consider f being Function of G,H such that
A1: LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) and
 ( f is additive & f is homogeneous ) by Th7;
take  f ; ::_thesis: F = LModMorphismStr(# G,H,f #)
thus  F = LModMorphismStr(# G,H,f #) by A1; ::_thesis: verum
end;

theorem Th9: :: MOD_2:9
for R being Ring
for F being LModMorphism of R ex G, H being LeftMod of R st F is Morphism of G,H
proof
let R be Ring; ::_thesis: for F being LModMorphism of R ex G, H being LeftMod of R st F is Morphism of G,H
let F be LModMorphism of R; ::_thesis: ex G, H being LeftMod of R st F is Morphism of G,H
take G = the Dom of F; ::_thesis: ex H being LeftMod of R st F is Morphism of G,H
take H = the Cod of F; ::_thesis: F is Morphism of G,H
 ( dom F = G & cod F = H ) ;
hence  F is Morphism of G,H by Def8; ::_thesis: verum
end;

theorem :: MOD_2:10
for R being Ring
for F being strict LModMorphism of R ex G, H being LeftMod of R ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
proof
let R be Ring; ::_thesis: for F being strict LModMorphism of R ex G, H being LeftMod of R ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
let F be strict LModMorphism of R; ::_thesis: ex G, H being LeftMod of R ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
consider G, H being LeftMod of R such that
A1: F is Morphism of G,H by Th9;
reconsider F9 = F as Morphism of G,H by A1;
consider f being Function of G,H such that
A2: ( LModMorphismStr(# the Dom of F9, the Cod of F9, the Fun of F9 #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by Th7;
take  G ; ::_thesis: ex H being LeftMod of R ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
take  H ; ::_thesis: ex f being Function of G,H st
( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
take  f ; ::_thesis: ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )
thus  ( F is strict Morphism of G,H & F = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous ) by A2; ::_thesis: verum
end;

theorem Th11: :: MOD_2:11
for R being Ring
for g, f being LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proof
let R be Ring; ::_thesis: for g, f being LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
defpred S1[ LModMorphism of R, LModMorphism of R] means  dom $1 = cod $2;
let g, f be LModMorphism of R; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
consider G2, G3 being LeftMod of R such that
A2: g is Morphism of G2,G3 by Th9;
A3: G2 = dom g by A2, Def8;
consider G1, G2 being LeftMod of R such that
A4: f is Morphism of G1,G2 by Th9;
 G2 = cod f by A4, Def8;
hence  ex G1, G2, G3 being LeftMod of R st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; ::_thesis: verum
end;

definition
let R be Ring;
let G, F be LModMorphism of R;
assume A1: dom G = cod F ;
funcG * F ->  strict LModMorphism of R means :Def10: :: MOD_2:def 10
 for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
it = LModMorphismStr(# G1,G3,(g * f) #);
existence
 ex b1 being strict LModMorphism of R st
for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b1 = LModMorphismStr(# G1,G3,(g * f) #)
proof
consider G19, G2, G39 being LeftMod of R such that
A2: G is Morphism of G2,G39 and
A3: F is Morphism of G19,G2 by A1, Th11;
consider f9 being Function of G19,G2 such that
A4: LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G19,G2,f9 #) and
A5: ( f9 is additive & f9 is homogeneous ) by A3, Th7;
consider g9 being Function of G2,G39 such that
A6: LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G39,g9 #) and
A7: ( g9 is additive & g9 is homogeneous ) by A2, Th7;
 ( g9 * f9 is additive & g9 * f9 is homogeneous ) by A7, A5, Th2;
then reconsider T9 = LModMorphismStr(# G19,G39,(g9 * f9) #) as strict LModMorphism of R by Th6;
take  T9 ; ::_thesis: for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
T9 = LModMorphismStr(# G1,G3,(g * f) #)
thus  for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
T9 = LModMorphismStr(# G1,G3,(g * f) #) by A6, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict LModMorphism of R st ( for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b1 = LModMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b2 = LModMorphismStr(# G1,G3,(g * f) #) ) holds
b1 = b2
proof
consider G19, G29 being LeftMod of R such that
A8: F is Morphism of G19,G29 by Th9;
reconsider F9 = F as Morphism of G19,G29 by A8;
consider G2, G39 being LeftMod of R such that
A9: G is Morphism of G2,G39 by Th9;
 G2 = dom G by A9, Def8;
then reconsider F9 = F9 as Morphism of G19,G2 by A1, Def8;
consider f9 being Function of G19,G2 such that
A10: LModMorphismStr(# the Dom of F9, the Cod of F9, the Fun of F9 #) = LModMorphismStr(# G19,G2,f9 #) and
 ( f9 is additive & f9 is homogeneous ) by Th7;
reconsider G9 = G as Morphism of G2,G39 by A9;
let S1, S2 be strict LModMorphism of R; ::_thesis: ( ( for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
S1 = LModMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
S2 = LModMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 )
assume that
A11: for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
S1 = LModMorphismStr(# G1,G3,(g * f) #) and
A12: for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
S2 = LModMorphismStr(# G1,G3,(g * f) #) ; ::_thesis: S1 = S2
consider g9 being Function of G2,G39 such that
A13: LModMorphismStr(# the Dom of G9, the Cod of G9, the Fun of G9 #) = LModMorphismStr(# G2,G39,g9 #) and
 ( g9 is additive & g9 is homogeneous ) by Th7;
thus S1 = LModMorphismStr(# G19,G39,(g9 * f9) #) by A11, A13, A10
.= S2 by A12, A13, A10 ; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines * MOD_2:def_10_:_
 for R being Ring
for G, F being LModMorphism of R st dom G = cod F holds
for b4 being strict LModMorphism of R holds
( b4 = G * F iff for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b4 = LModMorphismStr(# G1,G3,(g * f) #) );

theorem Th12: :: MOD_2:12
for R being Ring
for G2, G3, G1 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
proof
let R be Ring; ::_thesis: for G2, G3, G1 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
let G2, G3, G1 be LeftMod of R; ::_thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
let G be Morphism of G2,G3; ::_thesis: for F being Morphism of G1,G2 holds G * F is strict Morphism of G1,G3
let F be Morphism of G1,G2; ::_thesis: G * F is strict Morphism of G1,G3
consider g being Function of G2,G3 such that
A1: LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) and
 ( g is additive & g is homogeneous ) by Th7;
consider f being Function of G1,G2 such that
A2: LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) and
 ( f is additive & f is homogeneous ) by Th7;
dom G = G2 by Def8
.= cod F by Def8 ;
then  G * F = LModMorphismStr(# G1,G3,(g * f) #) by A1, A2, Def10;
then  ( dom (G * F) = G1 & cod (G * F) = G3 ) ;
hence  G * F is strict Morphism of G1,G3 by Def8; ::_thesis: verum
end;

definition
let R be Ring;
let G1, G2, G3 be LeftMod of R;
let G be Morphism of G2,G3;
let F be Morphism of G1,G2;
funcG *' F ->  strict Morphism of G1,G3 equals :: MOD_2:def 11
G * F;
coherence
 G * F is strict Morphism of G1,G3 by Th12;
end;

:: deftheorem  defines *' MOD_2:def_11_:_
 for R being Ring
for G1, G2, G3 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G *' F = G * F;

theorem Th13: :: MOD_2:13
for R being Ring
for G2, G3, G1 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) holds
( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
proof
let R be Ring; ::_thesis: for G2, G3, G1 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) holds
( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
let G2, G3, G1 be LeftMod of R; ::_thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) holds
( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
let G be Morphism of G2,G3; ::_thesis: for F being Morphism of G1,G2
for g being Function of G2,G3
for f being Function of G1,G2 st G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) holds
( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
let F be Morphism of G1,G2; ::_thesis: for g being Function of G2,G3
for f being Function of G1,G2 st G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) holds
( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
let g be Function of G2,G3; ::_thesis: for f being Function of G1,G2 st G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) holds
( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
let f be Function of G1,G2; ::_thesis: ( G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) implies ( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) ) )
assume A1: ( G = LModMorphismStr(# G2,G3,g #) & F = LModMorphismStr(# G1,G2,f #) ) ; ::_thesis: ( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) )
dom G = G2 by Def8
.= cod F by Def8 ;
hence  ( G *' F = LModMorphismStr(# G1,G3,(g * f) #) & G * F = LModMorphismStr(# G1,G3,(g * f) #) ) by A1, Def10; ::_thesis: verum
end;

theorem Th14: :: MOD_2:14
for R being Ring
for f, g being strict LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) )
proof
let R be Ring; ::_thesis: for f, g being strict LModMorphism of R st dom g = cod f holds
ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) )
let f, g be strict LModMorphism of R; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) ) )
assume A1: dom g = cod f ; ::_thesis: ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) )
set G1 = dom f;
set G2 = cod f;
set G3 = cod g;
reconsider f9 = f as strict Morphism of dom f, cod f by Def8;
reconsider g9 = g as strict Morphism of cod f, cod g by A1, Def8;
consider f0 being Function of (dom f),(cod f) such that
A2: f9 = LModMorphismStr(# (dom f),(cod f),f0 #) ;
consider g0 being Function of (cod f),(cod g) such that
A3: g9 = LModMorphismStr(# (cod f),(cod g),g0 #) by Th8;
take  dom f ; ::_thesis: ex G2, G3 being LeftMod of R ex f0 being Function of (dom f),G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# (dom f),G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# (dom f),G3,(g0 * f0) #) )
take  cod f ; ::_thesis: ex G3 being LeftMod of R ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),G3 st
( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),G3,g0 #) & g * f = LModMorphismStr(# (dom f),G3,(g0 * f0) #) )
take  cod g ; ::_thesis: ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),(cod g) st
( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take  f0 ; ::_thesis: ex g0 being Function of (cod f),(cod g) st
( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take  g0 ; ::_thesis: ( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
thus  ( f = LModMorphismStr(# (dom f),(cod f),f0 #) & g = LModMorphismStr(# (cod f),(cod g),g0 #) & g * f = LModMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) by A2, A3, Th13; ::_thesis: verum
end;

theorem :: MOD_2:15
for R being Ring
for f, g being strict LModMorphism of R st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
proof
let R be Ring; ::_thesis: for f, g being strict LModMorphism of R st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
let f, g be strict LModMorphism of R; ::_thesis: ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) )
assume  dom g = cod f ; ::_thesis: ( dom (g * f) = dom f & cod (g * f) = cod g )
then A1: ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) ) by Th14;
hence  dom (g * f) = dom f ; ::_thesis: cod (g * f) = cod g
thus  cod (g * f) = cod g by A1; ::_thesis: verum
end;

theorem Th16: :: MOD_2:16
for R being Ring
for G1, G2, G3, G4 being LeftMod of R
for f being strict Morphism of G1,G2
for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
proof
let R be Ring; ::_thesis: for G1, G2, G3, G4 being LeftMod of R
for f being strict Morphism of G1,G2
for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let G1, G2, G3, G4 be LeftMod of R; ::_thesis: for f being strict Morphism of G1,G2
for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let f be strict Morphism of G1,G2; ::_thesis: for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let g be strict Morphism of G2,G3; ::_thesis: for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let h be strict Morphism of G3,G4; ::_thesis: h * (g * f) = (h * g) * f
consider f0 being Function of G1,G2 such that
A1: f = LModMorphismStr(# G1,G2,f0 #) by Th8;
consider g0 being Function of G2,G3 such that
A2: g = LModMorphismStr(# G2,G3,g0 #) by Th8;
consider h0 being Function of G3,G4 such that
A3: h = LModMorphismStr(# G3,G4,h0 #) by Th8;
A4: h *' g = LModMorphismStr(# G2,G4,(h0 * g0) #) by A2, A3, Th13;
 g *' f = LModMorphismStr(# G1,G3,(g0 * f0) #) by A1, A2, Th13;
then h * (g * f) = LModMorphismStr(# G1,G4,(h0 * (g0 * f0)) #) by A3, Th13
.= LModMorphismStr(# G1,G4,((h0 * g0) * f0) #) by RELAT_1:36
.= (h * g) * f by A1, A4, Th13 ;
hence  h * (g * f) = (h * g) * f ; ::_thesis: verum
end;

theorem :: MOD_2:17
for R being Ring
for f, g, h being strict LModMorphism of R st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
proof
let R be Ring; ::_thesis: for f, g, h being strict LModMorphism of R st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
let f, g, h be strict LModMorphism of R; ::_thesis: ( dom h = cod g & dom g = cod f implies h * (g * f) = (h * g) * f )
assume that
A1: dom h = cod g and
A2: dom g = cod f ; ::_thesis: h * (g * f) = (h * g) * f
set G2 = cod f;
set G3 = cod g;
reconsider h9 = h as strict Morphism of cod g, cod h by A1, Def8;
reconsider g9 = g as strict Morphism of cod f, cod g by A2, Def8;
reconsider f9 = f as strict Morphism of dom f, cod f by Def8;
 h9 * (g9 * f9) = (h9 * g9) * f9 by Th16;
hence  h * (g * f) = (h * g) * f ; ::_thesis: verum
end;

theorem :: MOD_2:18
for R being Ring
for G being LeftMod of R holds
( dom (ID G) = G & cod (ID G) = G & ( for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ) & ( for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ) )
proof
let R be Ring; ::_thesis: for G being LeftMod of R holds
( dom (ID G) = G & cod (ID G) = G & ( for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ) & ( for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ) )
let G be LeftMod of R; ::_thesis: ( dom (ID G) = G & cod (ID G) = G & ( for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ) & ( for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ) )
set i = ID G;
thus  dom (ID G) = G ; ::_thesis: ( cod (ID G) = G & ( for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ) & ( for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ) )
thus  cod (ID G) = G ; ::_thesis: ( ( for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ) & ( for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ) )
thus  for f being strict LModMorphism of R st cod f = G holds
(ID G) * f = f ::_thesis: for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g
proof
let f be strict LModMorphism of R; ::_thesis: ( cod f = G implies (ID G) * f = f )
assume A1: cod f = G ; ::_thesis: (ID G) * f = f
set H = dom f;
reconsider f9 = f as Morphism of dom f,G by A1, Def8;
consider m being Function of (dom f),G such that
A2: f9 = LModMorphismStr(# (dom f),G,m #) by Th8;
 ( dom (ID G) = G & (id G) * m = m ) by FUNCT_2:17;
hence  (ID G) * f = f by A1, A2, Def10; ::_thesis: verum
end;
thus  for g being strict LModMorphism of R st dom g = G holds
g * (ID G) = g ::_thesis: verum
proof
let f be strict LModMorphism of R; ::_thesis: ( dom f = G implies f * (ID G) = f )
assume A3: dom f = G ; ::_thesis: f * (ID G) = f
set H = cod f;
reconsider f9 = f as Morphism of G, cod f by A3, Def8;
consider m being Function of G,(cod f) such that
A4: f9 = LModMorphismStr(# G,(cod f),m #) by Th8;
 ( cod (ID G) = G & m * (id G) = m ) by FUNCT_2:17;
hence  f * (ID G) = f by A3, A4, Def10; ::_thesis: verum
end;
end;

theorem Th19: :: MOD_2:19
for UN being Universe
for u, v, w being Element of UN holds {u,v,w} is Element of UN
proof
let UN be Universe; ::_thesis: for u, v, w being Element of UN holds {u,v,w} is Element of UN
let u, v, w be Element of UN; ::_thesis: {u,v,w} is Element of UN
 {u,v,w} = {u,v} \/ {w} by ENUMSET1:3;
hence  {u,v,w} is Element of UN ; ::_thesis: verum
end;

theorem Th20: :: MOD_2:20
for UN being Universe
for u being Element of UN holds succ u is Element of UN
proof
let UN be Universe; ::_thesis: for u being Element of UN holds succ u is Element of UN
let u be Element of UN; ::_thesis: succ u is Element of UN
 succ u = u \/ {u} by ORDINAL1:def_1;
hence  succ u is Element of UN ; ::_thesis: verum
end;

theorem Th21: :: MOD_2:21
for UN being Universe holds
( 0 is Element of UN & 1 is Element of UN & 2 is Element of UN )
proof
let UN be Universe; ::_thesis: ( 0 is Element of UN & 1 is Element of UN & 2 is Element of UN )
thus  0 is Element of UN by CLASSES2:56; ::_thesis: ( 1 is Element of UN & 2 is Element of UN )
 ( {} is Element of UN & 1 = succ 0 ) by CLASSES2:56;
hence A1: 1 is Element of UN by Th20; ::_thesis: 2 is Element of UN
 2 = succ 1 ;
hence  2 is Element of UN by A1, Th20; ::_thesis: verum
end;

   Lm2:  ex c being Element of {0,1,2} st c = 0
proof
reconsider c = 0 as Element of {0,1,2} by ENUMSET1:def_1;
take  c ; ::_thesis: c = 0
thus  c = 0 ; ::_thesis: verum
end;

Lm3:  ex c being Element of {0,1,2} st c = 1
proof
reconsider c = 1 as Element of {0,1,2} by ENUMSET1:def_1;
take  c ; ::_thesis: c = 1
thus  c = 1 ; ::_thesis: verum
end;

Lm4:  ex c being Element of {0,1,2} st c = 2
proof
reconsider c = 2 as Element of {0,1,2} by ENUMSET1:def_1;
take  c ; ::_thesis: c = 2
thus  c = 2 ; ::_thesis: verum
end;

definition
let a be Element of {0,1,2};
func - a ->  Element of {0,1,2} equals :Def12: :: MOD_2:def 12
 0  if a = 0
2 if a = 1
1 if a = 2
;
coherence
 ( ( a = 0 implies 0 is Element of {0,1,2} ) & ( a = 1 implies 2 is Element of {0,1,2} ) & ( a = 2 implies 1 is Element of {0,1,2} ) ) by Lm3, Lm4;
consistency
 for b1 being Element of {0,1,2} holds
( ( a = 0 & a = 1 implies ( b1 = 0 iff b1 = 2 ) ) & ( a = 0 & a = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( a = 1 & a = 2 implies ( b1 = 2 iff b1 = 1 ) ) ) ;
let b be Element of {0,1,2};
funca + b ->  Element of {0,1,2} equals :Def13: :: MOD_2:def 13
b if a = 0
a if b = 0
2 if ( a = 1 & b = 1 )
0  if ( a = 1 & b = 2 )
0  if ( a = 2 & b = 1 )
1 if ( a = 2 & b = 2 )
;
coherence
 ( ( a = 0 implies b is Element of {0,1,2} ) & ( b = 0 implies a is Element of {0,1,2} ) & ( a = 1 & b = 1 implies 2 is Element of {0,1,2} ) & ( a = 1 & b = 2 implies 0 is Element of {0,1,2} ) & ( a = 2 & b = 1 implies 0 is Element of {0,1,2} ) & ( a = 2 & b = 2 implies 1 is Element of {0,1,2} ) ) by Lm2, Lm3, Lm4;
consistency
 for b1 being Element of {0,1,2} holds
( ( a = 0 & b = 0 implies ( b1 = b iff b1 = a ) ) & ( a = 0 & a = 1 & b = 1 implies ( b1 = b iff b1 = 2 ) ) & ( a = 0 & a = 1 & b = 2 implies ( b1 = b iff b1 = 0 ) ) & ( a = 0 & a = 2 & b = 1 implies ( b1 = b iff b1 = 0 ) ) & ( a = 0 & a = 2 & b = 2 implies ( b1 = b iff b1 = 1 ) ) & ( b = 0 & a = 1 & b = 1 implies ( b1 = a iff b1 = 2 ) ) & ( b = 0 & a = 1 & b = 2 implies ( b1 = a iff b1 = 0 ) ) & ( b = 0 & a = 2 & b = 1 implies ( b1 = a iff b1 = 0 ) ) & ( b = 0 & a = 2 & b = 2 implies ( b1 = a iff b1 = 1 ) ) & ( a = 1 & b = 1 & a = 1 & b = 2 implies ( b1 = 2 iff b1 = 0 ) ) & ( a = 1 & b = 1 & a = 2 & b = 1 implies ( b1 = 2 iff b1 = 0 ) ) & ( a = 1 & b = 1 & a = 2 & b = 2 implies ( b1 = 2 iff b1 = 1 ) ) & ( a = 1 & b = 2 & a = 2 & b = 1 implies ( b1 = 0 iff b1 = 0 ) ) & ( a = 1 & b = 2 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( a = 2 & b = 1 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) ) ;
funca * b ->  Element of {0,1,2} equals :Def14: :: MOD_2:def 14
 0  if b = 0
0  if a = 0
a if b = 1
b if a = 1
1 if ( a = 2 & b = 2 )
;
coherence
 ( ( b = 0 implies 0 is Element of {0,1,2} ) & ( a = 0 implies 0 is Element of {0,1,2} ) & ( b = 1 implies a is Element of {0,1,2} ) & ( a = 1 implies b is Element of {0,1,2} ) & ( a = 2 & b = 2 implies 1 is Element of {0,1,2} ) ) by Lm3;
consistency
 for b1 being Element of {0,1,2} holds
( ( b = 0 & a = 0 implies ( b1 = 0 iff b1 = 0 ) ) & ( b = 0 & b = 1 implies ( b1 = 0 iff b1 = a ) ) & ( b = 0 & a = 1 implies ( b1 = 0 iff b1 = b ) ) & ( b = 0 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( a = 0 & b = 1 implies ( b1 = 0 iff b1 = a ) ) & ( a = 0 & a = 1 implies ( b1 = 0 iff b1 = b ) ) & ( a = 0 & a = 2 & b = 2 implies ( b1 = 0 iff b1 = 1 ) ) & ( b = 1 & a = 1 implies ( b1 = a iff b1 = b ) ) & ( b = 1 & a = 2 & b = 2 implies ( b1 = a iff b1 = 1 ) ) & ( a = 1 & a = 2 & b = 2 implies ( b1 = b iff b1 = 1 ) ) ) ;
end;

:: deftheorem Def12 defines - MOD_2:def_12_:_
 for a being Element of {0,1,2} holds
( ( a = 0 implies - a = 0 ) & ( a = 1 implies - a = 2 ) & ( a = 2 implies - a = 1 ) );

:: deftheorem Def13 defines + MOD_2:def_13_:_
 for a, b being Element of {0,1,2} holds
( ( a = 0 implies a + b = b ) & ( b = 0 implies a + b = a ) & ( a = 1 & b = 1 implies a + b = 2 ) & ( a = 1 & b = 2 implies a + b = 0 ) & ( a = 2 & b = 1 implies a + b = 0 ) & ( a = 2 & b = 2 implies a + b = 1 ) );

:: deftheorem Def14 defines * MOD_2:def_14_:_
 for a, b being Element of {0,1,2} holds
( ( b = 0 implies a * b = 0 ) & ( a = 0 implies a * b = 0 ) & ( b = 1 implies a * b = a ) & ( a = 1 implies a * b = b ) & ( a = 2 & b = 2 implies a * b = 1 ) );

definition
func add3  ->  BinOp of {0,1,2} means :Def15: :: MOD_2:def 15
 for a, b being Element of {0,1,2} holds it . (a,b) = a + b;
existence
 ex b1 being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b
proof
deffunc H1( Element of {0,1,2}, Element of {0,1,2}) ->  Element of {0,1,2} = $1 + $2;
 ex o being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds o . (a,b) = H1(a,b) from BINOP_1:sch_4();
hence  ex b1 being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of {0,1,2} st ( for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b ) & ( for a, b being Element of {0,1,2} holds b2 . (a,b) = a + b ) holds
b1 = b2
proof
let o1, o2 be BinOp of {0,1,2}; ::_thesis: ( ( for a, b being Element of {0,1,2} holds o1 . (a,b) = a + b ) & ( for a, b being Element of {0,1,2} holds o2 . (a,b) = a + b ) implies o1 = o2 )
assume that
A1: for a, b being Element of {0,1,2} holds o1 . (a,b) = a + b and
A2: for a, b being Element of {0,1,2} holds o2 . (a,b) = a + b ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_{0,1,2}_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of {0,1,2}; ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = a + b by A1
.= o2 . (a,b) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
func mult3  ->  BinOp of {0,1,2} means :Def16: :: MOD_2:def 16
 for a, b being Element of {0,1,2} holds it . (a,b) = a * b;
existence
 ex b1 being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds b1 . (a,b) = a * b
proof
deffunc H1( Element of {0,1,2}, Element of {0,1,2}) ->  Element of {0,1,2} = $1 * $2;
 ex o being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds o . (a,b) = H1(a,b) from BINOP_1:sch_4();
hence  ex b1 being BinOp of {0,1,2} st
for a, b being Element of {0,1,2} holds b1 . (a,b) = a * b ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of {0,1,2} st ( for a, b being Element of {0,1,2} holds b1 . (a,b) = a * b ) & ( for a, b being Element of {0,1,2} holds b2 . (a,b) = a * b ) holds
b1 = b2
proof
let o1, o2 be BinOp of {0,1,2}; ::_thesis: ( ( for a, b being Element of {0,1,2} holds o1 . (a,b) = a * b ) & ( for a, b being Element of {0,1,2} holds o2 . (a,b) = a * b ) implies o1 = o2 )
assume that
A3: for a, b being Element of {0,1,2} holds o1 . (a,b) = a * b and
A4: for a, b being Element of {0,1,2} holds o2 . (a,b) = a * b ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_{0,1,2}_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of {0,1,2}; ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = a * b by A3
.= o2 . (a,b) by A4 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
func compl3  ->  UnOp of {0,1,2} means :Def17: :: MOD_2:def 17
 for a being Element of {0,1,2} holds it . a = - a;
existence
 ex b1 being UnOp of {0,1,2} st
for a being Element of {0,1,2} holds b1 . a = - a
proof
deffunc H1( Element of {0,1,2}) ->  Element of {0,1,2} = - $1;
 ex f being UnOp of {0,1,2} st
for x being Element of {0,1,2} holds f . x = H1(x) from FUNCT_2:sch_4();
hence  ex b1 being UnOp of {0,1,2} st
for a being Element of {0,1,2} holds b1 . a = - a ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of {0,1,2} st ( for a being Element of {0,1,2} holds b1 . a = - a ) & ( for a being Element of {0,1,2} holds b2 . a = - a ) holds
b1 = b2
proof
let o1, o2 be UnOp of {0,1,2}; ::_thesis: ( ( for a being Element of {0,1,2} holds o1 . a = - a ) & ( for a being Element of {0,1,2} holds o2 . a = - a ) implies o1 = o2 )
assume that
A5: for a being Element of {0,1,2} holds o1 . a = - a and
A6: for a being Element of {0,1,2} holds o2 . a = - a ; ::_thesis: o1 = o2
now__::_thesis:_for_a_being_Element_of_{0,1,2}_holds_o1_._a_=_o2_._a
let a be Element of {0,1,2}; ::_thesis: o1 . a = o2 . a
thus o1 . a = - a by A5
.= o2 . a by A6 ; ::_thesis: verum
end;
hence  o1 = o2 by FUNCT_2:63; ::_thesis: verum
end;
func unit3  ->  Element of {0,1,2} equals :: MOD_2:def 18
1;
coherence
 1 is Element of {0,1,2} by ENUMSET1:def_1;
func zero3  ->  Element of {0,1,2} equals :: MOD_2:def 19
 0 ;
coherence
 0 is Element of {0,1,2} by ENUMSET1:def_1;
end;

:: deftheorem Def15 defines add3 MOD_2:def_15_:_
 for b1 being BinOp of {0,1,2} holds
( b1 = add3 iff for a, b being Element of {0,1,2} holds b1 . (a,b) = a + b );

:: deftheorem Def16 defines mult3 MOD_2:def_16_:_
 for b1 being BinOp of {0,1,2} holds
( b1 = mult3 iff for a, b being Element of {0,1,2} holds b1 . (a,b) = a * b );

:: deftheorem Def17 defines compl3 MOD_2:def_17_:_
 for b1 being UnOp of {0,1,2} holds
( b1 = compl3 iff for a being Element of {0,1,2} holds b1 . a = - a );

:: deftheorem  defines unit3 MOD_2:def_18_:_
 unit3 = 1;

:: deftheorem  defines zero3 MOD_2:def_19_:_
 zero3 = 0 ;

definition
func Z_3  ->  strict doubleLoopStr  equals :Def20: :: MOD_2:def 20
 doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #);
coherence
 doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #) is strict doubleLoopStr ;
end;

:: deftheorem Def20 defines Z_3 MOD_2:def_20_:_
 Z_3 = doubleLoopStr(# {0,1,2},add3,mult3,unit3,zero3 #);

registration
cluster Z_3  ->  non empty strict ;
coherence
 not Z_3 is empty ;
end;

Lm5: now__::_thesis:_for_h,_e_being_Element_of_Z_3_st_e_=_1_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h, e be Element of Z_3; ::_thesis: ( e = 1 implies ( h * e = h & e * h = h ) )
assume A1: e = 1 ; ::_thesis: ( h * e = h & e * h = h )
reconsider a = e, b = h as Element of {0,1,2} ;
thus h * e = b * a by Def16
.= h by A1, Def14 ; ::_thesis: e * h = h
thus e * h = a * b by Def16
.= h by A1, Def14 ; ::_thesis: verum
end;

registration
cluster Z_3  ->  strict well-unital ;
coherence
 Z_3 is well-unital
proof
let x be Element of Z_3; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. Z_3) = x & (1. Z_3) * x = x )
thus  ( x * (1. Z_3) = x & (1. Z_3) * x = x ) by Lm5; ::_thesis: verum
end;
end;

theorem Th22: :: MOD_2:22
( 0. Z_3 = 0 & 1. Z_3 = 1 & 0. Z_3 is Element of {0,1,2} & 1. Z_3 is Element of {0,1,2} & the addF of Z_3 = add3 & the multF of Z_3 = mult3 ) ;

Lm6:  for x, y, z being Scalar of Z_3
for X, Y, Z being Element of {0,1,2} st X = x & Y = y & Z = z holds
( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
proof
let x, y, z be Scalar of Z_3; ::_thesis: for X, Y, Z being Element of {0,1,2} st X = x & Y = y & Z = z holds
( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
let X, Y, Z be Element of {0,1,2}; ::_thesis: ( X = x & Y = y & Z = z implies ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) ) )
assume that
A1: X = x and
A2: Y = y and
A3: Z = z ; ::_thesis: ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
A4: ( x * y = X * Y & y * z = Y * Z ) by A1, A2, A3, Def16;
 ( x + y = X + Y & y + z = Y + Z ) by A1, A2, A3, Def15;
hence  ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) ) by A1, A3, A4, Def15, Def16; ::_thesis: verum
end;

Lm7:  for x, y, z, a being Element of {0,1,2} st a = 0 holds
( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) )
proof
let x, y, z, a be Element of {0,1,2}; ::_thesis: ( a = 0 implies ( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) ) )
assume A1: a = 0 ; ::_thesis: ( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) )
thus  x + (- x) = a ::_thesis: ( x + a = x & (x + y) + z = x + (y + z) )
proof
now__::_thesis:_x_+_(-_x)_=_a
percases ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def_1;
supposeA2: x = 0 ; ::_thesis: x + (- x) = a
then  - x = 0 by Def12;
hence  x + (- x) = a by A1, A2, Def13; ::_thesis: verum
end;
supposeA3: x = 1 ; ::_thesis: x + (- x) = a
then  - x = 2 by Def12;
hence  x + (- x) = a by A1, A3, Def13; ::_thesis: verum
end;
supposeA4: x = 2 ; ::_thesis: x + (- x) = a
then  - x = 1 by Def12;
hence  x + (- x) = a by A1, A4, Def13; ::_thesis: verum
end;
end;
end;
hence  x + (- x) = a ; ::_thesis: verum
end;
thus  x + a = x by A1, Def13; ::_thesis: (x + y) + z = x + (y + z)
thus  (x + y) + z = x + (y + z) ::_thesis: verum
proof
now__::_thesis:_(x_+_y)_+_z_=_x_+_(y_+_z)
percases ( x = 0 or y = 0 or z = 0 or ( x = 1 & y = 1 & z = 1 ) or ( x = 1 & y = 1 & z = 2 ) or ( x = 1 & y = 2 & z = 1 ) or ( x = 1 & y = 2 & z = 2 ) or ( x = 2 & y = 1 & z = 1 ) or ( x = 2 & y = 1 & z = 2 ) or ( x = 2 & y = 2 & z = 1 ) or ( x = 2 & y = 2 & z = 2 ) ) by ENUMSET1:def_1;
supposeA5: x = 0 ; ::_thesis: (x + y) + z = x + (y + z)
hence (x + y) + z = y + z by Def13
.= x + (y + z) by A5, Def13 ;
::_thesis: verum
end;
supposeA6: y = 0 ; ::_thesis: (x + y) + z = x + (y + z)
then  x + y = x by Def13;
hence  (x + y) + z = x + (y + z) by A6, Def13; ::_thesis: verum
end;
supposeA7: z = 0 ; ::_thesis: (x + y) + z = x + (y + z)
then  y + z = y by Def13;
hence  (x + y) + z = x + (y + z) by A7, Def13; ::_thesis: verum
end;
supposeA8: ( x = 1 & y = 1 & z = 1 ) ; ::_thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = 0 by A8, Def13
.= x + (y + z) by A8, Def13 ; ::_thesis: verum
end;
supposeA9: ( x = 1 & y = 1 & z = 2 ) ; ::_thesis: (x + y) + z = x + (y + z)
then A10: y + z = 0 by Def13;
 x + y = 2 by A9, Def13;
hence (x + y) + z = 1 by A9, Def13
.= x + (y + z) by A9, A10, Def13 ;
::_thesis: verum
end;
supposeA11: ( x = 1 & y = 2 & z = 1 ) ; ::_thesis: (x + y) + z = x + (y + z)
then A12: y + z = 0 by Def13;
 x + y = 0 by A11, Def13;
hence (x + y) + z = 1 by A11, Def13
.= x + (y + z) by A11, A12, Def13 ;
::_thesis: verum
end;
supposeA13: ( x = 1 & y = 2 & z = 2 ) ; ::_thesis: (x + y) + z = x + (y + z)
then A14: y + z = 1 by Def13;
 x + y = 0 by A13, Def13;
hence (x + y) + z = 2 by A13, Def13
.= x + (y + z) by A13, A14, Def13 ;
::_thesis: verum
end;
supposeA15: ( x = 2 & y = 1 & z = 1 ) ; ::_thesis: (x + y) + z = x + (y + z)
then A16: y + z = 2 by Def13;
 x + y = 0 by A15, Def13;
hence (x + y) + z = 1 by A15, Def13
.= x + (y + z) by A15, A16, Def13 ;
::_thesis: verum
end;
supposeA17: ( x = 2 & y = 1 & z = 2 ) ; ::_thesis: (x + y) + z = x + (y + z)
then A18: y + z = 0 by Def13;
 x + y = 0 by A17, Def13;
hence (x + y) + z = 2 by A17, Def13
.= x + (y + z) by A17, A18, Def13 ;
::_thesis: verum
end;
supposeA19: ( x = 2 & y = 2 & z = 1 ) ; ::_thesis: (x + y) + z = x + (y + z)
then A20: y + z = 0 by Def13;
 x + y = 1 by A19, Def13;
hence (x + y) + z = 2 by A19, Def13
.= x + (y + z) by A19, A20, Def13 ;
::_thesis: verum
end;
supposeA21: ( x = 2 & y = 2 & z = 2 ) ; ::_thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = 0 by A21, Def13
.= x + (y + z) by A21, Def13 ; ::_thesis: verum
end;
end;
end;
hence  (x + y) + z = x + (y + z) ; ::_thesis: verum
end;
end;

registration
cluster Z_3  ->  right_complementable strict add-associative right_zeroed ;
coherence
 ( Z_3 is add-associative & Z_3 is right_zeroed & Z_3 is right_complementable )
proof
thus  Z_3 is add-associative ::_thesis: ( Z_3 is right_zeroed & Z_3 is right_complementable )
proof
let x, y, z be Element of Z_3; :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider X = x, Y = y, Z = z as Element of {0,1,2} ;
thus (x + y) + z = (X + Y) + Z by Lm6
.= X + (Y + Z) by Lm7
.= x + (y + z) by Lm6 ; ::_thesis: verum
end;
thus  Z_3 is right_zeroed ::_thesis: Z_3 is right_complementable
proof
let x be Element of Z_3; :: according to RLVECT_1:def_4 ::_thesis: x + (0. Z_3) = x
reconsider X = x, a = 0 as Element of {0,1,2} by Def20;
thus x + (0. Z_3) = X + a by Def15
.= x by Lm7 ; ::_thesis: verum
end;
let x be Element of Z_3; :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider x9 = x as Element of {0,1,2} ;
reconsider y = compl3 . x9 as Element of Z_3 ;
reconsider y9 = y as Element of {0,1,2} ;
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. Z_3
A1: y9 = - x9 by Def17;
thus  x + y = 0. Z_3 ::_thesis: verum
proof
percases ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def_1;
supposeA2: x = 0 ; ::_thesis: x + y = 0. Z_3
then A3: y9 = 0 by A1, Def12;
thus x + y = x9 + y9 by Def15
.= 0. Z_3 by A2, A3, Def13 ; ::_thesis: verum
end;
supposeA4: x = 1 ; ::_thesis: x + y = 0. Z_3
then A5: y9 = 2 by A1, Def12;
thus x + y = x9 + y9 by Def15
.= 0. Z_3 by A4, A5, Def13 ; ::_thesis: verum
end;
supposeA6: x = 2 ; ::_thesis: x + y = 0. Z_3
then A7: y9 = 1 by A1, Def12;
thus x + y = x9 + y9 by Def15
.= 0. Z_3 by A6, A7, Def13 ; ::_thesis: verum
end;
end;
end;
end;
end;

theorem Th23: :: MOD_2:23
for x, y being Scalar of Z_3
for X, Y being Element of {0,1,2} st X = x & Y = y holds
( x + y = X + Y & x * y = X * Y & - x = - X )
proof
let x, y be Scalar of Z_3; ::_thesis: for X, Y being Element of {0,1,2} st X = x & Y = y holds
( x + y = X + Y & x * y = X * Y & - x = - X )
let X, Y be Element of {0,1,2}; ::_thesis: ( X = x & Y = y implies ( x + y = X + Y & x * y = X * Y & - x = - X ) )
assume that
A1: X = x and
A2: Y = y ; ::_thesis: ( x + y = X + Y & x * y = X * Y & - x = - X )
thus  x + y = X + Y by A1, A2, Def15; ::_thesis: ( x * y = X * Y & - x = - X )
thus  x * y = X * Y by A1, A2, Def16; ::_thesis: - x = - X
reconsider a = - X as Element of Z_3 ;
x + a = X + (- X) by A1, Def15
.= 0. Z_3 by Lm7 ;
hence  - x = - X by RLVECT_1:def_10; ::_thesis: verum
end;

theorem Th24: :: MOD_2:24
for x, y, z being Scalar of Z_3
for X, Y, Z being Element of {0,1,2} st X = x & Y = y & Z = z holds
( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
proof
let x, y, z be Scalar of Z_3; ::_thesis: for X, Y, Z being Element of {0,1,2} st X = x & Y = y & Z = z holds
( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
let X, Y, Z be Element of {0,1,2}; ::_thesis: ( X = x & Y = y & Z = z implies ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) ) )
assume that
A1: X = x and
A2: Y = y and
A3: Z = z ; ::_thesis: ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) )
A4: ( x * y = X * Y & y * z = Y * Z ) by A1, A2, A3, Th23;
 ( x + y = X + Y & y + z = Y + Z ) by A1, A2, A3, Th23;
hence  ( (x + y) + z = (X + Y) + Z & x + (y + z) = X + (Y + Z) & (x * y) * z = (X * Y) * Z & x * (y * z) = X * (Y * Z) ) by A1, A3, A4, Th23; ::_thesis: verum
end;

theorem Th25: :: MOD_2:25
for x, y, z, a, b being Element of {0,1,2} st a = 0 & b = 1 holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
proof
let x, y, z, a, b be Element of {0,1,2}; ::_thesis: ( a = 0 & b = 1 implies ( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) ) )
assume that
A1: a = 0 and
A2: b = 1 ; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus  x + y = y + x ::_thesis: ( (x + y) + z = x + (y + z) & x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
proof
now__::_thesis:_x_+_y_=_y_+_x
percases ( x = 0 or y = 0 or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) ) by ENUMSET1:def_1;
supposeA3: x = 0 ; ::_thesis: x + y = y + x
hence x + y = y by Def13
.= y + x by A3, Def13 ;
::_thesis: verum
end;
supposeA4: y = 0 ; ::_thesis: x + y = y + x
hence x + y = x by Def13
.= y + x by A4, Def13 ;
::_thesis: verum
end;
suppose ( x = 1 & y = 1 ) ; ::_thesis: x + y = y + x
hence  x + y = y + x ; ::_thesis: verum
end;
supposeA5: ( x = 1 & y = 2 ) ; ::_thesis: x + y = y + x
hence x + y = 0 by Def13
.= y + x by A5, Def13 ;
::_thesis: verum
end;
supposeA6: ( x = 2 & y = 1 ) ; ::_thesis: x + y = y + x
hence x + y = 0 by Def13
.= y + x by A6, Def13 ;
::_thesis: verum
end;
suppose ( x = 2 & y = 2 ) ; ::_thesis: x + y = y + x
hence  x + y = y + x ; ::_thesis: verum
end;
end;
end;
hence  x + y = y + x ; ::_thesis: verum
end;
thus  (x + y) + z = x + (y + z) by A1, Lm7; ::_thesis: ( x + a = x & x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus  x + a = x by A1, Def13; ::_thesis: ( x + (- x) = a & x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus  x + (- x) = a by A1, Lm7; ::_thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus  x * y = y * x ::_thesis: ( (x * y) * z = x * (y * z) & b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
proof
now__::_thesis:_x_*_y_=_y_*_x
percases ( y = 0 or x = 0 or y = 1 or x = 1 or ( x = 2 & y = 2 ) ) by ENUMSET1:def_1;
supposeA7: y = 0 ; ::_thesis: x * y = y * x
hence x * y = 0 by Def14
.= y * x by A7, Def14 ;
::_thesis: verum
end;
supposeA8: x = 0 ; ::_thesis: x * y = y * x
hence x * y = 0 by Def14
.= y * x by A8, Def14 ;
::_thesis: verum
end;
supposeA9: y = 1 ; ::_thesis: x * y = y * x
hence x * y = x by Def14
.= y * x by A9, Def14 ;
::_thesis: verum
end;
supposeA10: x = 1 ; ::_thesis: x * y = y * x
hence x * y = y by Def14
.= y * x by A10, Def14 ;
::_thesis: verum
end;
suppose ( x = 2 & y = 2 ) ; ::_thesis: x * y = y * x
hence  x * y = y * x ; ::_thesis: verum
end;
end;
end;
hence  x * y = y * x ; ::_thesis: verum
end;
thus  (x * y) * z = x * (y * z) ::_thesis: ( b * x = x & ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
proof
now__::_thesis:_(x_*_y)_*_z_=_x_*_(y_*_z)
percases ( z = 0 or y = 0 or x = 0 or z = 1 or y = 1 or x = 1 or ( x = 2 & y = 2 & z = 2 ) ) by ENUMSET1:def_1;
supposeA11: z = 0 ; ::_thesis: (x * y) * z = x * (y * z)
then A12: y * z = 0 by Def14;
thus (x * y) * z = 0 by A11, Def14
.= x * (y * z) by A12, Def14 ; ::_thesis: verum
end;
supposeA13: y = 0 ; ::_thesis: (x * y) * z = x * (y * z)
then A14: y * z = 0 by Def14;
 x * y = 0 by A13, Def14;
hence (x * y) * z = 0 by Def14
.= x * (y * z) by A14, Def14 ;
::_thesis: verum
end;
supposeA15: x = 0 ; ::_thesis: (x * y) * z = x * (y * z)
then  x * y = 0 by Def14;
hence (x * y) * z = 0 by Def14
.= x * (y * z) by A15, Def14 ;
::_thesis: verum
end;
supposeA16: z = 1 ; ::_thesis: (x * y) * z = x * (y * z)
then  y * z = y by Def14;
hence  (x * y) * z = x * (y * z) by A16, Def14; ::_thesis: verum
end;
supposeA17: y = 1 ; ::_thesis: (x * y) * z = x * (y * z)
then  x * y = x by Def14;
hence  (x * y) * z = x * (y * z) by A17, Def14; ::_thesis: verum
end;
supposeA18: x = 1 ; ::_thesis: (x * y) * z = x * (y * z)
hence (x * y) * z = y * z by Def14
.= x * (y * z) by A18, Def14 ;
::_thesis: verum
end;
supposeA19: ( x = 2 & y = 2 & z = 2 ) ; ::_thesis: (x * y) * z = x * (y * z)
then A20: y * z = 1 by Def14;
 x * y = 1 by A19, Def14;
hence (x * y) * z = x by A19, Def14
.= x * (y * z) by A20, Def14 ;
::_thesis: verum
end;
end;
end;
hence  (x * y) * z = x * (y * z) ; ::_thesis: verum
end;
thus  b * x = x by A2, Def14; ::_thesis: ( ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) & a <> b & x * (y + z) = (x * y) + (x * z) )
thus  ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ::_thesis: ( a <> b & x * (y + z) = (x * y) + (x * z) )
proof
now__::_thesis:_(_(_x_=_0_&_(_x_<>_a_implies_ex_y_being_Element_of_{0,1,2}_st_x_*_y_=_b_)_)_or_(_x_=_1_&_ex_y_being_Element_of_{0,1,2}_st_
(_x_<>_a_implies_ex_y_being_Element_of_{0,1,2}_st_x_*_y_=_b_)_)_or_(_x_=_2_&_ex_y_being_Element_of_{0,1,2}_st_
(_x_<>_a_implies_ex_y_being_Element_of_{0,1,2}_st_x_*_y_=_b_)_)_)
percases ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def_1;
case x = 0 ; ::_thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )
hence  ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A1; ::_thesis: verum
end;
caseA21: x = 1 ; ::_thesis: ex y being Element of {0,1,2} st
( x <> a implies ex y being Element of {0,1,2} st x * y = b )
reconsider y = 1 as Element of {0,1,2} by ENUMSET1:def_1;
take y = y; ::_thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )
 x * y = 1 by A21, Def14;
hence  ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; ::_thesis: verum
end;
caseA22: x = 2 ; ::_thesis: ex y being Element of {0,1,2} st
( x <> a implies ex y being Element of {0,1,2} st x * y = b )
reconsider y = 2 as Element of {0,1,2} by ENUMSET1:def_1;
take y = y; ::_thesis: ( x <> a implies ex y being Element of {0,1,2} st x * y = b )
 x * y = 1 by A22, Def14;
hence  ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) by A2; ::_thesis: verum
end;
end;
end;
hence  ( x <> a implies ex y being Element of {0,1,2} st x * y = b ) ; ::_thesis: verum
end;
thus  a <> b by A1, A2; ::_thesis: x * (y + z) = (x * y) + (x * z)
thus  x * (y + z) = (x * y) + (x * z) ::_thesis: verum
proof
now__::_thesis:_x_*_(y_+_z)_=_(x_*_y)_+_(x_*_z)
percases ( x = 0 or y = 0 or z = 0 or ( x = 1 & y = 1 & z = 1 ) or ( x = 1 & y = 1 & z = 2 ) or ( x = 1 & y = 2 & z = 1 ) or ( x = 1 & y = 2 & z = 2 ) or ( x = 2 & y = 1 & z = 1 ) or ( x = 2 & y = 1 & z = 2 ) or ( x = 2 & y = 2 & z = 1 ) or ( x = 2 & y = 2 & z = 2 ) ) by ENUMSET1:def_1;
supposeA23: x = 0 ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A24: ( x * y = 0 & x * z = 0 ) by Def14;
thus x * (y + z) = 0 by A23, Def14
.= (x * y) + (x * z) by A24, Def13 ; ::_thesis: verum
end;
suppose y = 0 ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then  ( y + z = z & x * y = 0 ) by Def13, Def14;
hence  x * (y + z) = (x * y) + (x * z) by Def13; ::_thesis: verum
end;
suppose z = 0 ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then  ( y + z = y & x * z = 0 ) by Def13, Def14;
hence  x * (y + z) = (x * y) + (x * z) by Def13; ::_thesis: verum
end;
supposeA25: ( x = 1 & y = 1 & z = 1 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then  x * y = 1 by Def14;
hence  x * (y + z) = (x * y) + (x * z) by A25, Def14; ::_thesis: verum
end;
supposeA26: ( x = 1 & y = 1 & z = 2 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A27: ( x * y = 1 & x * z = 2 ) by Def14;
 y + z = 0 by A26, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A27, Def13 ;
::_thesis: verum
end;
supposeA28: ( x = 1 & y = 2 & z = 1 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A29: ( x * y = 2 & x * z = 1 ) by Def14;
 y + z = 0 by A28, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A29, Def13 ;
::_thesis: verum
end;
supposeA30: ( x = 1 & y = 2 & z = 2 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then  x * y = 2 by Def14;
hence  x * (y + z) = (x * y) + (x * z) by A30, Def14; ::_thesis: verum
end;
supposeA31: ( x = 2 & y = 1 & z = 1 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A32: x * y = 2 by Def14;
 y + z = 2 by A31, Def13;
hence x * (y + z) = 1 by A31, Def14
.= (x * y) + (x * z) by A31, A32, Def13 ;
::_thesis: verum
end;
supposeA33: ( x = 2 & y = 1 & z = 2 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A34: ( x * y = 2 & x * z = 1 ) by Def14;
 y + z = 0 by A33, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A34, Def13 ;
::_thesis: verum
end;
supposeA35: ( x = 2 & y = 2 & z = 1 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A36: ( x * y = 1 & x * z = 2 ) by Def14;
 y + z = 0 by A35, Def13;
hence x * (y + z) = 0 by Def14
.= (x * y) + (x * z) by A36, Def13 ;
::_thesis: verum
end;
supposeA37: ( x = 2 & y = 2 & z = 2 ) ; ::_thesis: x * (y + z) = (x * y) + (x * z)
then A38: x * y = 1 by Def14;
 y + z = 1 by A37, Def13;
hence x * (y + z) = 2 by A37, Def14
.= (x * y) + (x * z) by A37, A38, Def13 ;
::_thesis: verum
end;
end;
end;
hence  x * (y + z) = (x * y) + (x * z) ; ::_thesis: verum
end;
end;

theorem Th26: :: MOD_2:26
for F being non empty doubleLoopStr st ( for x, y, z being Scalar of F holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) ) holds
F is Field
proof
let F be non empty doubleLoopStr ; ::_thesis: ( ( for x, y, z being Scalar of F holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) ) implies F is Field )
assume A1: for x, y, z being Scalar of F holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) ; ::_thesis: F is Field
A2: for x being Scalar of F st x <> 0. F holds
ex y being Scalar of F st y * x = 1. F
proof
let x be Scalar of F; ::_thesis: ( x <> 0. F implies ex y being Scalar of F st y * x = 1. F )
assume  x <> 0. F ; ::_thesis: ex y being Scalar of F st y * x = 1. F
then consider y being Scalar of F such that
A3: x * y = 1. F by A1;
take  y ; ::_thesis: y * x = 1. F
thus  y * x = 1. F by A1, A3; ::_thesis: verum
end;
A4: now__::_thesis:_for_x,_y,_z_being_Scalar_of_F_holds_
(_x_+_y_=_y_+_x_&_(x_+_y)_+_z_=_x_+_(y_+_z)_&_x_+_(0._F)_=_x_&_x_+_(-_x)_=_0._F_&_x_*_y_=_y_*_x_&_(x_*_y)_*_z_=_x_*_(y_*_z)_&_(1._F)_*_x_=_x_&_x_*_(1._F)_=_x_&_(_x_<>_0._F_implies_ex_y_being_Scalar_of_F_st_x_*_y_=_1._F_)_&_0._F_<>_1._F_&_x_*_(y_+_z)_=_(x_*_y)_+_(x_*_z)_&_(y_+_z)_*_x_=_(y_*_x)_+_(z_*_x)_)
let x, y, z be Scalar of F; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus  ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. F) = x & x + (- x) = 0. F & x * y = y * x & (x * y) * z = x * (y * z) & (1. F) * x = x & x * (1. F) = x & ( x <> 0. F implies ex y being Scalar of F st x * y = 1. F ) & 0. F <> 1. F & x * (y + z) = (x * y) + (x * z) ) by A1; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = x * (y + z) by A1
.= (x * y) + (x * z) by A1
.= (y * x) + (x * z) by A1
.= (y * x) + (z * x) by A1 ; ::_thesis: verum
end;
 F is right_complementable
proof
let v be Element of F; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
take  - v ; :: according to ALGSTR_0:def_11 ::_thesis: v + (- v) = 0. F
thus  v + (- v) = 0. F by A4; ::_thesis: verum
end;
hence  F is Field by A2, A4, GROUP_1:def_3, GROUP_1:def_12, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, STRUCT_0:def_8, VECTSP_1:def_6, VECTSP_1:def_7, VECTSP_1:def_9; ::_thesis: verum
end;

theorem Th27: :: MOD_2:27
Z_3 is Fanoian Field
proof
set F = Z_3 ;
reconsider a = 0. Z_3, b = 1. Z_3 as Element of {0,1,2} ;
now__::_thesis:_for_x,_y,_z_being_Scalar_of_Z_3_holds_
(_x_+_y_=_y_+_x_&_(x_+_y)_+_z_=_x_+_(y_+_z)_&_x_+_(0._Z_3)_=_x_&_x_+_(-_x)_=_0._Z_3_&_x_*_y_=_y_*_x_&_(x_*_y)_*_z_=_x_*_(y_*_z)_&_(1._Z_3)_*_x_=_x_&_x_*_(1._Z_3)_=_x_&_(_x_<>_0._Z_3_implies_ex_y_being_Scalar_of_Z_3_st_x_*_y_=_1._Z_3_)_&_0._Z_3_<>_1._Z_3_&_x_*_(y_+_z)_=_(x_*_y)_+_(x_*_z)_)
let x, y, z be Scalar of Z_3; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus  ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) ) ::_thesis: verum
proof
reconsider X = x, Y = y, Z = z as Element of {0,1,2} ;
A1: ( x * y = X * Y & x * z = X * Z ) by Th23;
thus x + y = X + Y by Th23
.= Y + X by Th25
.= y + x by Th23 ; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (x + y) + z = (X + Y) + Z by Th24
.= X + (Y + Z) by Th25
.= x + (y + z) by Th24 ; ::_thesis: ( x + (0. Z_3) = x & x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x + (0. Z_3) = X + a by Th23
.= x by Th25 ; ::_thesis: ( x + (- x) = 0. Z_3 & x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
 - x = - X by Th23;
hence x + (- x) = X + (- X) by Th23
.= 0. Z_3 by Th25 ;
::_thesis: ( x * y = y * x & (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x * y = X * Y by Th23
.= Y * X by Th25
.= y * x by Th23 ; ::_thesis: ( (x * y) * z = x * (y * z) & (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (x * y) * z = (X * Y) * Z by Th24
.= X * (Y * Z) by Th25
.= x * (y * z) by Th24 ; ::_thesis: ( (1. Z_3) * x = x & x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus (1. Z_3) * x = b * X by Th23
.= x by Th25 ; ::_thesis: ( x * (1. Z_3) = x & ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus x * (1. Z_3) = X * b by Th23
.= b * X by Th25
.= x by Th25 ; ::_thesis: ( ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) & 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
thus  ( x <> 0. Z_3 implies ex y being Scalar of Z_3 st x * y = 1. Z_3 ) ::_thesis: ( 0. Z_3 <> 1. Z_3 & x * (y + z) = (x * y) + (x * z) )
proof
assume  x <> 0. Z_3 ; ::_thesis: ex y being Scalar of Z_3 st x * y = 1. Z_3
then consider Y being Element of {0,1,2} such that
A2: X * Y = b by Th25;
reconsider y = Y as Scalar of Z_3 ;
take  y ; ::_thesis: x * y = 1. Z_3
thus  x * y = 1. Z_3 by A2, Th23; ::_thesis: verum
end;
thus  0. Z_3 <> 1. Z_3 ; ::_thesis: x * (y + z) = (x * y) + (x * z)
 y + z = Y + Z by Th23;
hence x * (y + z) = X * (Y + Z) by Th23
.= (X * Y) + (X * Z) by Th25
.= (x * y) + (x * z) by A1, Th23 ;
::_thesis: verum
end;
end;
then reconsider F = Z_3 as Field by Th26;
(1. F) + (1. F) = b + b by Def15
.= 2 by Def13 ;
hence  Z_3 is Fanoian Field by Th22, VECTSP_1:def_19; ::_thesis: verum
end;

registration
cluster Z_3  ->  right_complementable almost_left_invertible strict associative commutative well-unital distributive Fanoian Abelian add-associative right_zeroed ;
coherence
 ( Z_3 is Fanoian & Z_3 is add-associative & Z_3 is right_zeroed & Z_3 is right_complementable & Z_3 is Abelian & Z_3 is commutative & Z_3 is associative & Z_3 is well-unital & Z_3 is distributive & Z_3 is almost_left_invertible ) by Th27;
end;

Lm8:  for UN being Universe holds the carrier of Z_3 in UN
proof
let UN be Universe; ::_thesis: the carrier of Z_3 in UN
reconsider a = 0 , b = 1, c = 2 as Element of UN by Th21;
 {a,b,c} is Element of UN by Th19;
hence  the carrier of Z_3 in UN ; ::_thesis: verum
end;

theorem Th28: :: MOD_2:28
for D, D9 being non empty set
for UN being Universe
for f being Function of D,D9 st D in UN & D9 in UN holds
f in UN
proof
let D, D9 be non empty set ; ::_thesis: for UN being Universe
for f being Function of D,D9 st D in UN & D9 in UN holds
f in UN
let UN be Universe; ::_thesis: for f being Function of D,D9 st D in UN & D9 in UN holds
f in UN
let f be Function of D,D9; ::_thesis: ( D in UN & D9 in UN implies f in UN )
assume  ( D in UN & D9 in UN ) ; ::_thesis: f in UN
then A1: Funcs (D,D9) in UN by CLASSES2:61;
 f in Funcs (D,D9) by FUNCT_2:8;
hence  f in UN by A1, ORDINAL1:10; ::_thesis: verum
end;

Lm9:  for D being non empty set
for UN being Universe holds
( ( for f being BinOp of D st D in UN holds
f in UN ) & ( for f being UnOp of D st D in UN holds
f in UN ) )
proof
let D be non empty set ; ::_thesis: for UN being Universe holds
( ( for f being BinOp of D st D in UN holds
f in UN ) & ( for f being UnOp of D st D in UN holds
f in UN ) )
let UN be Universe; ::_thesis: ( ( for f being BinOp of D st D in UN holds
f in UN ) & ( for f being UnOp of D st D in UN holds
f in UN ) )
now__::_thesis:_for_f_being_BinOp_of_D_st_D_in_UN_holds_
f_in_UN
let f be BinOp of D; ::_thesis: ( D in UN implies f in UN )
assume A1: D in UN ; ::_thesis: f in UN
then  [:D,D:] in UN by CLASSES2:61;
then A2: Funcs ([:D,D:],D) in UN by A1, CLASSES2:61;
 f in Funcs ([:D,D:],D) by FUNCT_2:8;
hence  f in UN by A2, ORDINAL1:10; ::_thesis: verum
end;
hence  ( ( for f being BinOp of D st D in UN holds
f in UN ) & ( for f being UnOp of D st D in UN holds
f in UN ) ) by Th28; ::_thesis: verum
end;

theorem :: MOD_2:29
for UN being Universe holds
( the carrier of Z_3 in UN & the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN )
proof
let UN be Universe; ::_thesis: ( the carrier of Z_3 in UN & the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN )
thus  the carrier of Z_3 in UN by Lm8; ::_thesis: ( the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN )
hence  ( the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN ) by Lm9, ORDINAL1:10; ::_thesis: verum
end;