consider f being object 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 object st x in dom B holds
g . x in B . x ) ) by A1, CARD_3:def 5;
dom B = I by PARTFUN1:def 2;
then reconsider f = f as ManySortedSet of I by A2, PARTFUN1:def 2, 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 object 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 object st x in dom B holds
(f +* ((indx B),y)) . x in B . x
proof
let x be object ; :: 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 2;
then A7: x in dom f by PARTFUN1:def 2;
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:31; :: 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:32;
hence (f +* ((indx B),y)) . x in B . x by A2, A6; :: thesis: verum
end;
end;
end;
dom f = I by PARTFUN1:def 2;
then A8: (f +* ((indx B),y)) . (indx B) = y by FUNCT_7:31;
dom (f +* ((indx B),y)) = I by PARTFUN1:def 2
.= dom B by PARTFUN1:def 2 ;
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