let A be non empty set ; :: thesis: for S being non empty non void ManySortedSign

for C being category st C = MSAlgCat (S,A) holds

for o being Object of C holds o is strict feasible MSAlgebra over S

let S be non empty non void ManySortedSign ; :: thesis: for C being category st C = MSAlgCat (S,A) holds

for o being Object of C holds o is strict feasible MSAlgebra over S

let C be category; :: thesis: ( C = MSAlgCat (S,A) implies for o being Object of C holds o is strict feasible MSAlgebra over S )

assume A1: C = MSAlgCat (S,A) ; :: thesis: for o being Object of C holds o is strict feasible MSAlgebra over S

let o be Object of C; :: thesis: o is strict feasible MSAlgebra over S

o in the carrier of C ;

then o in MSAlg_set (S,A) by A1, Def4;

then ex M being strict feasible MSAlgebra over S st

( o = M & ( for C1 being Component of the Sorts of M holds C1 c= A ) ) by Def2;

hence o is strict feasible MSAlgebra over S ; :: thesis: verum

for C being category st C = MSAlgCat (S,A) holds

for o being Object of C holds o is strict feasible MSAlgebra over S

let S be non empty non void ManySortedSign ; :: thesis: for C being category st C = MSAlgCat (S,A) holds

for o being Object of C holds o is strict feasible MSAlgebra over S

let C be category; :: thesis: ( C = MSAlgCat (S,A) implies for o being Object of C holds o is strict feasible MSAlgebra over S )

assume A1: C = MSAlgCat (S,A) ; :: thesis: for o being Object of C holds o is strict feasible MSAlgebra over S

let o be Object of C; :: thesis: o is strict feasible MSAlgebra over S

o in the carrier of C ;

then o in MSAlg_set (S,A) by A1, Def4;

then ex M being strict feasible MSAlgebra over S st

( o = M & ( for C1 being Component of the Sorts of M holds C1 c= A ) ) by Def2;

hence o is strict feasible MSAlgebra over S ; :: thesis: verum