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
A166: now :: thesis: for x being object st x in dom f1 holds
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;
A170: now :: thesis: for e being object st e in I holds
(P +* ((indx b1),x0)) . e in b1 . e
let e be object ; :: thesis: ( e in I implies (P +* ((indx b1),x0)) . b1 in b1 . b1 )
assume A171: e in I ; :: thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1
per cases ( e = indx b1 or e <> indx b1 ) ;
suppose A172: e = indx b1 ; :: thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1
then (P +* ((indx b1),x0)) . e = x0 by A169, FUNCT_7:31;
then (P +* ((indx b1),x0)) . e in [#] (A . (indx b1)) ;
hence (P +* ((indx b1),x0)) . e in b1 . e by A2, A172, Th10; :: thesis: verum
end;
suppose e <> indx b1 ; :: thesis: (P +* ((indx b1),x0)) . b1 in b1 . b1
then (P +* ((indx b1),x0)) . e = P . e by FUNCT_7:32;
hence (P +* ((indx b1),x0)) . e in b1 . e by A167, A168, A171, 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 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;
dom f1 = the carrier of (A . (indx b1)) by FUNCT_2:def 1
.= dom f2 by FUNCT_2:def 1 ;
hence f1 = f2 by A166; :: thesis: verum