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
reconsider f = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
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 13;
hence Den o,(MSAlg U1) is operation of U1 by A1, FUNCT_1:def 5; :: thesis: verum