set s = permutation_of_indices f;
set i = indx b1;
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 st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) ) & f2 is isomorphic & ( for a being ManySortedSet of st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ) implies f1 = f2 )
assume that
A160: ( f1 is isomorphic & ( for a being ManySortedSet of st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f1 . (a . (indx b1)) ) ) and
A161: ( f2 is isomorphic & ( for a being ManySortedSet of st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = f2 . (a . (indx b1)) ) ) ; :: thesis: f1 = f2
A162: dom f1 = the carrier of (A . (indx b1)) by FUNCT_2:def 1
.= dom f2 by FUNCT_2:def 1 ;

now

let x be set ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider x0 = x as Point of (A . (indx b1)) ;
consider p being set such that
A163: p in product b1 by XBOOLE_0:def 1;
reconsider p = p as Point of (Segre_Product A) by A2, A163;
reconsider P = p as ManySortedSet of by PENCIL_1:14;
set a = P +* (indx b1),x0;
A164: ( dom (P +* (indx b1),x0) = I & dom P = I & dom b1 = I ) by PARTFUN1:def 4;

now

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

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

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

then (P +* (indx b1),x0) . e = x0 by A164, FUNCT_7:33;
then (P +* (indx b1),x0) . e in [#] (A . (indx b1)) ;
hence (P +* (indx b1),x0) . e in b1 . e by A2, A166, 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:34;
hence (P +* (indx b1),x0) . e in b1 . e by A163, A164, A165, CARD_3:18; :: thesis: verum

end;

end;

end;

then A167: P +* (indx b1),x0 in product b1 by A164, CARD_3:18;
reconsider a1 = P +* (indx b1),x0 as Point of (Segre_Product A) by PENCIL_1:25;
reconsider b = f . a1 as ManySortedSet of by PENCIL_1:14;
A168: f2 . ((P +* (indx b1),x0) . (indx b1)) = b . ((permutation_of_indices f) . (indx b1)) by A161, A167;
dom P = I by PARTFUN1:def 4;
then (P +* (indx b1),x0) . (indx b1) = x by FUNCT_7:33;
hence f1 . x = f2 . x by A160, A167, A168; :: thesis: verum

end;

hence f1 = f2 by A162, FUNCT_1:9; :: thesis: verum