let S be non empty ManySortedSign ; :: thesis: ( S is trivial implies for A being MSAlgebra of S
for c1, c2 being Component of the Sorts of A holds c1 = c2 )
assume A1: S is trivial ; :: thesis: for A being MSAlgebra of S
for c1, c2 being Component of the Sorts of A holds c1 = c2
let A be MSAlgebra of 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
consider i1 being set such that
A2: i1 in the carrier of S and
A3: c1 = the Sorts of A . i1 by PBOOLE:150;
consider i2 being set such that
A4: i2 in the carrier of S and
A5: c2 = the Sorts of A . i2 by PBOOLE:150;
thus c1 = c2 by A1, A2, A3, A4, A5, STRUCT_0:def 10; :: thesis: verum