let A be Universal_Algebra; :: thesis: for f being Function of (dom (signature A)),({0} *) holds
( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
let f be Function of (dom (signature A)),({0} *); :: thesis: ( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
set S = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #);
A1: ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental
proof
take len (signature A) ; :: according to MSUALG_1:def 7 :: thesis: the carrier' of ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) = Seg (len (signature A))
thus the carrier' of ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) = Seg (len (signature A)) by FINSEQ_1:def 3; :: thesis: verum
end;
signature A <> {} by Th4;
hence ( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict ) by A1; :: thesis: verum