let U1 be Universal_Algebra; :: thesis: for n being Nat st n in dom the charact of U1 holds
n is OperSymbol of (MSSign U1)
A1: dom (signature U1) = dom the charact of U1 by Lm1;
let n be Nat; :: thesis: ( n in dom the charact of U1 implies n is OperSymbol of (MSSign U1) )
assume n in dom the charact of U1 ; :: thesis: n is OperSymbol of (MSSign U1)
hence n is OperSymbol of (MSSign U1) by A1, MSUALG_1:def 8; :: thesis: verum