thus not the carrier of (MSSign A,P) is empty by Def15; :: according to STRUCT_0:def 1 :: thesis: not MSSign A,P is void
consider g being OperSymbol of A;
consider x being Element of dom (Den g,A);
reconsider x = x as Element of the carrier of A * ;
( union P = the carrier of A & rng x c= the carrier of A ) by EQREL_1:def 6;
then consider q being Function such that
A1: ( dom q = dom x & rng q c= P & x in product q ) by Th6;
dom x = Seg (len x) by FINSEQ_1:def 3;
then reconsider q = q as FinSequence by A1, FINSEQ_1:def 2;
reconsider q = q as FinSequence of P by A1, FINSEQ_1:def 4;
reconsider q = q as Element of P * by FINSEQ_1:def 11;
( product q meets dom (Den g,A) & the carrier' of (MSSign A,P) = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ) by A1, Def15, XBOOLE_0:3;
then [g,q] in the carrier' of (MSSign A,P) ;
hence not the carrier' of (MSSign A,P) is empty ; :: according to STRUCT_0:def 13 :: thesis: verum