( o in the carrier' of (MSSign A,P) & 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 ex f being OperSymbol of A ex p being Element of P * st
( o = [f,p] & product p meets dom (Den f,A) ) ;
hence o `2 is Element of P * by MCART_1:7; :: thesis: verum