consider F being RingMorphism such that
A2: ( dom F = G & cod F = H ) by A1, Def8;
set S = RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #);
( RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) is RingMorphism & dom RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = G & cod RingMorphismStr(# the Dom of F,the Cod of F,the Fun of F #) = H ) by A2, Lm2;
hence ex b₁ being strict RingMorphism st
( dom b₁ = G & cod b₁ = H ) ; :: thesis: verum