let U1 be Universal_Algebra; :: thesis: for o being OperSymbol of (MSSign U1) holds Den (o,(MSAlg U1)) = the charact of U1 . o
let o be OperSymbol of (MSSign U1); :: thesis: Den (o,(MSAlg U1)) = the charact of U1 . o
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 11;
hence Den (o,(MSAlg U1)) = (MSCharact U1) . o by MSUALG_1:def 6
.= the charact of U1 . o by MSUALG_1:def 10 ;
:: thesis: verum