let S be non empty non void ManySortedSign ; for U0 being MSAlgebra of 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 of 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,sproof
let x be
set ;
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 4;
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
set st
(
x1 in dom (Den o1,U0) &
a = (Den o1,U0) . x1 )
by A8, FUNCT_1:def 5;
A10:
the_result_sort_of o1 = s
by A7, MSUALG_1:def 7;
A11:
the_arity_of o1 = {}
by A6, MSUALG_1:def 6;
then
Args o1,
U0 = {{} }
by PRALG_2:11;
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 set ; 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 10
.=
the Sorts of U0 . (the ResultSort of S . o)
by A15, FUNCT_1:23
.=
the Sorts of U0 . s
by A13, MSUALG_1:def 7
;
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:11;
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 5, MSUALG_1:def 6, MSUALG_1:def 7;
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 4;
x is
Element of
A
by A12, A14, A16, A18, Th6;
hence
x in Constants U0,
s
by A19, A17;
verum
end;