let R be Ring; :: thesis: for G, H being LeftMod of R
for f being Function of G,H st f is linear holds
LModMorphismStr(# G,H,f #) is strict Morphism of G,H
let G, H be LeftMod of R; :: thesis: for f being Function of G,H st f is linear holds
LModMorphismStr(# G,H,f #) is strict Morphism of G,H
let f be Function of G,H; :: thesis: ( f is linear implies LModMorphismStr(# G,H,f #) is strict Morphism of G,H )
assume A1: f is linear ; :: thesis: LModMorphismStr(# G,H,f #) is strict Morphism of G,H
set F = LModMorphismStr(# G,H,f #);
( dom LModMorphismStr(# G,H,f #) = G & cod LModMorphismStr(# G,H,f #) = H & fun LModMorphismStr(# G,H,f #) = f ) ;
hence LModMorphismStr(# G,H,f #) is strict Morphism of G,H by A1, Th11; :: thesis: verum