consider m being Morphism of G,H;
m is RingMorphism ;
hence ex b₁ being Morphism of G,H st b₁ is strict ; :: thesis: verum