let U1 be Universal_Algebra; :: thesis: for o being OperSymbol of (MSSign U1) holds Den (o,(MSAlg U1)) is operation of U1
let o be OperSymbol of (MSSign U1); :: thesis: Den (o,(MSAlg U1)) is operation of U1
A1: dom (signature U1) = dom the charact of U1 by Lm1;
( Den (o,(MSAlg U1)) = the charact of U1 . o & the carrier' of (MSSign U1) = dom (signature U1) ) by Th12, MSUALG_1:def 8;
hence Den (o,(MSAlg U1)) is operation of U1 by A1, FUNCT_1:def 3; :: thesis: verum