let I be non empty set ; :: thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds
B1 = B2

let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I; :: thesis: for B1, B2 being Segre-Coset of A st 2 c= card (B1 /\ B2) holds
B1 = B2

let B1, B2 be Segre-Coset of A; :: thesis: ( 2 c= card (B1 /\ B2) implies B1 = B2 )
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A1: B1 = product L1 and
A2: L1 . (indx L1) = [#] (A . (indx L1)) by Def2;
consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3: B2 = product L2 and
A4: L2 . (indx L2) = [#] (A . (indx L2)) by Def2;
assume A5: 2 c= card (B1 /\ B2) ; :: thesis: B1 = B2
then A6: indx L1 = indx L2 by ;
A7: now :: thesis: for i being object st i in I holds
L1 . i = L2 . i
let i be object ; :: thesis: ( i in I implies L1 . b1 = L2 . b1 )
assume i in I ; :: thesis: L1 . b1 = L2 . b1
per cases ( i <> indx L1 or i = indx L1 ) ;
suppose i <> indx L1 ; :: thesis: L1 . b1 = L2 . b1
hence L1 . i = L2 . i by ; :: thesis: verum
end;
suppose i = indx L1 ; :: thesis: L1 . b1 = L2 . b1
hence L1 . i = L2 . i by A2, A4, A6; :: thesis: verum
end;
end;
end;
A8: dom L2 = I by PARTFUN1:def 2;
dom L1 = I by PARTFUN1:def 2;
hence B1 = B2 by ; :: thesis: verum