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