let D be non empty set ; :: thesis: for b being BinOp of D
for F, G being XFinSequence of
for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
let b be BinOp of D; :: thesis: for F, G being XFinSequence of
for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
let F, G be XFinSequence of ; :: thesis: for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G
let P be Permutation of (dom F); :: thesis: ( b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P implies b "**" F = b "**" G )
assume that
A1: ( b is commutative & b is associative ) and
A2: ( b is having_a_unity or len F >= 1 ) and
A3: G = F * P ; :: thesis: b "**" F = b "**" G
dom F = len F ;
then reconsider d = dom F as Element of NAT ;
defpred S₁[ set , set ] means for n being Element of NAT st $1 = n holds
$2 = (P . (n - 1)) + 1;
A4: for x being set st x in Seg d holds
ex y being set st
( y in Seg d & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Seg d implies ex y being set st
( y in Seg d & S₁[x,y] ) )
assume A5: x in Seg d ; :: thesis: ex y being set st
( y in Seg d & S₁[x,y] )
reconsider x' = x as Element of NAT by A5;
1 + 0 <= x' by A5, FINSEQ_1:3;
then reconsider x'1 = x' - 1 as Element of NAT by NAT_1:21;
take (P . x'1) + 1 ; :: thesis: ( (P . x'1) + 1 in Seg d & S₁[x,(P . x'1) + 1] )
x'1 + 1 <= d by A5, FINSEQ_1:3;
then ( x'1 < d & ( dom F = {} implies dom F = {} ) ) by NAT_1:13;
then ( x'1 in d & dom F = dom P ) by FUNCT_2:def 1, NAT_1:45;
then P . x'1 in rng P by FUNCT_1:def 5;
then P . x'1 < d by NAT_1:45;
then ( 0 + 1 <= (P . x'1) + 1 & (P . x'1) + 1 <= d ) by NAT_1:13;
hence ( (P . x'1) + 1 in Seg d & S₁[x,(P . x'1) + 1] ) by FINSEQ_1:3; :: thesis: verum

end;

consider P' being Function of (Seg d),(Seg d) such that
A6: for x being set st x in Seg d holds
S₁[x,P' . x] from FUNCT_2:sch 1(A4);
set xF = XFS2FS F;
set xG = XFS2FS G;

now

let x1, x2 be set ; :: thesis: ( x1 in dom P' & x2 in dom P' & P' . x1 = P' . x2 implies x1 = x2 )
assume A7: ( x1 in dom P' & x2 in dom P' & P' . x1 = P' . x2 ) ; :: thesis: x1 = x2
dom P' = Seg d by FUNCT_2:67;
then reconsider X1 = x1, X2 = x2 as Element of NAT by A7;
( 1 + 0 <= X1 & 1 + 0 <= X2 ) by A7, FINSEQ_1:3;
then reconsider X1' = X1 - 1, X2' = X2 - 1 as Element of NAT by NAT_1:21;
A8: ( X1' < X1' + 1 & X2' < X2' + 1 & X1 <= d & X2 <= d ) by A7, FINSEQ_1:3, NAT_1:13;
then A9: ( X1' < d & X2' < d & ( dom F = {} implies dom F = {} ) ) by XXREAL_0:2;
( P' . X1 = (P . X1') + 1 & P' . X2 = (P . X2') + 1 ) by A6, A7;
then ( ((P . X1') + 1) - 1 = ((P . X2') + 1) - 1 & ((P . X2') + 1) - 1 = P . X2' & ((P . X1') + 1) - 1 = P . X1' & P' . X1 = (P . X1') + 1 & P' . X2 = (P . X2') + 1 & dom P = dom F ) by A7, A8, FUNCT_2:def 1;
then ( P . X1' = P . X2' & X1' in dom P & X2' in dom P ) by A9, NAT_1:45;
then ( (X1 - 1) + 1 = (X2 - 1) + 1 & (X1 - 1) + 1 = X1 ) by FUNCT_1:def 8;
hence x1 = x2 ; :: thesis: verum

end;

then ( P' is one-to-one & card (Seg d) = card (Seg d) & len (XFS2FS F) = len F ) by FUNCT_1:def 8, PRGCOR_2:def 2;
then ( P' is one-to-one & P' is onto & dom (XFS2FS F) = Seg (len F) & len F = d ) by FINSEQ_1:def 3, STIRL2_1:70;
then reconsider P' = P' as Permutation of (dom (XFS2FS F)) ;
rng P c= dom F ;
then ( dom (F * P) = dom P & dom P = dom F ) by FUNCT_2:67, RELAT_1:46;
then A10: ( dom G = dom F & dom F = len F & dom G = len G ) by A3;
XFS2FS G = (XFS2FS F) * P'

proof

A11: for x' being set st x' in dom (XFS2FS G) holds
(XFS2FS G) . x' = ((XFS2FS F) * P') . x'

proof

let x' be set ; :: thesis: ( x' in dom (XFS2FS G) implies (XFS2FS G) . x' = ((XFS2FS F) * P') . x' )
assume A12: x' in dom (XFS2FS G) ; :: thesis: (XFS2FS G) . x' = ((XFS2FS F) * P') . x'
reconsider x = x' as Element of NAT by A12;
A13: ( dom (XFS2FS G) = Seg (len (XFS2FS G)) & len (XFS2FS G) = len G ) by FINSEQ_1:def 3, PRGCOR_2:def 2;
then 0 < x by A12, FINSEQ_1:3;
then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
A14: ( 1 <= x & x <= len F ) by A10, A12, A13, FINSEQ_1:3;
then ( x1 < x1 + 1 & x -' 1 = x1 & x <= len F ) by NAT_1:13, XREAL_1:235;
then A15: x -' 1 < dom G by A10, XXREAL_0:2;
A16: ( (P . (x - 1)) + 1 = P' . x & x in dom P' ) by A6, A10, A12, A13, FUNCT_2:67;
then (P . (x - 1)) + 1 in rng P' by FUNCT_1:def 5;
then ( (P . (x - 1)) + 1 in dom (XFS2FS F) & dom (XFS2FS F) = Seg (len (XFS2FS F)) & len (XFS2FS F) = len F ) by FINSEQ_1:def 3, PRGCOR_2:def 2;
then ( 1 <= (P . (x - 1)) + 1 & (P . (x - 1)) + 1 <= len F & x -' 1 = x - 1 & (P . (x -' 1)) + 1 is Element of NAT & x -' 1 in dom G ) by A14, A15, FINSEQ_1:3, NAT_1:45, XREAL_1:235;
then ( F . (((P . (x -' 1)) + 1) -' 1) = (XFS2FS F) . ((P . (x -' 1)) + 1) & ((P . (x -' 1)) + 1) -' 1 = P . (x -' 1) & (F * P) . (x -' 1) = F . (P . (x -' 1)) ) by A3, FUNCT_1:22, NAT_D:34, PRGCOR_2:def 2;
then ( (F * P) . (x -' 1) = (XFS2FS F) . ((P . (x - 1)) + 1) & (XFS2FS G) . x = (F * P) . (x -' 1) ) by A3, A10, A14, PRGCOR_2:def 2, XREAL_1:235;
hence (XFS2FS G) . x' = ((XFS2FS F) * P') . x' by A16, FUNCT_1:23; :: thesis: verum

end;

rng P' c= dom (XFS2FS F) ;
then ( dom ((XFS2FS F) * P') = dom P' & dom P' = Seg d & dom (XFS2FS G) = Seg (len (XFS2FS G)) & len (XFS2FS G) = len F ) by A10, FINSEQ_1:def 3, FUNCT_2:67, PRGCOR_2:def 2, RELAT_1:46;
hence XFS2FS G = (XFS2FS F) * P' by A11, FUNCT_1:9; :: thesis: verum

end;

then ( XFS2FS G = (XFS2FS F) * P' & ( b is having_a_unity or len (XFS2FS F) >= 1 ) ) by A2, PRGCOR_2:def 2;
then ( b "**" (XFS2FS G) = b "**" (XFS2FS F) & b "**" (XFS2FS G) = b "**" G ) by A1, A2, A10, Th47, FINSOP_1:8;
hence b "**" F = b "**" G by A2, Th47; :: thesis: verum