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 A1, A3, PENCIL_1:26;

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 . b₁ = L2 . b₁ )
assume i in I ; :: thesis: L1 . b₁ = L2 . b₁

per cases ( i <> indx L1 or i = indx L1 ) ;

suppose i <> indx L1 ; :: thesis: L1 . b₁ = L2 . b₁

hence L1 . i = L2 . i by A5, A1, A3, PENCIL_1:26; :: thesis: verum

end;

suppose i = indx L1 ; :: thesis: L1 . b₁ = L2 . b₁

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 A1, A3, A8, A7, FUNCT_1:2; :: thesis: verum