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