let G, H be Ring; :: thesis: 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; :: thesis: ( G <= H implies ex f being Function of G,H st F = RingMorphismStr(# G,H,f #) )
assume G <= H ; :: thesis: 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 ; :: thesis: F = RingMorphismStr(# G,H,f #)
thus F = RingMorphismStr(# G,H,f #) by A1; :: thesis: verum