let I be set ; :: thesis:
let C be Subset of I; :: thesis:
let M be ManySortedSet of I; :: thesis:
dom (M #) = I * by PARTFUN1:def 2;
then dom ((M #) | (C *)) = C * by Th2, RELAT_1:62;
then reconsider D = (M #) | (C *) as ManySortedSet of C * by PARTFUN1:def 2;
A1: C * c= I * by Th2;
for i being Element of C * holds ((M #) | (C *)) . i = product ((M | C) * i)

let i be Element of C * ; :: thesis:
A2: rng i c= C ;
i in C * ;
then A3: i in dom D by PARTFUN1:def 2;
A4: i in I * by A1;
for a being object holds
( a in D . i iff ex g being Function st
( a = g & dom g = dom ((M | C) * i) & ( for a being object st a in dom ((M | C) * i) holds
g . a in ((M | C) * i) . a ) ) )

let a be object ; :: thesis:

assume a in D . i ; :: thesis:
then a in (M #) . i by A3, FUNCT_1:47;
then a in product (M * i) by A4, FINSEQ_2:def 5;
then consider g being Function such that
A5: a = g and
A6: dom g = dom (M * i) and
A7: for x being object st x in dom (M * i) holds
g . x in (M * i) . x by CARD_3:def 5;
take g = g; :: thesis:
thus a = g by A5; :: thesis:
rng i c= C ;
hence dom g = dom ((M | C) * i) by A6, Th1; :: thesis:
thus for a being object st a in dom ((M | C) * i) holds
g . a in ((M | C) * i) . a :: thesis:

A8: rng i c= C ;
let a be object ; :: thesis:
assume a in dom ((M | C) * i) ; :: thesis:
then a in dom (M * i) by A8, Th1;
then g . a in (M * i) . a by A7;
hence g . a in ((M | C) * i) . a by A8, Th1; :: thesis:

end;

given g being Function such that A9: a = g and
A10: dom g = dom ((M | C) * i) and
A11: for a being object st a in dom ((M | C) * i) holds
g . a in ((M | C) * i) . a ; :: thesis:
A12: for a being object st a in dom (M * i) holds
g . a in (M * i) . a

let a be object ; :: thesis:
assume a in dom (M * i) ; :: thesis:
then a in dom ((M | C) * i) by A2, Th1;
then g . a in ((M | C) * i) . a by A11;
hence g . a in (M * i) . a by A2, Th1; :: thesis:

end;

end;

hence ((M #) | (C *)) . i = product ((M | C) * i) by CARD_3:def 5; :: thesis:

end;

hence (M | C) # = D by FINSEQ_2:def 5
.= (M #) | (C *) ;
:: thesis: