let D be non empty set ; :: thesis: for b being BinOp of D
for F, G being XFinSequence of D
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 D
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 D; :: 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
set xF = XFS2FS F;
A4: ( b is having_a_unity or len (XFS2FS F) >= 1 ) by A2, PRGCOR_2:def 2;
set xG = XFS2FS G;
defpred S₁[ set , set ] means for n being Element of NAT st $1 = n holds
$2 = (P . (n - 1)) + 1;
dom F = len F ;
then reconsider d = dom F as Element of NAT ;
A5: 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 A6: 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 A6;
1 + 0 <= x' by A6, FINSEQ_1:3;
then reconsider x'1 = x' - 1 as Element of NAT by NAT_1:21;
A7: x'1 + 1 <= d by A6, FINSEQ_1:3;
then x'1 < d by NAT_1:13;
then A8: x'1 in d by NAT_1:45;
take (P . x'1) + 1 ; :: thesis: ( (P . x'1) + 1 in Seg d & S₁[x,(P . x'1) + 1] )
dom F = dom P by A7, FUNCT_2:def 1;
then P . x'1 in rng P by A8, 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
A9: for x being set st x in Seg d holds
S₁[x,P' . x] from FUNCT_2:sch 1(A5);

now

let x1, x2 be set ; :: thesis: ( x1 in dom P' & x2 in dom P' & P' . x1 = P' . x2 implies x1 = x2 )
assume that
A10: x1 in dom P' and
A11: x2 in dom P' and
A12: 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 A10, A11;
( 1 + 0 <= X1 & 1 + 0 <= X2 ) by A10, A11, FINSEQ_1:3;
then reconsider X1' = X1 - 1, X2' = X2 - 1 as Element of NAT by NAT_1:21;
A13: ( X1' < X1' + 1 & X1 <= d ) by A10, FINSEQ_1:3, NAT_1:13;
then A14: dom P = dom F by FUNCT_2:def 1;
( X2' < X2' + 1 & X2 <= d ) by A11, FINSEQ_1:3, NAT_1:13;
then X2' < d by XXREAL_0:2;
then A15: X2' in dom P by A14, NAT_1:45;
X1' < d by A13, XXREAL_0:2;
then A16: X1' in dom P by A14, NAT_1:45;
P' . X1 = (P . X1') + 1 by A9, A10;
then ((P . X1') + 1) - 1 = ((P . X2') + 1) - 1 by A9, A11, A12;
then (X1 - 1) + 1 = (X2 - 1) + 1 by A16, A15, FUNCT_1:def 8;
hence x1 = x2 ; :: thesis: verum

end;

then A17: P' is one-to-one by FUNCT_1:def 8;
card (Seg d) = card (Seg d) ;
then A18: ( P' is one-to-one & P' is onto ) by A17, STIRL2_1:70;
len (XFS2FS F) = len F by PRGCOR_2:def 2;
then dom (XFS2FS F) = Seg (len F) by FINSEQ_1:def 3;
then reconsider P' = P' as Permutation of dom (XFS2FS F) by A18;
A19: ( dom P' = Seg d & dom (XFS2FS G) = Seg (len (XFS2FS G)) ) by FINSEQ_1:def 3, FUNCT_2:67;
rng P' c= dom (XFS2FS F) ;
then A20: dom ((XFS2FS F) * P') = dom P' by RELAT_1:46;
rng P c= dom F ;
then dom (F * P) = dom P by RELAT_1:46;
then A21: dom G = dom F by A3, FUNCT_2:67;
A22: dom G = len G ;
A23: 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 A24: x' in dom (XFS2FS G) ; :: thesis: (XFS2FS G) . x' = ((XFS2FS F) * P') . x'
reconsider x = x' as Element of NAT by A24;
A25: dom (XFS2FS G) = Seg (len (XFS2FS G)) by FINSEQ_1:def 3;
then A26: 1 <= x by A24, FINSEQ_1:3;
then A27: x -' 1 = x - 1 by XREAL_1:235;
0 < x by A24, A25, FINSEQ_1:3;
then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
A28: dom (XFS2FS F) = Seg (len (XFS2FS F)) by FINSEQ_1:def 3;
A29: len (XFS2FS G) = len G by PRGCOR_2:def 2;
then A30: ( (P . (x - 1)) + 1 = P' . x & x in dom P' ) by A9, A21, A24, A25, FUNCT_2:67;
then A31: (P . (x - 1)) + 1 in rng P' by FUNCT_1:def 5;
A32: x <= len F by A21, A24, A25, A29, FINSEQ_1:3;
then A33: (XFS2FS G) . x = (F * P) . (x -' 1) by A3, A21, A22, A26, PRGCOR_2:def 2;
len (XFS2FS F) = len F by PRGCOR_2:def 2;
then A34: (P . (x - 1)) + 1 <= len F by A31, A28, FINSEQ_1:3;
( x1 < x1 + 1 & x -' 1 = x1 ) by A26, NAT_1:13, XREAL_1:235;
then x -' 1 < dom G by A21, A32, XXREAL_0:2;
then x -' 1 in dom G by NAT_1:45;
then A35: ( ((P . (x -' 1)) + 1) -' 1 = P . (x -' 1) & (F * P) . (x -' 1) = F . (P . (x -' 1)) ) by A3, FUNCT_1:22, NAT_D:34;
1 <= (P . (x - 1)) + 1 by A31, A28, FINSEQ_1:3;
then (F * P) . (x -' 1) = (XFS2FS F) . ((P . (x - 1)) + 1) by A34, A27, A35, PRGCOR_2:def 2;
hence (XFS2FS G) . x' = ((XFS2FS F) * P') . x' by A30, A33, FUNCT_1:23; :: thesis: verum

end;

len (XFS2FS G) = len F by A21, A22, PRGCOR_2:def 2;
then XFS2FS G = (XFS2FS F) * P' by A23, A20, A19, FUNCT_1:def 17;
then A36: b "**" (XFS2FS G) = b "**" (XFS2FS F) by A1, A4, FINSOP_1:8;
b "**" (XFS2FS G) = b "**" G by A2, A21, A22, Th47;
hence b "**" F = b "**" G by A2, A36, Th47; :: thesis: verum