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 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 i' = i as Element of a ;
reconsider i'' = i' as Element of I ;
A3: Aa . i' = A . i' by A1, FUNCT_1:72;
consider U0 being MSAlgebra of S such that
A4: ( U0 = Aa . i & (Carrier Aa,s) . i = the Sorts of U0 . s ) by A2, PRALG_2:def 16;
consider U1 being MSAlgebra of S such that
A5: ( U1 = A . i'' & (Carrier A,s) . i'' = the Sorts of U1 . s ) by PRALG_2:def 16;
thus (Carrier Aa,s) . i = Cas . i by A3, A4, A5, FUNCT_1:72; :: thesis: verum

end;

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