set i = ZERO (G,H);
fun (ZERO (G,H)) = ZeroMap (G,H) ;
hence ZERO (G,H) is strict Morphism of G,H by Th5; :: thesis: verum