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 } *
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng a or y in { the set } * )
assume y in rng a ; :: thesis: y in { the set } *
then y = <*> { the set } by A2, TARSKI:def 1;
hence y in { the set } * by FINSEQ_1:def 11; :: thesis: verum
end;
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 #) ; :: thesis: ( 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 ; :: thesis: ( 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 #); :: thesis: s is with_const_op
take o ; :: according to MSUALG_2:def 1 :: thesis: ( 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; :: thesis: 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; :: thesis: verum
end;
hence ManySortedSign(# { the set },{ the set },a,r #) is all-with_const_op ; :: thesis: ManySortedSign(# { the set },{ the set },a,r #) is strict
thus ManySortedSign(# { the set },{ the set },a,r #) is strict ; :: thesis: verum