let S be non empty non void ManySortedSign ; for U0 being MSAlgebra over S
for s being SortSymbol of S st the Sorts of U0 . s <> {} holds
Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
let U0 be MSAlgebra over S; for s being SortSymbol of S st the Sorts of U0 . s <> {} holds
Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
let s be SortSymbol of S; ( the Sorts of U0 . s <> {} implies Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } )
assume A1:
the Sorts of U0 . s <> {}
; Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
thus
Constants (U0,s) c= { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
XBOOLE_0:def 10 { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } c= Constants (U0,s)proof
let x be
object ;
TARSKI:def 3 ( not x in Constants (U0,s) or x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } )
assume A2:
x in Constants (
U0,
s)
;
x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
ex
A being non
empty set st
(
A = the
Sorts of
U0 . s &
Constants (
U0,
s)
= { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } )
by A1, MSUALG_2:def 3;
then consider A being non
empty set such that
A = the
Sorts of
U0 . s
and A3:
x in { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) }
by A2;
consider a being
Element of
A such that A4:
a = x
and A5:
ex
o being
OperSymbol of
S st
( the
Arity of
S . o = {} & the
ResultSort of
S . o = s &
a in rng (Den (o,U0)) )
by A3;
consider o1 being
OperSymbol of
S such that A6:
the
Arity of
S . o1 = {}
and A7:
the
ResultSort of
S . o1 = s
and A8:
a in rng (Den (o1,U0))
by A5;
A9:
ex
x1 being
object st
(
x1 in dom (Den (o1,U0)) &
a = (Den (o1,U0)) . x1 )
by A8, FUNCT_1:def 3;
A10:
the_result_sort_of o1 = s
by A7, MSUALG_1:def 2;
A11:
the_arity_of o1 = {}
by A6, MSUALG_1:def 1;
then
Args (
o1,
U0)
= {{}}
by PRALG_2:4;
then
x = const (
o1,
U0)
by A4, A9, TARSKI:def 1;
hence
x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
by A10, A11;
verum
end;
let x be object ; TARSKI:def 3 ( not x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } or x in Constants (U0,s) )
assume
x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
; x in Constants (U0,s)
then consider o being Element of the carrier' of S such that
A12:
x = const (o,U0)
and
A13:
the_result_sort_of o = s
and
A14:
the_arity_of o = {}
;
o in the carrier' of S
;
then A15:
o in dom the ResultSort of S
by FUNCT_2:def 1;
A16: Result (o,U0) =
( the Sorts of U0 * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the Sorts of U0 . ( the ResultSort of S . o)
by A15, FUNCT_1:13
.=
the Sorts of U0 . s
by A13, MSUALG_1:def 2
;
thus
x in Constants (U0,s)
verumproof
A17:
ex
o being
OperSymbol of
S st
( the
Arity of
S . o = {} & the
ResultSort of
S . o = s &
x in rng (Den (o,U0)) )
proof
take
o
;
( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den (o,U0)) )
(
Args (
o,
U0)
= dom (Den (o,U0)) &
Args (
o,
U0)
= {{}} )
by A1, A14, A16, FUNCT_2:def 1, PRALG_2:4;
then
{} in dom (Den (o,U0))
by TARSKI:def 1;
hence
( the
Arity of
S . o = {} & the
ResultSort of
S . o = s &
x in rng (Den (o,U0)) )
by A12, A13, A14, FUNCT_1:def 3, MSUALG_1:def 1, MSUALG_1:def 2;
verum
end;
consider A being non
empty set such that A18:
A = the
Sorts of
U0 . s
and A19:
Constants (
U0,
s)
= { a where a is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) }
by A1, MSUALG_2:def 3;
x is
Element of
A
by A12, A14, A16, A18, Th5;
hence
x in Constants (
U0,
s)
by A19, A17;
verum
end;