let U1, U2 be Universal_Algebra; :: thesis: ( 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;
assume A1:
MSAlg U1 is MSSubAlgebra of MSAlg U2
; :: thesis: 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 ;
A2:
MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #)
by MSUALG_1:def 16;
A3:
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #)
by MSUALG_1:def 16;
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;
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A1, MSUALG_2:def 10;
let B be non empty Subset of U2; :: thesis: ( B = the carrier of U1 implies the charact of U1 = Opers U2,B )
assume A5:
B = the carrier of U1
; :: thesis: the charact of U1 = Opers U2,B
A6:
( C is opers_closed & the Charact of MU1 = Opers (MSAlg U2),C )
by A1, MSUALG_2:def 10;
reconsider ch1 = the charact of U1 as PFuncFinSequence of B by A5;
A7: dom ch1 =
dom the Charact of MU1
by A2, 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
;
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
let n be
set ;
:: thesis: 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;
:: thesis: ( n in dom ch1 & o = the charact of U2 . n implies ch1 . n = o /. B )
assume A8:
(
n in dom ch1 &
o = the
charact of
U2 . n )
;
:: thesis: ch1 . n = o /. B
B is
opers_closed
by A1, A5, Th14;
then A9:
B is_closed_on o
by UNIALG_2:def 5;
n in dom the
Charact of
(MSAlg U2)
by A3, A7, A8, MSUALG_1:def 15;
then reconsider N =
n as
OperSymbol of
(MSSign U2) by PARTFUN1:def 4;
A10:
C is_closed_on N
by A6, MSUALG_2:def 7;
A11:
(
dom the
charact of
U2 = Seg (len the charact of U2) &
dom (signature U2) = Seg (len (signature U2)) )
by FINSEQ_1:def 3;
A13:
(
N in dom (signature U2) &
(signature U2) . N in dom (*--> 0 ) )
then A16:
N in dom ((*--> 0 ) * (signature U2))
by FUNCT_1:21;
then A17:
((C # ) * the Arity of (MSSign U2)) . N =
(C # ) . (((*--> 0 ) * (signature U2)) . N)
by A4, FUNCT_1:23
.=
(C # ) . ((*--> 0 ) . ((signature U2) . N))
by A16, FUNCT_1:22
.=
(C # ) . ((*--> 0 ) . (arity o))
by A8, A13, UNIALG_1:def 11
.=
(C # ) . ((arity o) |-> 0 )
by PBOOLE:def 20
;
(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;
A18:
C = 0 .--> the
carrier of
U1
by A2, MSUALG_1:def 14;
then
dom C = {0 }
by FUNCOP_1:19;
then A19:
0 in dom C
by TARSKI:def 1;
A20:
0 in {0 }
by TARSKI:def 1;
A21:
((C # ) * the Arity of (MSSign U2)) . N =
product (C * ao0)
by A17, PBOOLE:def 19
.=
product ((Seg (arity o)) --> (C . 0 ))
by A19, FUNCOP_1:23
.=
product ((Seg (arity o)) --> B)
by A5, A18, A20, 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 A2, MSUALG_1:def 15
.=
N /. C
by A6, MSUALG_2:def 9
.=
(Den N,(MSAlg U2)) | (((C # ) * the Arity of (MSSign U2)) . N)
by A10, MSUALG_2:def 8
.=
((MSCharact U2) . N) | (((C # ) * the Arity of (MSSign U2)) . N)
by A3, MSUALG_1:def 11
.=
o | ((arity o) -tuples_on B)
by A8, A21, MSUALG_1:def 15
;
hence
ch1 . n = o /. B
by A9, UNIALG_2:def 6;
:: thesis: verum
end;
hence
the charact of U1 = Opers U2,B
by A7, UNIALG_2:def 7; :: thesis: verum