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

A164: 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

A165: 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

.= dom f2 by FUNCT_2:def 1 ;

hence f1 = f2 by A166; :: thesis: verum

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

A164: 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

A165: 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

A166: now :: thesis: for x being object st x in dom f1 holds

f1 . x = f2 . x

dom f1 =
the carrier of (A . (indx b1))
by FUNCT_2:def 1
f1 . x = f2 . x

let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )

consider p being object such that

A167: 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 A2, A167;

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;

A168: dom b1 = I by PARTFUN1:def 2;

A169: dom P = I by PARTFUN1:def 2;

dom P = I by PARTFUN1:def 2;

then A173: (P +* ((indx b1),x0)) . (indx b1) = x by FUNCT_7:31;

dom (P +* ((indx b1),x0)) = I by PARTFUN1:def 2;

then A174: P +* ((indx b1),x0) in product b1 by A168, A170, CARD_3:9;

then f2 . ((P +* ((indx b1),x0)) . (indx b1)) = b . ((permutation_of_indices f) . (indx b1)) by A165;

hence f1 . x = f2 . x by A164, A174, A173; :: thesis: verum

end;consider p being object such that

A167: 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 A2, A167;

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;

A168: dom b1 = I by PARTFUN1:def 2;

A169: dom P = I by PARTFUN1:def 2;

A170: now :: thesis: for e being object st e in I holds

(P +* ((indx b1),x0)) . e in b1 . e

reconsider b = f . a1 as ManySortedSet of I by PENCIL_1:14;(P +* ((indx b1),x0)) . e in b1 . e

let e be object ; :: thesis: ( e in I implies (P +* ((indx b1),x0)) . b_{1} in b1 . b_{1} )

assume A171: e in I ; :: thesis: (P +* ((indx b1),x0)) . b_{1} in b1 . b_{1}

end;assume A171: e in I ; :: thesis: (P +* ((indx b1),x0)) . b

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

end;

dom P = I by PARTFUN1:def 2;

then A173: (P +* ((indx b1),x0)) . (indx b1) = x by FUNCT_7:31;

dom (P +* ((indx b1),x0)) = I by PARTFUN1:def 2;

then A174: P +* ((indx b1),x0) in product b1 by A168, A170, CARD_3:9;

then f2 . ((P +* ((indx b1),x0)) . (indx b1)) = b . ((permutation_of_indices f) . (indx b1)) by A165;

hence f1 . x = f2 . x by A164, A174, A173; :: thesis: verum

.= dom f2 by FUNCT_2:def 1 ;

hence f1 = f2 by A166; :: thesis: verum