let G, H be Ring; for F being Morphism of G,H st G <= H holds
ex f being Function of G,H st F = RingMorphismStr(# G,H,f #)
let F be Morphism of G,H; ( G <= H implies ex f being Function of G,H st F = RingMorphismStr(# G,H,f #) )
assume
G <= H
; ex f being Function of G,H st F = RingMorphismStr(# G,H,f #)
then consider f being Function of G,H such that
A1:
F = RingMorphismStr(# G,H,f #)
and
f is linear
by Lm7;
take
f
; F = RingMorphismStr(# G,H,f #)
thus
F = RingMorphismStr(# G,H,f #)
by A1; verum