set R = nabla the carrier of M;
let v, v9, w, w9 be Element of M; :: according to ALGSTR_4:def 3 :: thesis: ( v in Class ((nabla the carrier of M),v9) & w in Class ((nabla the carrier of M),w9) implies v * w in Class ((nabla the carrier of M),(v9 * w9)) )
assume ( v in Class ((nabla the carrier of M),v9) & w in Class ((nabla the carrier of M),w9) ) ; :: thesis: v * w in Class ((nabla the carrier of M),(v9 * w9))
then A1: not M is empty ;
then Class ((nabla the carrier of M),(v9 * w9)) = the carrier of M by EQREL_1:26;
hence v * w in Class ((nabla the carrier of M),(v9 * w9)) by A1, SUBSET_1:def 1; :: thesis: verum