MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 11;
then the Sorts of (MSAlg U1) = 0 .--> the carrier of U1 by MSUALG_1:def 9;
then rng the Sorts of (MSAlg U1) = { the carrier of U1} by FUNCOP_1:8;
then A7: the carrier of U1 is Component of the Sorts of (MSAlg U1) by TARSKI:def 1;
reconsider cc = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def 7;
let x be object ; :: thesis: ( x in dom (Den (a,(MSAlg U1))) implies (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x )
A8: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 11;
U1,U2 are_similar by A1, UNIALG_2:13;
then A9: signature U1 = signature U2 ;
assume x in dom (Den (a,(MSAlg U1))) ; :: thesis: (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x
then x in Args (a,(MSAlg U1)) by A6, XBOOLE_0:def 4;
then x in (len (the_arity_of a)) -tuples_on (the_sort_of (MSAlg U1)) by MSUALG_1:6;
then A10: x in (len (the_arity_of a)) -tuples_on the carrier of U1 by A7, MSUALG_1:def 12;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
set ff1 = (*--> 0) * (signature U1);
set ff2 = (dom (signature U1)) --> z;
set gg2 = (dom (signature U2)) --> z;
reconsider ff1 = (*--> 0) * (signature U1) as Function of (dom (signature U1)),({0} *) by MSUALG_1:2;
consider n being Nat such that
A11: dom (signature U2) = Seg n by FINSEQ_1:def 2;
A12: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10;
then A13: a in Seg n by A11;
A14: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def 3
.= Seg (len (signature U2)) by UNIALG_1:def 4
.= dom (signature U2) by FINSEQ_1:def 3 ;
then reconsider op = the charact of U2 . a as operation of U2 by A12, FUNCT_1:def 3;
reconsider a = a as Element of NAT by A13;
A15: rng (signature U1) c= NAT by FINSEQ_1:def 4;
U1,U2 are_similar by A1, UNIALG_2:13;
then A16: signature U1 = signature U2 ;
then A17: (signature U1) . a in rng (signature U1) by A12, FUNCT_1:def 3;
then reconsider sig = (signature U1) . a as Element of NAT by A15;
dom (*--> 0) = NAT by FUNCT_2:def 1;
then ( MSSign U1 = ManySortedSign(# {0},(dom (signature U1)),ff1,((dom (signature U1)) --> z) #) & a in dom ((*--> 0) * (signature U1)) ) by A12, A16, A17, A15, FUNCT_1:11, MSUALG_1:10;
then the Arity of (MSSign U1) . a = (*--> 0) . ((signature U1) . a) by FUNCT_1:12;
then A18: the Arity of (MSSign U1) . a = sig |-> 0 by FINSEQ_2:def 6;
reconsider ar = the Arity of (MSSign U1) . a as FinSequence ;
x in (len ar) -tuples_on the carrier of U1 by A10, MSUALG_1:def 1;
then x in sig -tuples_on the carrier of U1 by A18, CARD_1:def 7;
then A19: x in (arity op) -tuples_on the carrier of U1 by A12, A9, UNIALG_1:def 4;
for n being object st n in dom (Opers (U2,cc)) holds
(Opers (U2,cc)) . n is Function ;
then reconsider f = Opers (U2,cc) as Function-yielding Function by FUNCOP_1:def 6;
cc is opers_closed by A1, UNIALG_2:def 7;
then A20: cc is_closed_on op ;
a in dom the charact of U2 by A12, A14;
then A21: o in dom (Opers (U2,cc)) by UNIALG_2:def 6;
reconsider a = a as OperSymbol of (MSSign U1) ;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 11;
then (Den (a,(MSAlg U1))) . x = ((MSCharact U1) . o) . x by MSUALG_1:def 6
.= ( the charact of U1 . o) . x by MSUALG_1:def 10
.= (f . o) . x by A1, UNIALG_2:def 7
.= (op /. cc) . x by A21, UNIALG_2:def 6
.= (op | ((arity op) -tuples_on cc)) . x by A20, UNIALG_2:def 5
.= ( the charact of U2 . o) . x by A19, FUNCT_1:49
.= ( the Charact of (MSAlg U2) . o) . x by A8, MSUALG_1:def 10
.= (Den (o,(MSAlg U2))) . x by MSUALG_1:def 6 ;
hence (Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x ; :: thesis: verum