set B = the Element of Carrier A;
set i1 = the Element of I;
A1: ex R being 1-sorted st
( R = A . the Element of I & the carrier of R = (Carrier A) . the Element of I ) by PRALG_1:def 15;
then reconsider b1 = the Element of Carrier A . the Element of I as Element of (A . the Element of I) by PBOOLE:def 14;
reconsider B = the Element of Carrier A as ManySortedSet of I ;
dom A = I by PARTFUN1:def 2;
then A . the Element of I in rng A by FUNCT_1:def 3;
then not A . the Element of I is trivial by Def17;
then reconsider Ai1 = the carrier of (A . the Element of I) as non trivial set ;
ex x1, x2 being Element of Ai1 st x1 <> x2 by SUBSET_1:def 7;
then 2 c= card the carrier of (A . the Element of I) by Th2;
then consider b2 being object such that
A2: b2 in the carrier of (A . the Element of I) and
A3: b1 <> b2 by Th3;
reconsider b2 = b2 as Element of (A . the Element of I) by A2;
set B1 = B +* ( the Element of I,b2);
A4: for i being set st i in I holds
(B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
proof
let i be set ; :: thesis: ( i in I implies (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i )
assume A5: i in I ; :: thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
per cases ( i <> the Element of I or i = the Element of I ) ;
suppose i <> the Element of I ; :: thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
then (B +* ( the Element of I,b2)) . i = B . i by FUNCT_7:32;
hence (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i by A5, PBOOLE:def 14; :: thesis: verum
end;
suppose A6: i = the Element of I ; :: thesis: (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i
then the Element of I in dom B by A5, PARTFUN1:def 2;
hence (B +* ( the Element of I,b2)) . i is Element of (Carrier A) . i by A1, A6, FUNCT_7:31; :: thesis: verum
end;
end;
end;
{B,(B +* ( the Element of I,b2))} c= Carrier A
proof
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i )
assume A7: i in I ; :: thesis: {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i
then reconsider j = i as Element of I ;
j in dom A by A7, PARTFUN1:def 2;
then A . j in rng A by FUNCT_1:def 3;
then A8: not A . j is empty by YELLOW_6:def 2;
B . j is Element of (Carrier A) . j by PBOOLE:def 14;
then A9: B . j is Element of (A . j) by YELLOW_6:2;
(B +* ( the Element of I,b2)) . j is Element of (Carrier A) . j by A4;
then (B +* ( the Element of I,b2)) . j is Element of (A . j) by YELLOW_6:2;
then {(B . j),((B +* ( the Element of I,b2)) . j)} c= the carrier of (A . j) by A8, A9, ZFMISC_1:32;
then {B,(B +* ( the Element of I,b2))} . j c= the carrier of (A . j) by PZFMISC1:def 2;
hence {B,(B +* ( the Element of I,b2))} . i c= (Carrier A) . i by YELLOW_6:2; :: thesis: verum
end;
then reconsider C = {B,(B +* ( the Element of I,b2))} as ManySortedSubset of Carrier A by PBOOLE:def 18;
dom B = I by PARTFUN1:def 2;
then (B +* ( the Element of I,b2)) . the Element of I = b2 by FUNCT_7:31;
then A10: C . the Element of I = {b1,b2} by PZFMISC1:def 2;
A11: now :: thesis: not C . the Element of I is trivial
assume C . the Element of I is trivial ; :: thesis: contradiction
then ( C . the Element of I is empty or ex x being object st C . the Element of I = {x} ) by ZFMISC_1:131;
hence contradiction by A3, A10, ZFMISC_1:5; :: thesis: verum
end;
take C ; :: thesis: ( C is Segre-like & not C is trivial-yielding & C is V2() )
thus C is Segre-like :: thesis: ( not C is trivial-yielding & C is V2() )
proof
take the Element of I ; :: according to PENCIL_1:def 20 :: thesis: for j being Element of I st the Element of I <> j holds
C . j is 1 -element
let j be Element of I; :: thesis: ( the Element of I <> j implies C . j is 1 -element )
assume the Element of I <> j ; :: thesis: C . j is 1 -element
then B . j = (B +* ( the Element of I,b2)) . j by FUNCT_7:32;
then C . j = {(B . j),(B . j)} by PZFMISC1:def 2
.= {(B . j)} by ENUMSET1:29 ;
hence C . j is 1 -element ; :: thesis: verum
end;
dom C = I by PARTFUN1:def 2;
then C . the Element of I in rng C by FUNCT_1:def 3;
hence not C is trivial-yielding by A11; :: thesis: C is V2()
thus C is V2() ; :: thesis: verum