let S be non empty ManySortedSign ; :: thesis: ( S is trivial implies for A being MSAlgebra over S
for c1, c2 being Component of the Sorts of A holds c1 = c2 )
assume A1: S is trivial ; :: thesis: for A being MSAlgebra over S
for c1, c2 being Component of the Sorts of A holds c1 = c2
let A be MSAlgebra over S; :: thesis: for c1, c2 being Component of the Sorts of A holds c1 = c2
let c1, c2 be Component of the Sorts of A; :: thesis: c1 = c2
( ex i1 being object st
( i1 in the carrier of S & c1 = the Sorts of A . i1 ) & ex i2 being object st
( i2 in the carrier of S & c2 = the Sorts of A . i2 ) ) by PBOOLE:138;
hence c1 = c2 by A1; :: thesis: verum