let F be strict RingMorphism; ex G, H being Ring ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
consider G, H being Ring such that
A1:
G <= H
and
dom F = G
and
cod F = H
and
A2:
F is Morphism of G,H
by Lm6;
reconsider F9 = F as Morphism of G,H by A2;
consider f being Function of G,H such that
A3:
( F9 = RingMorphismStr(# G,H,f #) & f is linear )
by A1, Lm7;
take
G
; ex H being Ring ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
take
H
; ex f being Function of G,H st
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
take
f
; ( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
thus
( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )
by A3; verum