theorem Th2: :: PRALG_3:2

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a