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
B is opers_closed )
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
B is opers_closed
then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ;
let B be non empty Subset of U2; ( B = the carrier of U1 implies B is opers_closed )
assume A3:
B = the carrier of U1
; B is opers_closed
let o be operation of U2; UNIALG_2:def 4 B is_closed_on o
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A2, MSUALG_2:def 9;
A4:
MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #)
by MSUALG_1:def 11;
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;
A5:
MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #)
by MSUALG_1:10;
A6:
C is opers_closed
by A2, MSUALG_2:def 9;
thus
B is_closed_on o
verumproof
A7:
0 in {0}
by TARSKI:def 1;
let s be
FinSequence of
B;
UNIALG_2:def 3 ( not len s = arity o or o . s in B )
consider n being
object such that A8:
n in dom the
charact of
U2
and A9:
o = the
charact of
U2 . n
by FUNCT_1:def 3;
A10:
(
dom the
charact of
U2 = Seg (len the charact of U2) &
dom (signature U2) = Seg (len (signature U2)) )
by FINSEQ_1:def 3;
then A11:
n in dom (signature U2)
by A8, UNIALG_1:def 4;
reconsider n =
n as
OperSymbol of
(MSSign U2) by A5, A8, A10, UNIALG_1:def 4;
assume A12:
len s = arity o
;
o . s in B
ex
y being
set st
(
y in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) &
((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . y = o . s )
proof
take
s
;
( s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) & ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = o . s )
thus
s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n))
((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s = o . sproof
(arity o) |-> 0 is
FinSequence of the
carrier of
(MSSign U2)
by A5, FINSEQ_2:63;
then reconsider ao0 =
(arity o) |-> 0 as
Element of the
carrier of
(MSSign U2) * by FINSEQ_1:def 11;
(
Seg (arity o) <> {} implies (
dom ((arity o) |-> 0) = Seg (arity o) &
rng ((arity o) |-> 0) c= the
carrier of
(MSSign U2) ) )
by A5, FUNCOP_1:13;
then
(arity o) |-> 0 is
FinSequence of the
carrier of
(MSSign U2)
by A13, FINSEQ_1:def 4;
then reconsider aro =
(arity o) |-> 0 as
Element of the
carrier of
(MSSign U2) * by FINSEQ_1:def 11;
A14:
dom the
Arity of
(MSSign U2) = the
carrier' of
(MSSign U2)
by FUNCT_2:def 1;
the
Sorts of
(MSAlg U2) = 0 .--> the
carrier of
U2
by A1, MSUALG_1:def 9;
then A15: the
Sorts of
(MSAlg U2) * aro =
(arity o) |-> the
carrier of
U2
by FINSEQ_2:144
.=
(Seg (arity o)) --> the
carrier of
U2
;
dom s = Seg (arity o)
by A12, FINSEQ_1:def 3;
then A16:
dom s = dom ( the Sorts of (MSAlg U2) * aro)
by A15;
A17:
for
x being
object st
x in dom ( the Sorts of (MSAlg U2) * aro) holds
s . x in ( the Sorts of (MSAlg U2) * aro) . x
dom (Den (n,(MSAlg U2))) = Args (
n,
(MSAlg U2))
by FUNCT_2:def 1;
then dom (Den (n,(MSAlg U2))) =
(( the Sorts of (MSAlg U2) #) * the Arity of (MSSign U2)) . n
by MSUALG_1:def 4
.=
( the Sorts of (MSAlg U2) #) . (((*--> 0) * (signature U2)) . n)
by A5, A14, FUNCT_1:13
.=
( the Sorts of (MSAlg U2) #) . ((*--> 0) . ((signature U2) . n))
by A11, FUNCT_1:13
.=
( the Sorts of (MSAlg U2) #) . ((*--> 0) . (arity o))
by A9, A11, UNIALG_1:def 4
.=
( the Sorts of (MSAlg U2) #) . ((arity o) |-> 0)
by FINSEQ_2:def 6
;
then
dom (Den (n,(MSAlg U2))) = product ( the Sorts of (MSAlg U2) * aro)
by FINSEQ_2:def 5;
then A21:
s in dom (Den (n,(MSAlg U2)))
by A16, A17, CARD_3:def 5;
A22:
s is
Element of
(len s) -tuples_on B
by FINSEQ_2:92;
A23:
0 in {0}
by TARSKI:def 1;
A24:
n in dom (signature U2)
by A8, A10, UNIALG_1:def 4;
A25:
C = 0 .--> the
carrier of
U1
by A4, MSUALG_1:def 9;
then
dom C = {0}
;
then A26:
0 in dom C
by TARSKI:def 1;
(
dom (*--> 0) = NAT &
(signature U2) . n = arity o )
by A9, A11, FUNCT_2:def 1, UNIALG_1:def 4;
then A27:
n in dom ((*--> 0) * (signature U2))
by A24, FUNCT_1:11;
then ((C #) * the Arity of (MSSign U2)) . n =
(C #) . (((*--> 0) * (signature U2)) . n)
by A5, FUNCT_1:13
.=
(C #) . ((*--> 0) . ((signature U2) . n))
by A27, FUNCT_1:12
.=
(C #) . ((*--> 0) . (arity o))
by A9, A24, UNIALG_1:def 4
.=
(C #) . ((arity o) |-> 0)
by FINSEQ_2:def 6
;
then ((C #) * the Arity of (MSSign U2)) . n =
product (C * ao0)
by FINSEQ_2:def 5
.=
product ((Seg (arity o)) --> (C . 0))
by A26, FUNCOP_1:17
.=
product ((Seg (arity o)) --> B)
by A3, A25, A23, FUNCOP_1:7
.=
Funcs (
(Seg (arity o)),
B)
by CARD_3:11
.=
(arity o) -tuples_on B
by FINSEQ_2:93
;
then
s in (dom (Den (n,(MSAlg U2)))) /\ (((C #) * the Arity of (MSSign U2)) . n)
by A12, A21, A22, XBOOLE_0:def 4;
hence
s in dom ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n))
by RELAT_1:61;
verum
end;
hence ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) . s =
(Den (n,(MSAlg U2))) . s
by FUNCT_1:47
.=
((MSCharact U2) . n) . s
by A1, MSUALG_1:def 6
.=
o . s
by A9, MSUALG_1:def 10
;
verum
end;
then A28:
o . s in rng ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n))
by FUNCT_1:def 3;
C is_closed_on n
by A6;
then A29:
rng ((Den (n,(MSAlg U2))) | (((C #) * the Arity of (MSSign U2)) . n)) c= (C * the ResultSort of (MSSign U2)) . n
;
n in dom ((dom (signature U2)) --> 0)
by A11;
then (C * the ResultSort of (MSSign U2)) . n =
C . (((dom (signature U2)) --> 0) . n)
by A5, FUNCT_1:13
.=
the
Sorts of
MU1 . 0
.=
(0 .--> the carrier of U1) . 0
by A4, MSUALG_1:def 9
.=
B
by A3, A7, FUNCOP_1:7
;
hence
o . s in B
by A29, A28;
verum
end;