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: Den o,(MSAlg U1) = the charact of U1 . o by Th12;
reconsider f = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A3: ( the carrier of (MSSign U1) = {0 } & the carrier' of (MSSign U1) = dom (signature U1) & the Arity of (MSSign U1) = f & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 ) by MSUALG_1:def 13;
dom (signature U1) = dom the charact of U1 by Lm1;
hence Den o,(MSAlg U1) is operation of U1 by A1, A3, FUNCT_1:def 5; :: thesis: verum