set D = { LModMorphismStr(# G,H,f #) where f is Element of Maps G,H : f is linear } ;
ZeroMap G,H is Element of Funcs the carrier of G,the carrier of H by FUNCT_2:11;
then reconsider f0 = ZeroMap G,H as Element of Maps G,H by GRCAT_1:def 26;
f0 is linear by MOD_2:8;
then LModMorphismStr(# G,H,f0 #) in { LModMorphismStr(# G,H,f #) where f is Element of Maps G,H : f is linear } ;
then reconsider D = { LModMorphismStr(# G,H,f #) where f is Element of Maps G,H : f is linear } as non empty set ;
A1: 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 linear ) ;
hence x is strict Morphism of G,H by MOD_2:12; :: thesis: verum

end;

then A2: for x being Element of D holds x is strict Morphism of G,H ;
A3: 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 & cod x = H ) by MOD_2:def 11;
then A4: ( the Dom of x = G & the Cod of x = H ) by MOD_2:def 6, MOD_2:def 7;
A5: the Fun of x is linear by MOD_2:10;
reconsider f = the Fun of x as Function of G,H by A4;
f is Element of Funcs the carrier of G,the carrier of H by FUNCT_2:11;
then reconsider g = f as Element of Maps G,H by GRCAT_1:def 26;
x = LModMorphismStr(# G,H,g #) by A4;
hence x in D by A5; :: thesis: verum

end;

reconsider D = D as LModMorphism_DOMAIN of G,H by A2, Th4;
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 A1, A3; :: thesis: verum