let A be non empty set ; :: thesis: for C being category st C = MSSCat A holds
for o being Object of C holds o is non empty non void ManySortedSign
let C be category; :: thesis: ( C = MSSCat A implies for o being Object of C holds o is non empty non void ManySortedSign )
assume A1: C = MSSCat A ; :: thesis: for o being Object of C holds o is non empty non void ManySortedSign
let o be Object of C; :: thesis: o is non empty non void ManySortedSign
reconsider o = o as Element of MSS_set A by A1, Def1;
o is non empty non void ManySortedSign ;
hence o is non empty non void ManySortedSign ; :: thesis: verum