consider x being set ;
set C = {x};
consider a being Function such that
A1: dom a = {x} and
A2: rng a = {(<*> {x})} by FUNCT_1:15;
rng a c= {x} *

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng a or y in {x} * )
assume y in rng a ; :: thesis: y in {x} *
then y = <*> {x} by A2, TARSKI:def 1;
hence y in {x} * by FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider a = a as Function of {x},({x} * ) by A1, FUNCT_2:def 1, RELSET_1:11;
consider r being Function such that
A3: dom r = {x} and
A4: rng r = {x} by FUNCT_1:15;
reconsider r = r as Function of {x},{x} by A3, A4, FUNCT_2:def 1, RELSET_1:11;
set M = ManySortedSign(# {x},{x},a,r #);
take ManySortedSign(# {x},{x},a,r #) ; :: thesis: ( not ManySortedSign(# {x},{x},a,r #) is void & ManySortedSign(# {x},{x},a,r #) is all-with_const_op & ManySortedSign(# {x},{x},a,r #) is strict )
thus not ManySortedSign(# {x},{x},a,r #) is void ; :: thesis: ( ManySortedSign(# {x},{x},a,r #) is all-with_const_op & ManySortedSign(# {x},{x},a,r #) is strict )
for s being SortSymbol of ManySortedSign(# {x},{x},a,r #) holds s is with_const_op

proof

reconsider o = x as OperSymbol of ManySortedSign(# {x},{x},a,r #) by TARSKI:def 1;
let s be SortSymbol of ManySortedSign(# {x},{x},a,r #); :: thesis: s is with_const_op
take o ; :: according to MSUALG_2:def 2 :: thesis: ( the Arity of ManySortedSign(# {x},{x},a,r #) . o = {} & the ResultSort of ManySortedSign(# {x},{x},a,r #) . o = s )
a . o in rng a by A1, FUNCT_1:def 5;
hence the Arity of ManySortedSign(# {x},{x},a,r #) . o = {} by A2, TARSKI:def 1; :: thesis: the ResultSort of ManySortedSign(# {x},{x},a,r #) . o = s
( s = x & r . o in rng r ) by A3, FUNCT_1:def 5, TARSKI:def 1;
hence the ResultSort of ManySortedSign(# {x},{x},a,r #) . o = s by A4, TARSKI:def 1; :: thesis: verum

end;

hence ManySortedSign(# {x},{x},a,r #) is all-with_const_op by Def3; :: thesis: ManySortedSign(# {x},{x},a,r #) is strict
thus ManySortedSign(# {x},{x},a,r #) is strict ; :: thesis: verum