thus
not the carrier of (MSSign A,P) is empty
by Def15; STRUCT_0:def 1 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 * ;
A1:
union P = the carrier of A
by EQREL_1:def 6;
rng x c= the carrier of A
;
then consider q being Function such that
A2:
dom q = dom x
and
A3:
rng q c= P
and
A4:
x in product q
by A1, Th6;
dom x = Seg (len x)
by FINSEQ_1:def 3;
then reconsider q = q as FinSequence by A2, FINSEQ_1:def 2;
reconsider q = q as FinSequence of P by A3, FINSEQ_1:def 4;
reconsider q = q as Element of P * by FINSEQ_1:def 11;
A5:
product q meets dom (Den g,A)
by A4, XBOOLE_0:3;
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 Def15;
then
[g,q] in the carrier' of (MSSign A,P)
by A5;
hence
not the carrier' of (MSSign A,P) is empty
; STRUCT_0:def 13 verum