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 ;
( x is strict Morphism of G,H implies x in D )
assume
x is
strict Morphism of
G,
H
;
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
;
verum
end;
A4:
for x being object st x in D holds
x is strict Morphism of G,H
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
; 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; verum