let s, t be Permutation of I; :: thesis: ( ( for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) & ( for i, j being Element of I holds
( t . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ) implies s = t )
assume that
A2: for i, j being Element of I holds
( s . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) and
A3: for i, j being Element of I holds
( t . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) ; :: thesis: s = t
A4: ( dom s = I & dom t = I ) by FUNCT_2:def 1;

now

let a be set ; :: thesis: ( a in I implies s . a = t . a )
assume a in I ; :: thesis: s . a = t . a
then reconsider i = a as Element of I ;
reconsider j1 = s . i as Element of I ;
reconsider j2 = t . i as Element of I ;
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A5: ( indx b1 = i & product b1 is Segre-Coset of A ) by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A5;
reconsider fB = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A6: ( fB = product b2 & b2 . (indx b2) = [#] (A . (indx b2)) ) by PENCIL_2:def 2;
j1 = indx b2 by A2, A5, A6
.= j2 by A3, A5, A6 ;
hence s . a = t . a ; :: thesis: verum

end;

hence s = t by A4, FUNCT_1:9; :: thesis: verum