let U1, U2 be Universal_Algebra; :: thesis: ( 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
; :: thesis: 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))
let B be MSSubset of (MSAlg U2); :: thesis: ( 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 A2:
B = the Sorts of (MSAlg U1)
; :: thesis: 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))
A3:
the Sorts of (MSAlg U2) is MSSubset of (MSAlg U2)
by PBOOLE:def 23;
A4:
MSSign U1 = MSSign U2
by A1, Th7;
let o be OperSymbol of (MSSign U2); :: thesis: 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;
A5:
dom (Den o,(MSAlg U2)) = Args o,(MSAlg U2)
by FUNCT_2:def 1;
A6:
Args o,(MSAlg U2) = ((the Sorts of (MSAlg U2) # ) * the Arity of (MSSign U2)) . o
by MSUALG_1:def 9;
((B # ) * the Arity of (MSSign U1)) . a c= ((the Sorts of (MSAlg U2) # ) * the Arity of (MSSign U2)) . o
then
Args a,(MSAlg U1) c= dom (Den o,(MSAlg U2))
by A2, A4, A5, A6, MSUALG_1:def 9;
then
dom ((Den o,(MSAlg U2)) | (Args a,(MSAlg U1))) = Args a,(MSAlg U1)
by RELAT_1:91;
then A8:
dom ((Den o,(MSAlg U2)) | (Args a,(MSAlg U1))) = dom (Den a,(MSAlg U1))
by FUNCT_2:def 1;
set X = Args a,(MSAlg U1);
set Y = dom (Den a,(MSAlg U1));
A9:
dom (Den a,(MSAlg U1)) = (dom (Den o,(MSAlg U2))) /\ (Args a,(MSAlg U1))
by A8, 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
let x be
set ;
:: thesis: ( x in dom (Den a,(MSAlg U1)) implies (Den o,(MSAlg U2)) . x = (Den a,(MSAlg U1)) . x )
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 A9, XBOOLE_0:def 4;
then A10:
x in (len (the_arity_of a)) -tuples_on (the_sort_of (MSAlg U1))
by MSUALG_1:11;
A11:
(
MSAlg U1 = MSAlgebra(#
(MSSorts U1),
(MSCharact U1) #) &
MSAlg U2 = MSAlgebra(#
(MSSorts U2),
(MSCharact U2) #) )
by MSUALG_1:def 16;
reconsider cc = the
carrier of
U1 as non
empty Subset of
U2 by A1, UNIALG_2:def 8;
now let n be
set ;
:: thesis: ( n in dom (Opers U2,cc) implies (Opers U2,cc) . n is Function )assume A12:
n in dom (Opers U2,cc)
;
:: thesis: (Opers U2,cc) . n is FunctionA13:
rng (Opers U2,cc) c= PFuncs (cc * ),
cc
by FINSEQ_1:def 4;
(Opers U2,cc) . n in rng (Opers U2,cc)
by A12, FUNCT_1:def 5;
hence
(Opers U2,cc) . n is
Function
by A13, PARTFUN1:120;
:: thesis: verum end;
then reconsider f =
Opers U2,
cc as
Function-yielding Function by FUNCOP_1:def 6;
set ff1 =
(*--> 0 ) * (signature U1);
set ff2 =
(dom (signature U1)) --> z;
set gg2 =
(dom (signature U2)) --> z;
reconsider gg1 =
(*--> 0 ) * (signature U2) as
Function of
(dom (signature U2)),
({0 } * ) by MSUALG_1:7;
A14:
MSSign U2 = ManySortedSign(#
{0 },
(dom (signature U2)),
gg1,
((dom (signature U2)) --> z) #)
by MSUALG_1:16;
A15:
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 A14, FUNCT_1:def 5;
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
the
carrier of
U1 is
Component of the
Sorts of
(MSAlg U1)
by TARSKI:def 1;
then A16:
x in (len (the_arity_of a)) -tuples_on the
carrier of
U1
by A10, MSUALG_1:def 17;
reconsider ff1 =
(*--> 0 ) * (signature U1) as
Function of
(dom (signature U1)),
({0 } * ) by MSUALG_1:7;
A17:
MSSign U1 = ManySortedSign(#
{0 },
(dom (signature U1)),
ff1,
((dom (signature U1)) --> z) #)
by MSUALG_1:16;
consider n being
Nat such that A18:
dom (signature U2) = Seg n
by FINSEQ_1:def 2;
a in Seg n
by A14, A18;
then reconsider a =
a as
Element of
NAT ;
U1,
U2 are_similar
by A1, UNIALG_2:16;
then A19:
signature U1 = signature U2
by UNIALG_2:def 2;
then A20:
(signature U1) . a in rng (signature U1)
by A14, FUNCT_1:def 5;
A21:
rng (signature U1) c= NAT
by FINSEQ_1:def 4;
dom (*--> 0 ) = NAT
by FUNCT_2:def 1;
then
a in dom ((*--> 0 ) * (signature U1))
by A14, A19, A20, A21, FUNCT_1:21;
then A22:
the
Arity of
(MSSign U1) . a = (*--> 0 ) . ((signature U1) . a)
by A17, FUNCT_1:22;
reconsider sig =
(signature U1) . a as
Element of
NAT by A20, A21;
A23:
the
Arity of
(MSSign U1) . a = sig |-> 0
by A22, PBOOLE:def 20;
U1,
U2 are_similar
by A1, UNIALG_2:16;
then A24:
signature U1 = signature U2
by UNIALG_2:def 2;
reconsider ar = the
Arity of
(MSSign U1) . a as
FinSequence by A23;
x in (len ar) -tuples_on the
carrier of
U1
by A16, MSUALG_1:def 6;
then
x in sig -tuples_on the
carrier of
U1
by A23, FINSEQ_1:def 18;
then A25:
x in (arity op) -tuples_on the
carrier of
U1
by A14, A24, UNIALG_1:def 11;
a in dom the
charact of
U2
by A14, A15;
then A26:
o in dom (Opers U2,cc)
by UNIALG_2:def 7;
cc is
opers_closed
by A1, UNIALG_2:def 8;
then A27:
cc is_closed_on op
by UNIALG_2:def 5;
reconsider a =
a as
OperSymbol of
(MSSign U1) ;
(Den a,(MSAlg U1)) . x =
((MSCharact U1) . o) . x
by A11, 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 A26, UNIALG_2:def 7
.=
(op | ((arity op) -tuples_on cc)) . x
by A27, UNIALG_2:def 6
.=
(the charact of U2 . o) . x
by A25, FUNCT_1:72
.=
(the Charact of (MSAlg U2) . o) . x
by A11, 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
;
:: thesis: 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 A9, FUNCT_1:68; :: thesis: verum