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:90
.= I /\ a by PARTFUN1:def 4
.= a by XBOOLE_1:28 ;
then reconsider Cas = (Carrier A,s) | a as ManySortedSet of a by PARTFUN1:def 4;
for i being set st i in a holds
(Carrier Aa,s) . i = Cas . i

proof

let i be set ; :: 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 of S st
( U1 = A . i99 & (Carrier A,s) . i99 = the Sorts of U1 . s ) ) by A1, FUNCT_1:72, PRALG_2:def 16;
ex U0 being MSAlgebra of S st
( U0 = Aa . i & (Carrier Aa,s) . i = the Sorts of U0 . s ) by A2, PRALG_2:def 16;
hence (Carrier Aa,s) . i = Cas . i by A3, FUNCT_1:72; :: thesis: verum

end;

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