let I be non empty set ; :: thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of
for L1, L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 holds
L1 = L2
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of ; :: thesis: for L1, L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 holds
L1 = L2
let L1, L2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 implies L1 = L2 )
assume A1: ( product L1 is Segre-Coset of A & product L2 is Segre-Coset of A & indx L1 = indx L2 & product L1 meets product L2 ) ; :: thesis: L1 = L2
then reconsider B1 = product L1, B2 = product L2 as Segre-Coset of A ;
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A2: ( B1 = product b1 & b1 . (indx b1) = [#] (A . (indx b1)) ) by PENCIL_2:def 2;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3: ( B2 = product b2 & b2 . (indx b2) = [#] (A . (indx b2)) ) by PENCIL_2:def 2;
A4: ( b1 = L1 & b2 = L2 ) by A2, A3, PUA2MSS1:2;
B1 /\ B2 <> {} by A1, XBOOLE_0:def 7;
then consider x being set such that
A5: x in B1 /\ B2 by XBOOLE_0:def 1;
A6: ( x in B1 & x in B2 ) by A5, XBOOLE_0:def 4;
reconsider x = x as Element of Carrier A by A5, Th6;
A7: dom L1 = I by PARTFUN1:def 4
.= dom L2 by PARTFUN1:def 4 ;

now

let a be set ; :: thesis: ( a in dom L1 implies L1 . b₁ = L2 . b₁ )
assume A8: a in dom L1 ; :: thesis: L1 . b₁ = L2 . b₁
then reconsider i = a as Element of I by PARTFUN1:def 4;

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

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

hence L1 . a = L2 . a by A1, A2, A3, A4; :: thesis: verum

end;

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

then ( L1 . i is trivial & not L1 . i is empty ) by PENCIL_1:def 21;
then consider o1 being set such that
A10: L1 . i = {o1} by REALSET1:def 4;
( L2 . i is trivial & not L2 . i is empty ) by A1, A9, PENCIL_1:def 21;
then consider o2 being set such that
A11: L2 . i = {o2} by REALSET1:def 4;
A12: x . i in L1 . i by A6, A8, CARD_3:18;
A13: x . i in L2 . i by A6, A7, A8, CARD_3:18;
o1 = x . i by A10, A12, TARSKI:def 1
.= o2 by A11, A13, TARSKI:def 1 ;
hence L1 . a = L2 . a by A10, A11; :: thesis: verum

end;

end;

end;

hence L1 = L2 by A7, FUNCT_1:9; :: thesis: verum