consider F being RingMorphism such that
A2: ( dom F = G & cod F = H ) by A1;
set S = RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #);
A3: ( 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;
RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is RingMorphism by Lm2;
hence ex b₁ being strict RingMorphism st
( dom b₁ = G & cod b₁ = H ) by A3; :: thesis: verum