set V = LModObjects (UN,R);
let f be Element of Morphs (LModObjects (UN,R)); :: thesis: f is strict
ex G, H being strict Element of LModObjects (UN,R) st f is strict Morphism of G,H by Def7;
hence f is strict ; :: thesis: verum