let S be non empty non void ManySortedSign ; for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1
let U0 be MSAlgebra over S; for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1
let U1 be MSSubAlgebra of U0; Constants U0 is MSSubset of U1
Constants U0 c= the Sorts of U1
proof
let x be
object ;
PBOOLE:def 2 ( not x in the carrier of S or (Constants U0) . x c= the Sorts of U1 . x )
assume
x in the
carrier of
S
;
(Constants U0) . x c= the Sorts of U1 . x
then reconsider s =
x as
SortSymbol of
S ;
thus
(Constants U0) . x c= the
Sorts of
U1 . x
verumproof
let y be
object ;
TARSKI:def 3 ( not y in (Constants U0) . x or y in the Sorts of U1 . x )
per cases
( the Sorts of U0 . s = {} or the Sorts of U0 . s <> {} )
;
suppose
the
Sorts of
U0 . s <> {}
;
( not y in (Constants U0) . x or y in the Sorts of U1 . x )then A2:
ex
A being non
empty set st
(
A = the
Sorts of
U0 . s &
Constants (
U0,
s)
= { b where b is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } )
by Def3;
reconsider u1 = the
Sorts of
U1 as
MSSubset of
U0 by Def9;
assume A3:
y in (Constants U0) . x
;
y in the Sorts of U1 . x
(Constants U0) . x = Constants (
U0,
s)
by Def4;
then consider b being
Element of the
Sorts of
U0 . s such that A4:
b = y
and A5:
ex
o being
OperSymbol of
S st
( the
Arity of
S . o = {} & the
ResultSort of
S . o = s &
b in rng (Den (o,U0)) )
by A3, A2;
consider o being
OperSymbol of
S such that A6:
the
Arity of
S . o = {}
and A7:
the
ResultSort of
S . o = s
and A8:
b in rng (Den (o,U0))
by A5;
A9:
dom the
Arity of
S = the
carrier' of
S
by FUNCT_2:def 1;
then A10:
the
Arity of
S . o in rng the
Arity of
S
by FUNCT_1:def 3;
(
dom {} = {} &
rng {} = {} )
;
then reconsider a =
{} as
Function of
{},
{} by FUNCT_2:1;
A11:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
dom (u1 #) = the
carrier of
S *
by PARTFUN1:def 2;
then
o in dom ((u1 #) * the Arity of S)
by A9, A10, FUNCT_1:11;
then A12:
((u1 #) * the Arity of S) . o =
(u1 #) . ( the Arity of S . o)
by FUNCT_1:12
.=
(u1 #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product (u1 * (the_arity_of o))
by FINSEQ_2:def 5
.=
product (u1 * a)
by A6, MSUALG_1:def 1
.=
{{}}
by CARD_3:10
;
dom ( the Sorts of U0 #) = the
carrier of
S *
by PARTFUN1:def 2;
then A13:
o in dom (( the Sorts of U0 #) * the Arity of S)
by A9, A10, FUNCT_1:11;
u1 is
opers_closed
by Def9;
then
u1 is_closed_on o
;
then A14:
rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o
;
rng (Den (o,U0)) c= Result (
o,
U0)
by RELAT_1:def 19;
then dom (Den (o,U0)) =
Args (
o,
U0)
by A8, FUNCT_2:def 1
.=
(( the Sorts of U0 #) * the Arity of S) . o
by MSUALG_1:def 4
.=
( the Sorts of U0 #) . ( the Arity of S . o)
by A13, FUNCT_1:12
.=
( the Sorts of U0 #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ( the Sorts of U0 * (the_arity_of o))
by FINSEQ_2:def 5
.=
product ( the Sorts of U0 * a)
by A6, MSUALG_1:def 1
.=
{{}}
by CARD_3:10
;
then
(Den (o,U0)) | (((u1 #) * the Arity of S) . o) = Den (
o,
U0)
by A12;
then
b in (u1 * the ResultSort of S) . o
by A8, A14;
hence
y in the
Sorts of
U1 . x
by A4, A7, A11, FUNCT_1:13;
verum end;
end;
end;
hence
Constants U0 is MSSubset of U1
by PBOOLE:def 18; verum