consider f being set such that
A1: f in product B by XBOOLE_0:def 1;
A2: ex g being Function st
( g = f & dom g = dom B & ( for x being set st x in dom B holds
g . x in B . x ) ) by A1, CARD_3:def 5;
dom B = I by PARTFUN1:def 4;
then reconsider f = f as ManySortedSet of I by A2, PARTFUN1:def 4, RELAT_1:def 18;
not B . (indx B) is trivial by Def21;
then 2 c= card (B . (indx B)) by Th4;
then consider y being set such that
A3: y in B . (indx B) and
A4: y <> f . (indx B) by Th3;
set l = f +* (indx B),y;
A5: for x being set st x in dom B holds
(f +* (indx B),y) . x in B . x

proof

let x be set ; :: thesis: ( x in dom B implies (f +* (indx B),y) . x in B . x )
assume A6: x in dom B ; :: thesis: (f +* (indx B),y) . x in B . x
then x in I by PARTFUN1:def 4;
then A7: x in dom f by PARTFUN1:def 4;

per cases ( x = indx B or x <> indx B ) ;

suppose x = indx B ; :: thesis: (f +* (indx B),y) . x in B . x

hence (f +* (indx B),y) . x in B . x by A3, A7, FUNCT_7:33; :: thesis: verum

end;

suppose x <> indx B ; :: thesis: (f +* (indx B),y) . x in B . x

then (f +* (indx B),y) . x = f . x by FUNCT_7:34;
hence (f +* (indx B),y) . x in B . x by A2, A6; :: thesis: verum

end;

end;

end;

dom f = I by PARTFUN1:def 4;
then A8: (f +* (indx B),y) . (indx B) = y by FUNCT_7:33;
dom (f +* (indx B),y) = I by PARTFUN1:def 4
.= dom B by PARTFUN1:def 4 ;
then f +* (indx B),y in product B by A5, CARD_3:def 5;
then 2 c= card (product B) by A1, A4, A8, Th2;
hence not product B is trivial by Th4; :: thesis: verum