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 11;
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 6
.= (MSCharact U2) . o by A3, A1, Th9
.= the charact of U2 . o by MSUALG_1:def 10 ;
A5: dom (signature U1) = dom the charact of U1 by Lm1;
signature U1 = signature U2 by A2;
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 8;
hence Den (o,((MSAlg U2) Over (MSSign U1))) is operation of U2 by A4, A5, FUNCT_1:def 3; :: thesis: verum