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 Def14;
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 ; :: thesis: verum