let I be set ; :: thesis: for C being Subset of I
for M being ManySortedSet of I holds (M | C) # = (M #) | (C *)
let C be Subset of I; :: thesis: for M being ManySortedSet of I holds (M | C) # = (M #) | (C *)
let M be ManySortedSet of I; :: thesis: (M | C) # = (M #) | (C *)
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)

proof

let i be Element of C * ; :: thesis: ((M #) | (C *)) . i = product ((M | C) * i)
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 ) ) )

proof

let a be object ; :: thesis: ( 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 ) ) )

hereby :: thesis: ( 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 ) ) implies a in D . i )

assume a in D . i ; :: thesis: 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 ) )
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: ( 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 ) )
thus a = g by A5; :: thesis: ( 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 ) )
rng i c= C ;
hence dom g = dom ((M | C) * i) by A6, Th1; :: thesis: for a being object st a in dom ((M | C) * i) holds
g . a in ((M | C) * i) . a
thus for a being object st a in dom ((M | C) * i) holds
g . a in ((M | C) * i) . a :: thesis: verum

proof

A8: rng i c= C ;
let a be object ; :: thesis: ( a in dom ((M | C) * i) implies g . a in ((M | C) * i) . a )
assume a in dom ((M | C) * i) ; :: thesis: g . a in ((M | C) * i) . a
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: verum

end;

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: a in D . i
A12: for a being object st a in dom (M * i) holds
g . a in (M * i) . a

proof

let a be object ; :: thesis: ( a in dom (M * i) implies g . a in (M * i) . a )
assume a in dom (M * i) ; :: thesis: g . a in (M * i) . a
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: verum

end;

dom g = dom (M * i) by A2, A10, Th1;
then a in product (M * i) by A9, A12, CARD_3:def 5;
then a in (M #) . i by A4, FINSEQ_2:def 5;
hence a in D . i by A3, FUNCT_1:47; :: thesis: verum

end;

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

end;

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