let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 <> {}
; :: thesis: 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 = {} ) }
:: according to XBOOLE_0:def 10 :: thesis: { (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 ;
:: according to TARSKI:def 3 :: thesis: ( 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
;
:: thesis: 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;
consider x1 being
set such that A9:
x1 in dom (Den o1,U0)
and A10:
a = (Den o1,U0) . x1
by A8, FUNCT_1:def 5;
A11:
the_result_sort_of o1 = s
by A7, MSUALG_1:def 7;
A12:
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, A10, 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 A11, A12;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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 = {} ) }
; :: thesis: x in Constants U0,s
then consider o being Element of the carrier' of S such that
A13:
x = const o,U0
and
A14:
the_result_sort_of o = s
and
A15:
the_arity_of o = {}
;
o in the carrier' of S
;
then A16:
o in dom the ResultSort of S
by FUNCT_2:def 1;
A17: 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 A16, FUNCT_1:23
.=
the Sorts of U0 . s
by A14, MSUALG_1:def 7
;
thus
x in Constants U0,s
:: thesis: verumproof
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;
A20:
x is
Element of
A
by A13, A15, A17, A18, Th6;
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
;
:: thesis: ( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den o,U0) )
A21:
Args o,
U0 = dom (Den o,U0)
by A1, A17, FUNCT_2:def 1;
Args o,
U0 = {{} }
by A15, PRALG_2:11;
then
{} in dom (Den o,U0)
by A21, TARSKI:def 1;
hence
( the
Arity of
S . o = {} & the
ResultSort of
S . o = s &
x in rng (Den o,U0) )
by A13, A14, A15, FUNCT_1:def 5, MSUALG_1:def 6, MSUALG_1:def 7;
:: thesis: verum
end;
hence
x in Constants U0,
s
by A19, A20;
:: thesis: verum
end;