let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_similar implies for o being OperSymbol of (MSSign U1) holds Den o,((MSAlg U2) Over (MSSign U1)) is operation of U2 )
assume A1: U1,U2 are_similar ; :: thesis: for o being OperSymbol of (MSSign U1) holds Den o,((MSAlg U2) Over (MSSign U1)) is operation of U2
then A2: signature U1 = signature U2 by UNIALG_2:def 2;
let o be OperSymbol of (MSSign U1); :: thesis: Den o,((MSAlg U2) Over (MSSign U1)) is operation of U2
set A = (MSAlg U2) Over (MSSign U1);
A3: MSSign U1 = MSSign U2 by A1, Th10;
A4: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 16;
A5: Den o,((MSAlg U2) Over (MSSign U1)) = the Charact of ((MSAlg U2) Over (MSSign U1)) . o by MSUALG_1:def 11
.= (MSCharact U2) . o by A3, A4, Th9
.= the charact of U2 . o by MSUALG_1:def 15 ;
reconsider f = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A7: ( 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;
A8: dom (signature U1) = dom the charact of U1 by Lm1;
then dom the charact of U1 = dom the charact of U2 by A2, Lm1;
hence Den o,((MSAlg U2) Over (MSSign U1)) is operation of U2 by A5, A7, A8, FUNCT_1:def 5; :: thesis: verum