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 23;
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:3;
( 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 9;
then
Args a,(MSAlg U1) c= dom (Den o,(MSAlg U2))
by A4, A2, A5, MSUALG_1:def 9;
then
dom ((Den o,(MSAlg U2)) | (Args a,(MSAlg U1))) = Args a,(MSAlg U1)
by RELAT_1:91;
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:90;
for x being set 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 16;
then
the
Sorts of
(MSAlg U1) = 0 .--> the
carrier of
U1
by MSUALG_1:def 14;
then
rng the
Sorts of
(MSAlg U1) = {the carrier of U1}
by FUNCOP_1:14;
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 8;
let x be
set ;
( 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 16;
U1,
U2 are_similar
by A1, UNIALG_2:16;
then A9:
signature U1 = signature U2
by UNIALG_2:def 2;
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:11;
then A10:
x in (len (the_arity_of a)) -tuples_on the
carrier of
U1
by A7, MSUALG_1:def 17;
reconsider gg1 =
(*--> 0 ) * (signature U2) as
Function of
(dom (signature U2)),
({0 } * ) by MSUALG_1:7;
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:7;
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:16;
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 11
.=
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 5;
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:16;
then A16:
signature U1 = signature U2
by UNIALG_2:def 2;
then A17:
(signature U1) . a in rng (signature U1)
by A12, FUNCT_1:def 5;
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:21, MSUALG_1:16;
then
the
Arity of
(MSSign U1) . a = (*--> 0 ) . ((signature U1) . a)
by FUNCT_1:22;
then A18:
the
Arity of
(MSSign U1) . a = sig |-> 0
by PBOOLE:def 20;
then 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 6;
then
x in sig -tuples_on the
carrier of
U1
by A18, FINSEQ_1:def 18;
then A19:
x in (arity op) -tuples_on the
carrier of
U1
by A12, A9, UNIALG_1:def 11;
now let n be
set ;
( n in dom (Opers U2,cc) implies (Opers U2,cc) . n is Function )assume
n in dom (Opers U2,cc)
;
(Opers U2,cc) . n is Functionthen
(
rng (Opers U2,cc) c= PFuncs (cc * ),
cc &
(Opers U2,cc) . n in rng (Opers U2,cc) )
by FINSEQ_1:def 4, FUNCT_1:def 5;
hence
(Opers U2,cc) . n is
Function
by PARTFUN1:120;
verum end;
then reconsider f =
Opers U2,
cc as
Function-yielding Function by FUNCOP_1:def 6;
cc is
opers_closed
by A1, UNIALG_2:def 8;
then A20:
cc is_closed_on op
by UNIALG_2:def 5;
a in dom the
charact of
U2
by A12, A14;
then A21:
o in dom (Opers U2,cc)
by UNIALG_2:def 7;
reconsider a =
a as
OperSymbol of
(MSSign U1) ;
MSAlg U1 = MSAlgebra(#
(MSSorts U1),
(MSCharact U1) #)
by MSUALG_1:def 16;
then (Den a,(MSAlg U1)) . x =
((MSCharact U1) . o) . x
by MSUALG_1:def 11
.=
(the charact of U1 . o) . x
by MSUALG_1:def 15
.=
(f . o) . x
by A1, UNIALG_2:def 8
.=
(op /. cc) . x
by A21, UNIALG_2:def 7
.=
(op | ((arity op) -tuples_on cc)) . x
by A20, UNIALG_2:def 6
.=
(the charact of U2 . o) . x
by A19, FUNCT_1:72
.=
(the Charact of (MSAlg U2) . o) . x
by A8, MSUALG_1:def 15
.=
(Den o,(MSAlg U2)) . x
by MSUALG_1:def 11
;
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:68; verum