let U1, U2 be Universal_Algebra; ( U1 is SubAlgebra of U2 implies for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) )
assume A1:
U1 is SubAlgebra of U2
; for B being MSSubset of (MSAlg U2) st B = the Sorts of (MSAlg U1) holds
for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
A2:
MSSign U1 = MSSign U2
by A1, Th7;
A3:
MSSign U1 = MSSign U2
by A1, Th7;
let B be MSSubset of (MSAlg U2); ( B = the Sorts of (MSAlg U1) implies for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1))) )
assume A4:
B = the Sorts of (MSAlg U1)
; for o being OperSymbol of (MSSign U2)
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
let o be OperSymbol of (MSSign U2); for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
reconsider a = o as Element of the carrier' of (MSSign U1) by A1, Th7;
set X = Args (a,(MSAlg U1));
set Y = dom (Den (a,(MSAlg U1)));
( the Sorts of (MSAlg U2) is MSSubset of (MSAlg U2) & B c= the Sorts of (MSAlg U2) )
by PBOOLE:def 18;
then A5:
((B #) * the Arity of (MSSign U1)) . a c= (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . o
by A3, MSUALG_2:2;
( dom (Den (o,(MSAlg U2))) = Args (o,(MSAlg U2)) & Args (o,(MSAlg U2)) = (( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . o )
by FUNCT_2:def 1, MSUALG_1:def 4;
then
Args (a,(MSAlg U1)) c= dom (Den (o,(MSAlg U2)))
by A4, A2, A5, MSUALG_1:def 4;
then
dom ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) = Args (a,(MSAlg U1))
by RELAT_1:62;
then
dom ((Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))) = dom (Den (a,(MSAlg U1)))
by FUNCT_2:def 1;
then A6:
dom (Den (a,(MSAlg U1))) = (dom (Den (o,(MSAlg U2)))) /\ (Args (a,(MSAlg U1)))
by RELAT_1:61;
for x being object st x in dom (Den (a,(MSAlg U1))) holds
(Den (o,(MSAlg U2))) . x = (Den (a,(MSAlg U1))) . x
proof
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 ;
( 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)))
;
(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
;
verum
end;
hence
for a being OperSymbol of (MSSign U1) st a = o holds
Den (a,(MSAlg U1)) = (Den (o,(MSAlg U2))) | (Args (a,(MSAlg U1)))
by A6, FUNCT_1:46; verum