let I be non empty set ; :: thesis: 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
let S be non empty non void ManySortedSign ; :: thesis: 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
let A be MSAlgebra-Family of I,S; :: thesis: 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
let s be SortSymbol of S; :: thesis: 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
let a be non empty Subset of I; :: thesis: for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
let Aa be MSAlgebra-Family of a,S; :: thesis: ( A | a = Aa implies Carrier (Aa,s) = (Carrier (A,s)) | a )
assume A1: A | a = Aa ; :: thesis: Carrier (Aa,s) = (Carrier (A,s)) | a
dom ((Carrier (A,s)) | a) = (dom (Carrier (A,s))) /\ a by RELAT_1:61
.= I /\ a by PARTFUN1:def 2
.= a by XBOOLE_1:28 ;
then reconsider Cas = (Carrier (A,s)) | a as ManySortedSet of a by PARTFUN1:def 2;
for i being object st i in a holds
(Carrier (Aa,s)) . i = Cas . i

proof

let i be object ; :: thesis: ( i in a implies (Carrier (Aa,s)) . i = Cas . i )
assume A2: i in a ; :: thesis: (Carrier (Aa,s)) . i = Cas . i
then reconsider i9 = i as Element of a ;
reconsider i99 = i9 as Element of I ;
A3: ( Aa . i9 = A . i9 & ex U1 being MSAlgebra over S st
( U1 = A . i99 & (Carrier (A,s)) . i99 = the Sorts of U1 . s ) ) by A1, FUNCT_1:49, PRALG_2:def 9;
ex U0 being MSAlgebra over S st
( U0 = Aa . i & (Carrier (Aa,s)) . i = the Sorts of U0 . s ) by A2, PRALG_2:def 9;
hence (Carrier (Aa,s)) . i = Cas . i by A3, FUNCT_1:49; :: thesis: verum

end;

hence Carrier (Aa,s) = (Carrier (A,s)) | a by PBOOLE:3; :: thesis: verum