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: now :: thesis: for a being object st a in I holds
s . a = t . a

let a be object ; :: 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
A5: indx b1 = i and
A6: product b1 is Segre-Coset of A by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A6;
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
A7: fB = product b2 and
b2 . (indx b2) = [#] (A . (indx b2)) by PENCIL_2:def 2;
j1 = indx b2 by A2, A5, A7
.= j2 by A3, A5, A7 ;
hence s . a = t . a ; :: thesis: verum

end;

thus s = t by A4; :: thesis: verum