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;

dom L1 = I by PARTFUN1:def 2;

hence B1 = B2 by A1, A3, A8, A7, FUNCT_1:2; :: thesis: verum

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

A8:
dom L2 = I
by PARTFUN1:def 2;L1 . i = L2 . i

let i be object ; :: thesis: ( i in I implies L1 . b_{1} = L2 . b_{1} )

assume i in I ; :: thesis: L1 . b_{1} = L2 . b_{1}

end;assume i in I ; :: thesis: L1 . b

dom L1 = I by PARTFUN1:def 2;

hence B1 = B2 by A1, A3, A8, A7, FUNCT_1:2; :: thesis: verum