consider G being Ring;
set i = RingMorphismStr(# G,G,(id G) #);
fun RingMorphismStr(# G,G,(id G) #) = id G ;
then RingMorphismStr(# G,G,(id G) #) is RingMorphism-like by Def6;
hence ex b₁ being RingMorphismStr st
( b₁ is strict & b₁ is RingMorphism-like ) ; :: thesis: verum