set F = the Morphism of G,H;
set D = { RingMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is linear } ;
consider f being Function of G,H such that
the Morphism of G,H = RingMorphismStr(# G,H,f #)
and
A2:
f is linear
by A1, Lm7;
reconsider f0 = f as Element of Maps (G,H) by FUNCT_2:8;
RingMorphismStr(# G,H,f0 #) in { RingMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is linear }
by A2;
then reconsider D = { RingMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is linear } as non empty set ;
A3:
for x being object st x in D holds
x is Morphism of G,H
then A4:
for x being Element of D holds x is Morphism of G,H
;
A5:
for x being object st x is Morphism of G,H holds
x in D
reconsider D = D as RingMorphism_DOMAIN of G,H by A4, Th13;
take
D
; for x being object holds
( x in D iff x is Morphism of G,H )
thus
for x being object holds
( x in D iff x is Morphism of G,H )
by A3, A5; verum