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

g * (ID G) = g :: thesis: verum

( 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

thus
for g being strict LModMorphism of R st dom g = G holds
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;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

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;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