A1: 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 A1;
hence o `1 is OperSymbol of A by MCART_1:7; :: thesis: verum