thus
not the carrier of (MSSign (A,P)) is empty
by Def14; STRUCT_0:def 1 not MSSign (A,P) is void
set g = the OperSymbol of A;
set x = the Element of dom (Den ( the OperSymbol of A,A));
reconsider x = the Element of dom (Den ( the OperSymbol of A,A)) as Element of the carrier of A * ;
A1:
union P = the carrier of A
by EQREL_1:def 4;
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, Th5;
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 ( the OperSymbol of A,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 Def14;
then
[ the OperSymbol of A,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