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

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