set x = the set ;
set C = { the set };
consider a being Function such that
A1:
dom a = { the set }
and
A2:
rng a = {(<*> { the set })}
by FUNCT_1:5;
rng a c= { the set } *
then reconsider a = a as Function of { the set },({ the set } *) by A1, FUNCT_2:def 1, RELSET_1:4;
consider r being Function such that
A3:
dom r = { the set }
and
A4:
rng r = { the set }
by FUNCT_1:5;
reconsider r = r as Function of { the set },{ the set } by A3, A4, FUNCT_2:def 1, RELSET_1:4;
set M = ManySortedSign(# { the set },{ the set },a,r #);
take
ManySortedSign(# { the set },{ the set },a,r #)
; ( not ManySortedSign(# { the set },{ the set },a,r #) is void & ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op & ManySortedSign(# { the set },{ the set },a,r #) is strict )
thus
not ManySortedSign(# { the set },{ the set },a,r #) is void
; ( ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op & ManySortedSign(# { the set },{ the set },a,r #) is strict )
for s being SortSymbol of ManySortedSign(# { the set },{ the set },a,r #) holds s is with_const_op
proof
reconsider o = the
set as
OperSymbol of
ManySortedSign(#
{ the set },
{ the set },
a,
r #)
by TARSKI:def 1;
let s be
SortSymbol of
ManySortedSign(#
{ the set },
{ the set },
a,
r #);
s is with_const_op
take
o
;
MSUALG_2:def 1 ( the Arity of ManySortedSign(# { the set },{ the set },a,r #) . o = {} & the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s )
a . o in rng a
by A1, FUNCT_1:def 3;
hence
the
Arity of
ManySortedSign(#
{ the set },
{ the set },
a,
r #)
. o = {}
by A2, TARSKI:def 1;
the ResultSort of ManySortedSign(# { the set },{ the set },a,r #) . o = s
(
s = the
set &
r . o in rng r )
by A3, FUNCT_1:def 3, TARSKI:def 1;
hence
the
ResultSort of
ManySortedSign(#
{ the set },
{ the set },
a,
r #)
. o = s
by A4, TARSKI:def 1;
verum
end;
hence
ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op
; ManySortedSign(# { the set },{ the set },a,r #) is strict
thus
ManySortedSign(# { the set },{ the set },a,r #) is strict
; verum