let MS be non void 1 -element segmental ManySortedSign ; for A being non-empty MSAlgebra over MS
for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
let A be non-empty MSAlgebra over MS; for B being non-empty MSSubAlgebra of A
for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
let B be non-empty MSSubAlgebra of A; for S being non empty Subset of (1-Alg A) st S = the carrier of (1-Alg B) holds
S is opers_closed
reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
A1:
C is opers_closed
by MSUALG_2:def 9;
A2:
1-Alg B = UAStr(# (the_sort_of B),(the_charact_of B) #)
by MSUALG_1:def 14;
let S be non empty Subset of (1-Alg A); ( S = the carrier of (1-Alg B) implies S is opers_closed )
assume A3:
S = the carrier of (1-Alg B)
; S is opers_closed
set 1A = 1-Alg A;
A4:
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #)
by MSUALG_1:def 14;
let o be operation of (1-Alg A); UNIALG_2:def 4 S is_closed_on o
A5:
dom the Sorts of A = the carrier of MS
by PARTFUN1:def 2;
then A6:
dom the Sorts of A = dom the Sorts of B
by PARTFUN1:def 2;
thus
S is_closed_on o
verumproof
reconsider com =
S as
Component of the
Sorts of
B by A2, A3, MSUALG_1:def 12;
consider n being
object such that A7:
n in dom the
charact of
(1-Alg A)
and A8:
o = the
charact of
(1-Alg A) . n
by FUNCT_1:def 3;
n in dom the
Charact of
A
by A4, A7, MSUALG_1:def 13;
then reconsider n =
n as
OperSymbol of
MS by PARTFUN1:def 2;
reconsider crn =
C . ( the ResultSort of MS . n) as
Component of the
Sorts of
B by A5, A6, FUNCT_1:def 3;
let s be
FinSequence of
S;
UNIALG_2:def 3 ( not len s = arity o or o . s in S )
A9:
dom the
Arity of
MS = the
carrier' of
MS
by FUNCT_2:def 1;
assume A10:
len s = arity o
;
o . s in S
ex
y being
set st
(
y in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) &
((Den (n,A)) | (((C #) * the Arity of MS) . n)) . y = o . s )
proof
take
s
;
( s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n)) & ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = o . s )
A11:
the
Charact of
A . n = the
charact of
(1-Alg A) . n
by A4, MSUALG_1:def 13;
thus
s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n))
((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s = o . sproof
rng s c= S
by FINSEQ_1:def 4;
then
rng s c= the
carrier of
(1-Alg A)
by XBOOLE_1:1;
then reconsider s1 =
s as
FinSequence of the
carrier of
(1-Alg A) by FINSEQ_1:def 4;
reconsider An = the
Arity of
MS . n as
Element of the
carrier of
MS * ;
set f = the
Sorts of
A * An;
consider d being
object such that A12:
d in dom o
by XBOOLE_0:def 1;
o in PFuncs (
( the carrier of (1-Alg A) *), the
carrier of
(1-Alg A))
by PARTFUN1:45;
then
ex
o1 being
Function st
(
o1 = o &
dom o1 c= the
carrier of
(1-Alg A) * &
rng o1 c= the
carrier of
(1-Alg A) )
by PARTFUN1:def 3;
then reconsider d =
d as
FinSequence of the
carrier of
(1-Alg A) by A12, FINSEQ_1:def 11;
A13:
dom (Den (n,A)) =
Args (
n,
A)
by FUNCT_2:def 1
.=
(len (the_arity_of n)) -tuples_on the
carrier of
(1-Alg A)
by A4, MSUALG_1:6
;
dom (Den (n,A)) = Args (
n,
A)
by FUNCT_2:def 1;
then dom (Den (n,A)) =
(( the Sorts of A #) * the Arity of MS) . n
by MSUALG_1:def 4
.=
( the Sorts of A #) . ( the Arity of MS . n)
by A9, FUNCT_1:13
;
then A14:
dom (Den (n,A)) = product ( the Sorts of A * An)
by FINSEQ_2:def 5;
A15:
o =
the
Charact of
A . n
by A4, A8, MSUALG_1:def 13
.=
Den (
n,
A)
by MSUALG_1:def 6
;
len d = len s1
by A10, A12, MARGREL1:def 25;
then
len s = len (the_arity_of n)
by A12, A15, A13, CARD_1:def 7;
then A16:
dom s =
Seg (len (the_arity_of n))
by FINSEQ_1:def 3
.=
dom (the_arity_of n)
by FINSEQ_1:def 3
.=
dom An
by MSUALG_1:def 1
;
A17:
dom s c= dom (C * An)
dom (C * An) c= dom s
by A16, RELAT_1:25;
then A19:
dom s = dom (C * An)
by A17;
A20:
for
x being
object st
x in dom s holds
s . x in (C * An) . x
A25:
dom ( the Sorts of A * An) c= dom s
by A16, FUNCT_1:11;
A26:
for
x being
object st
x in dom ( the Sorts of A * An) holds
s . x in ( the Sorts of A * An) . x
dom the
Arity of
MS = the
carrier' of
MS
by FUNCT_2:def 1;
then ((C #) * the Arity of MS) . n =
(C #) . An
by FUNCT_1:13
.=
product (C * An)
by FINSEQ_2:def 5
;
then A29:
s in ((C #) * the Arity of MS) . n
by A19, A20, CARD_3:9;
dom s c= dom ( the Sorts of A * An)
then
dom s = dom ( the Sorts of A * An)
by A25;
then
s in dom (Den (n,A))
by A14, A26, CARD_3:9;
then
s in (dom (Den (n,A))) /\ (((C #) * the Arity of MS) . n)
by A29, XBOOLE_0:def 4;
hence
s in dom ((Den (n,A)) | (((C #) * the Arity of MS) . n))
by RELAT_1:61;
verum
end;
hence ((Den (n,A)) | (((C #) * the Arity of MS) . n)) . s =
(Den (n,A)) . s
by FUNCT_1:47
.=
o . s
by A8, A11, MSUALG_1:def 6
;
verum
end;
then A31:
o . s in rng ((Den (n,A)) | (((C #) * the Arity of MS) . n))
by FUNCT_1:def 3;
dom the
ResultSort of
MS = the
carrier' of
MS
by FUNCT_2:def 1;
then A32:
(C * the ResultSort of MS) . n =
crn
by FUNCT_1:13
.=
com
by MSUALG_1:5
;
C is_closed_on n
by A1;
then
rng ((Den (n,A)) | (((C #) * the Arity of MS) . n)) c= (C * the ResultSort of MS) . n
;
hence
o . s in S
by A31, A32;
verum
end;