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 object st x is strict Morphism of G,H holds
x in D

proof

let x be object ; :: 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 ;
A3: cod x = H by MOD_2:def 8;
then the Cod of x = H ;
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;
hence x in D ; :: thesis: verum

end;

A4: for x being object st x in D holds
x is strict Morphism of G,H

proof

let x be object ; :: 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 object holds
( x in D iff x is strict Morphism of G,H )
thus for x being object holds
( x in D iff x is strict Morphism of G,H ) by A4, A1; :: thesis: verum