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 ;
hence ex b₁ being RingMorphismStr st
( b₁ is strict & b₁ is RingMorphism-like ) by Def5; :: thesis: verum