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;
now :: thesis: for a being object st a in dom L1 holds
L1 . a = L2 . a
let a be object ; :: thesis: ( a in dom L1 implies L1 . b1 = L2 . b1 )
assume A14: a in dom L1 ; :: thesis: L1 . b1 = L2 . b1
then reconsider i = a as Element of I ;
per cases ( i = indx L1 or i <> indx L1 ) ;
suppose i = indx L1 ; :: thesis: L1 . b1 = L2 . b1
hence L1 . a = L2 . a by A2, A8, A10, A13, A11; :: thesis: verum
end;
suppose A15: i <> indx L1 ; :: thesis: L1 . b1 = L2 . b1
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;
end;
end;
hence L1 = L2 by A12; :: thesis: verum