let U1, U2 be Universal_Algebra; ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies for B being non empty Subset of U2 st B = the carrier of U1 holds
the charact of U1 = Opers (U2,B) )
set MU1 = MSAlg U1;
set MU2 = MSAlg U2;
A1:
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #)
by MSUALG_1:def 11;
assume A2:
MSAlg U1 is MSSubAlgebra of MSAlg U2
; for B being non empty Subset of U2 st B = the carrier of U1 holds
the charact of U1 = Opers (U2,B)
then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ;
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A2, MSUALG_2:def 9;
A3:
the Charact of MU1 = Opers ((MSAlg U2),C)
by A2, MSUALG_2:def 9;
set gg1 = (*--> 0) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider gg1 = (*--> 0) * (signature U2) as Function of (dom (signature U2)),({0} *) by MSUALG_1:2;
A4:
MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #)
by MSUALG_1:10;
let B be non empty Subset of U2; ( B = the carrier of U1 implies the charact of U1 = Opers (U2,B) )
assume A5:
B = the carrier of U1
; the charact of U1 = Opers (U2,B)
then reconsider ch1 = the charact of U1 as PFuncFinSequence of B ;
A6:
MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #)
by MSUALG_1:def 11;
then A7: dom ch1 =
dom the Charact of MU1
by MSUALG_1:def 10
.=
the carrier' of (MSSign U2)
by PARTFUN1:def 2
.=
Seg (len (signature U2))
by A4, FINSEQ_1:def 3
.=
Seg (len the charact of U2)
by UNIALG_1:def 4
.=
dom the charact of U2
by FINSEQ_1:def 3
;
A8:
C is opers_closed
by A2, MSUALG_2:def 9;
for n being set
for o being operation of U2 st n in dom ch1 & o = the charact of U2 . n holds
ch1 . n = o /. B
proof
A9:
C = 0 .--> the
carrier of
U1
by A6, MSUALG_1:def 9;
then
dom C = {0}
;
then A10:
0 in dom C
by TARSKI:def 1;
let n be
set ;
for o being operation of U2 st n in dom ch1 & o = the charact of U2 . n holds
ch1 . n = o /. Blet o be
operation of
U2;
( n in dom ch1 & o = the charact of U2 . n implies ch1 . n = o /. B )
assume that A11:
n in dom ch1
and A12:
o = the
charact of
U2 . n
;
ch1 . n = o /. B
n in dom the
Charact of
(MSAlg U2)
by A1, A7, A11, MSUALG_1:def 10;
then reconsider N =
n as
OperSymbol of
(MSSign U2) by PARTFUN1:def 2;
A13:
(
dom the
charact of
U2 = Seg (len the charact of U2) &
dom (signature U2) = Seg (len (signature U2)) )
by FINSEQ_1:def 3;
then A14:
N in dom (signature U2)
by A7, A11, UNIALG_1:def 4;
(arity o) |-> 0 is
FinSequence of the
carrier of
(MSSign U2)
by A4, FINSEQ_2:63;
then reconsider ao0 =
(arity o) |-> 0 as
Element of the
carrier of
(MSSign U2) * by FINSEQ_1:def 11;
A15:
C is_closed_on N
by A8;
B is
opers_closed
by A2, A5, Th14;
then A16:
B is_closed_on o
;
A17:
0 in {0}
by TARSKI:def 1;
N in dom (signature U2)
by A7, A11, A13, UNIALG_1:def 4;
then
(
dom (*--> 0) = NAT &
(signature U2) . N = arity o )
by A12, FUNCT_2:def 1, UNIALG_1:def 4;
then A18:
N in dom ((*--> 0) * (signature U2))
by A14, FUNCT_1:11;
then ((C #) * the Arity of (MSSign U2)) . N =
(C #) . (((*--> 0) * (signature U2)) . N)
by A4, FUNCT_1:13
.=
(C #) . ((*--> 0) . ((signature U2) . N))
by A18, FUNCT_1:12
.=
(C #) . ((*--> 0) . (arity o))
by A12, A14, UNIALG_1:def 4
.=
(C #) . ((arity o) |-> 0)
by FINSEQ_2:def 6
;
then A19:
((C #) * the Arity of (MSSign U2)) . N =
product (C * ao0)
by FINSEQ_2:def 5
.=
product ((Seg (arity o)) --> (C . 0))
by A10, FUNCOP_1:17
.=
product ((Seg (arity o)) --> B)
by A5, A9, A17, FUNCOP_1:7
.=
Funcs (
(Seg (arity o)),
B)
by CARD_3:11
.=
(arity o) -tuples_on B
by FINSEQ_2:93
;
ch1 . N =
the
Charact of
MU1 . N
by A6, MSUALG_1:def 10
.=
N /. C
by A3, MSUALG_2:def 8
.=
(Den (N,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . N)
by A15, MSUALG_2:def 7
.=
((MSCharact U2) . N) | (((C #) * the Arity of (MSSign U2)) . N)
by A1, MSUALG_1:def 6
.=
o | ((arity o) -tuples_on B)
by A12, A19, MSUALG_1:def 10
;
hence
ch1 . n = o /. B
by A16, UNIALG_2:def 5;
verum
end;
hence
the charact of U1 = Opers (U2,B)
by A7, UNIALG_2:def 6; verum