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

( 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

thus
s = t
by A4; :: thesis: verums . 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;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