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