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

proof

let x be object ; :: thesis: ( x in D implies x is Morphism of G,H )
assume x in D ; :: thesis: x is Morphism of G,H
then ex f being Element of Maps (G,H) st
( x = RingMorphismStr(# G,H,f #) & f is linear ) ;
hence x is Morphism of G,H by Lm5; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x is Morphism of G,H implies x in D )
assume x is Morphism of G,H ; :: thesis: x in D
then reconsider x = x as Morphism of G,H ;
A6: ( dom x = G & cod x = H ) by A1, Def8;
then reconsider f = the Fun of x as Function of G,H ;
reconsider g = f as Element of Maps (G,H) by FUNCT_2:8;
A7: x = RingMorphismStr(# G,H,g #) by A6;
the Fun of x is linear by Lm3;
hence x in D by A7; :: thesis: verum

end;

reconsider D = D as RingMorphism_DOMAIN of G,H by A4, Th13;
take D ; :: thesis: 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; :: thesis: verum