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 )
set A = (MSAlg U2) Over (MSSign U1);
A1: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 16;
assume A2: 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 A3: MSSign U1 = MSSign U2 by Th10;
let o be OperSymbol of (MSSign U1); :: thesis: Den o,((MSAlg U2) Over (MSSign U1)) is operation of U2
A4: 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, A1, 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;
A5: dom (signature U1) = dom the charact of U1 by Lm1;
signature U1 = signature U2 by A2, UNIALG_2:def 2;
then ( the carrier' of (MSSign U1) = dom (signature U1) & dom the charact of U1 = dom the charact of U2 ) by A5, Lm1, MSUALG_1:def 13;
hence Den o,((MSAlg U2) Over (MSSign U1)) is operation of U2 by A4, A5, FUNCT_1:def 5; :: thesis: verum