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 16;
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 of MSSign U2 ;
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A2, MSUALG_2:def 10;
A3:
the Charact of MU1 = Opers (MSAlg U2),C
by A2, MSUALG_2:def 10;
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:7;
A4:
MSSign U2 = ManySortedSign(# {0 },(dom (signature U2)),gg1,((dom (signature U2)) --> z) #)
by MSUALG_1:16;
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 16;
then A7: dom ch1 =
dom the Charact of MU1
by MSUALG_1:def 15
.=
the carrier' of (MSSign U2)
by PARTFUN1:def 4
.=
Seg (len (signature U2))
by A4, FINSEQ_1:def 3
.=
Seg (len the charact of U2)
by UNIALG_1:def 11
.=
dom the charact of U2
by FINSEQ_1:def 3
;
A8:
C is opers_closed
by A2, MSUALG_2:def 10;
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 14;
then
dom C = {0 }
by FUNCOP_1:19;
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 15;
then reconsider N =
n as
OperSymbol of
(MSSign U2) by PARTFUN1:def 4;
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 11;
(arity o) |-> 0 is
FinSequence of the
carrier of
(MSSign U2)
by A4, FINSEQ_2:77;
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, MSUALG_2:def 7;
B is
opers_closed
by A2, A5, Th14;
then A16:
B is_closed_on o
by UNIALG_2:def 5;
A17:
0 in {0 }
by TARSKI:def 1;
N in dom (signature U2)
by A7, A11, A13, UNIALG_1:def 11;
then
(
dom (*--> 0 ) = NAT &
(signature U2) . N = arity o )
by A12, FUNCT_2:def 1, UNIALG_1:def 11;
then A18:
N in dom ((*--> 0 ) * (signature U2))
by A14, FUNCT_1:21;
then ((C # ) * the Arity of (MSSign U2)) . N =
(C # ) . (((*--> 0 ) * (signature U2)) . N)
by A4, FUNCT_1:23
.=
(C # ) . ((*--> 0 ) . ((signature U2) . N))
by A18, FUNCT_1:22
.=
(C # ) . ((*--> 0 ) . (arity o))
by A12, A14, UNIALG_1:def 11
.=
(C # ) . ((arity o) |-> 0 )
by PBOOLE:def 20
;
then A19:
((C # ) * the Arity of (MSSign U2)) . N =
product (C * ao0)
by PBOOLE:def 19
.=
product ((Seg (arity o)) --> (C . 0 ))
by A10, FUNCOP_1:23
.=
product ((Seg (arity o)) --> B)
by A5, A9, A17, FUNCOP_1:13
.=
Funcs (Seg (arity o)),
B
by CARD_3:20
.=
(arity o) -tuples_on B
by FINSEQ_2:111
;
ch1 . N =
the
Charact of
MU1 . N
by A6, MSUALG_1:def 15
.=
N /. C
by A3, MSUALG_2:def 9
.=
(Den N,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . N)
by A15, MSUALG_2:def 8
.=
((MSCharact U2) . N) | (((C # ) * the Arity of (MSSign U2)) . N)
by A1, MSUALG_1:def 11
.=
o | ((arity o) -tuples_on B)
by A12, A19, MSUALG_1:def 15
;
hence
ch1 . n = o /. B
by A16, UNIALG_2:def 6;
verum
end;
hence
the charact of U1 = Opers U2,B
by A7, UNIALG_2:def 7; verum