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
A1: 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
A2: 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

A3: now :: thesis: for a being set st a in I holds
s . a = t . a

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 j2 = t . i as Element of I ;
reconsider j1 = s . i as Element of I ;
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A4: indx b1 = i and
A5: 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 B1, PENCIL_2:24;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A6: fB = product b2 and
b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def 2;
j1 = indx b2 by A1, A4, A6
.= j2 by A2, A4, A6 ;
hence s . a = t . a ; :: thesis: verum

end;

( dom s = I & dom t = I ) by FUNCT_2:def 1;
hence s = t by A3, FUNCT_1:2; :: thesis: verum