set i = indx b1;
set s = permutation_of_indices f;
let f1, f2 be Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))); :: thesis: ( f1 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) ) & f2 is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ) implies f1 = f2 )
assume that
f1 is isomorphic and
A162: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) and
f2 is isomorphic and
A163: for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ; :: thesis: f1 = f2

A164: now :: thesis: for x being set st x in dom f1 holds
f1 . x = f2 . x

let x be set ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
consider p being set such that
A165: p in product b1 by XBOOLE_0:def 1;
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider x0 = x as Point of (A . (indx b1)) ;
reconsider p = p as Point of (Segre_Product A) by B2, A165;
reconsider P = p as ManySortedSet of I by PENCIL_1:14;
set a = P +* ((indx b1),x0);
reconsider a1 = P +* ((indx b1),x0) as Point of (Segre_Product A) by PENCIL_1:25;
A166: dom b1 = I by PARTFUN1:def 2;
A167: dom P = I by PARTFUN1:def 2;

A168: now :: thesis: for e being set st e in I holds
(P +* ((indx b1),x0)) . e in b1 . e

let e be set ; :: thesis: ( e in I implies (P +* ((indx b1),x0)) . b₁ in b1 . b₁ )
assume A169: e in I ; :: thesis: (P +* ((indx b1),x0)) . b₁ in b1 . b₁

per cases ( e = indx b1 or e <> indx b1 ) ;

suppose A170: e = indx b1 ; :: thesis: (P +* ((indx b1),x0)) . b₁ in b1 . b₁

then (P +* ((indx b1),x0)) . e = x0 by A167, FUNCT_7:31;
then (P +* ((indx b1),x0)) . e in [#] (A . (indx b1)) ;
hence (P +* ((indx b1),x0)) . e in b1 . e by B2, A170, Th10; :: thesis: verum

end;

suppose e <> indx b1 ; :: thesis: (P +* ((indx b1),x0)) . b₁ in b1 . b₁

then (P +* ((indx b1),x0)) . e = P . e by FUNCT_7:32;
hence (P +* ((indx b1),x0)) . e in b1 . e by A165, A166, A169, CARD_3:9; :: thesis: verum

end;

end;

end;

reconsider b = f . a1 as ManySortedSet of I by PENCIL_1:14;
dom P = I by PARTFUN1:def 2;
then A171: (P +* ((indx b1),x0)) . (indx b1) = x by FUNCT_7:31;
dom (P +* ((indx b1),x0)) = I by PARTFUN1:def 2;
then A172: P +* ((indx b1),x0) in product b1 by A166, A168, CARD_3:9;
then f2 . ((P +* ((indx b1),x0)) . (indx b1)) = b . ((permutation_of_indices f) . (indx b1)) by A163;
hence f1 . x = f2 . x by A162, A172, A171; :: thesis: verum

end;

dom f1 = the carrier of (A . (indx b1)) by FUNCT_2:def 1
.= dom f2 by FUNCT_2:def 1 ;
hence f1 = f2 by A164, FUNCT_1:2; :: thesis: verum