let A be Universal_Algebra; :: thesis: for f being Function of (dom (signature A)),({0 } * ) holds
( not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is empty & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & 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: ( not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is empty & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & 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) #);
thus not the carrier of ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is empty ; :: according to STRUCT_0:def 1 :: thesis: ( ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & 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 )
A1: ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental

proof

take len (signature A) ; :: according to MSUALG_1:def 12 :: 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 Th9;
hence ( ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & 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