A2: 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) ) by A2;
hence o `2 is Element of P * by MCART_1:7; :: thesis: verum