[: the carrier of G, the carrier of F:] <> {} by ZFMISC_1:90;
hence ModuleStr(# [: the carrier of G, the carrier of F:],(prod_ADD (G,F)),(prod_ZERO (G,F)),(prod_MLT (G,F)) #) is non empty strict ModuleStr over K ; :: thesis: verum