let I be non empty set ; :: thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I

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 I; :: 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 that

A1: ( product L1 is Segre-Coset of A & product L2 is Segre-Coset of A ) and

A2: indx L1 = indx L2 and

A3: product L1 meets product L2 ; :: thesis: L1 = L2

reconsider B1 = product L1, B2 = product L2 as Segre-Coset of A by A1;

B1 /\ B2 <> {} by A3;

then consider x being object such that

A4: x in B1 /\ B2 by XBOOLE_0:def 1;

A5: x in B2 by A4, XBOOLE_0:def 4;

A6: x in B1 by A4, XBOOLE_0:def 4;

reconsider x = x as Element of Carrier A by A4, Th6;

consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A7: B1 = product b1 and

A8: 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

A9: B2 = product b2 and

A10: b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def 2;

A11: b2 = L2 by A9, PUA2MSS1:2;

A12: dom L1 = I by PARTFUN1:def 2

.= dom L2 by PARTFUN1:def 2 ;

A13: b1 = L1 by A7, PUA2MSS1:2;

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 I; :: 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 that

A1: ( product L1 is Segre-Coset of A & product L2 is Segre-Coset of A ) and

A2: indx L1 = indx L2 and

A3: product L1 meets product L2 ; :: thesis: L1 = L2

reconsider B1 = product L1, B2 = product L2 as Segre-Coset of A by A1;

B1 /\ B2 <> {} by A3;

then consider x being object such that

A4: x in B1 /\ B2 by XBOOLE_0:def 1;

A5: x in B2 by A4, XBOOLE_0:def 4;

A6: x in B1 by A4, XBOOLE_0:def 4;

reconsider x = x as Element of Carrier A by A4, Th6;

consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A7: B1 = product b1 and

A8: 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

A9: B2 = product b2 and

A10: b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def 2;

A11: b2 = L2 by A9, PUA2MSS1:2;

A12: dom L1 = I by PARTFUN1:def 2

.= dom L2 by PARTFUN1:def 2 ;

A13: b1 = L1 by A7, PUA2MSS1:2;

now :: thesis: for a being object st a in dom L1 holds

L1 . a = L2 . a

hence
L1 = L2
by A12; :: thesis: verumL1 . a = L2 . a

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

assume A14: a in dom L1 ; :: thesis: L1 . b_{1} = L2 . b_{1}

then reconsider i = a as Element of I ;

end;assume A14: a in dom L1 ; :: thesis: L1 . b

then reconsider i = a as Element of I ;

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

end;

suppose A15:
i <> indx L1
; :: thesis: L1 . b_{1} = L2 . b_{1}

then
( not L1 . i is empty & L1 . i is trivial )
by PENCIL_1:def 21;

then L1 . i is 1 -element ;

then consider o1 being object such that

A16: L1 . i = {o1} by ZFMISC_1:131;

( not L2 . i is empty & L2 . i is trivial ) by A2, A15, PENCIL_1:def 21;

then L2 . i is 1 -element ;

then consider o2 being object such that

A17: L2 . i = {o2} by ZFMISC_1:131;

A18: x . i in L2 . i by A5, A12, A14, CARD_3:9;

x . i in L1 . i by A6, A14, CARD_3:9;

then o1 = x . i by A16, TARSKI:def 1

.= o2 by A17, A18, TARSKI:def 1 ;

hence L1 . a = L2 . a by A16, A17; :: thesis: verum

end;then L1 . i is 1 -element ;

then consider o1 being object such that

A16: L1 . i = {o1} by ZFMISC_1:131;

( not L2 . i is empty & L2 . i is trivial ) by A2, A15, PENCIL_1:def 21;

then L2 . i is 1 -element ;

then consider o2 being object such that

A17: L2 . i = {o2} by ZFMISC_1:131;

A18: x . i in L2 . i by A5, A12, A14, CARD_3:9;

x . i in L1 . i by A6, A14, CARD_3:9;

then o1 = x . i by A16, TARSKI:def 1

.= o2 by A17, A18, TARSKI:def 1 ;

hence L1 . a = L2 . a by A16, A17; :: thesis: verum