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)
let n be Nat; :: thesis: ( n in dom the charact of U1 implies n is OperSymbol of (MSSign U1) )
assume A1: n in dom the charact of U1 ; :: thesis: n is OperSymbol of (MSSign U1)
dom (signature U1) = dom the charact of U1 by Lm1;
hence n is OperSymbol of (MSSign U1) by A1, MSUALG_1:def 13; :: thesis: verum