let D be non empty set ; :: thesis: for F, G being XFinSequence of D
for b being BinOp 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 b being BinOp 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 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, AFINSQ_1:def 9;
set xG = XFS2FS G;
defpred S₁[ set , set ] means for n being 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 x9 = x as Element of NAT by A6;
1 + 0 <= x9 by A6, FINSEQ_1:1;
then reconsider x91 = x9 - 1 as Element of NAT by NAT_1:21;
A7: x91 + 1 <= d by A6, FINSEQ_1:1;
then x91 < d by NAT_1:13;
then A8: x91 in d by NAT_1:44;
take (P . x91) + 1 ; :: thesis: ( (P . x91) + 1 in Seg d & S₁[x,(P . x91) + 1] )
dom F = dom P by A7, FUNCT_2:def 1;
then P . x91 in rng P by A8, FUNCT_1:def 3;
then P . x91 < d by NAT_1:44;
then ( 0 + 1 <= (P . x91) + 1 & (P . x91) + 1 <= d ) by NAT_1:13;
hence ( (P . x91) + 1 in Seg d & S₁[x,(P . x91) + 1] ) by FINSEQ_1:1; :: thesis: verum

end;

consider P9 being Function of (Seg d),(Seg d) such that
A9: for x being set st x in Seg d holds
S₁[x,P9 . x] from FUNCT_2:sch 1(A5);

now

let x1, x2 be set ; :: thesis: ( x1 in dom P9 & x2 in dom P9 & P9 . x1 = P9 . x2 implies x1 = x2 )
assume that
A10: x1 in dom P9 and
A11: x2 in dom P9 and
A12: P9 . x1 = P9 . x2 ; :: thesis: x1 = x2
dom P9 = Seg d by FUNCT_2:52;
then reconsider X1 = x1, X2 = x2 as Element of NAT by A10, A11;
( 1 + 0 <= X1 & 1 + 0 <= X2 ) by A10, A11, FINSEQ_1:1;
then reconsider X19 = X1 - 1, X29 = X2 - 1 as Element of NAT by NAT_1:21;
A13: ( X19 < X19 + 1 & X1 <= d ) by A10, FINSEQ_1:1, NAT_1:13;
then A14: dom P = dom F by FUNCT_2:def 1;
( X29 < X29 + 1 & X2 <= d ) by A11, FINSEQ_1:1, NAT_1:13;
then X29 < d by XXREAL_0:2;
then A15: X29 in dom P by A14, NAT_1:44;
X19 < d by A13, XXREAL_0:2;
then A16: X19 in dom P by A14, NAT_1:44;
P9 . X1 = (P . X19) + 1 by A9, A10;
then ((P . X19) + 1) - 1 = ((P . X29) + 1) - 1 by A9, A11, A12;
then (X1 - 1) + 1 = (X2 - 1) + 1 by A16, A15, FUNCT_1:def 4;
hence x1 = x2 ; :: thesis: verum

end;

then A17: P9 is one-to-one by FUNCT_1:def 4;
card (Seg d) = card (Seg d) ;
then A18: ( P9 is one-to-one & P9 is onto ) by A17, Lm2;
len (XFS2FS F) = len F by AFINSQ_1:def 9;
then dom (XFS2FS F) = Seg (len F) by FINSEQ_1:def 3;
then reconsider P9 = P9 as Permutation of (dom (XFS2FS F)) by A18;
A19: ( dom P9 = Seg d & dom (XFS2FS G) = Seg (len (XFS2FS G)) ) by FINSEQ_1:def 3, FUNCT_2:52;
rng P9 c= dom (XFS2FS F) ;
then A20: dom ((XFS2FS F) * P9) = dom P9 by RELAT_1:27;
rng P c= dom F ;
then dom (F * P) = dom P by RELAT_1:27;
then A21: dom G = dom F by A3, FUNCT_2:52;
A22: dom G = len G ;
A23: for x9 being set st x9 in dom (XFS2FS G) holds
(XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9

proof

let x9 be set ; :: thesis: ( x9 in dom (XFS2FS G) implies (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 )
assume A24: x9 in dom (XFS2FS G) ; :: thesis: (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9
reconsider x = x9 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:1;
then A27: x -' 1 = x - 1 by XREAL_1:233;
0 < x by A24, A25, FINSEQ_1:1;
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 AFINSQ_1:def 9;
then A30: ( (P . (x - 1)) + 1 = P9 . x & x in dom P9 ) by A9, A21, A24, A25, FUNCT_2:52;
then A31: (P . (x - 1)) + 1 in rng P9 by FUNCT_1:def 3;
A32: x <= len F by A21, A24, A25, A29, FINSEQ_1:1;
then A33: (XFS2FS G) . x = (F * P) . (x -' 1) by A3, A21, A22, A26, AFINSQ_1:def 9;
len (XFS2FS F) = len F by AFINSQ_1:def 9;
then A34: (P . (x - 1)) + 1 <= len F by A31, A28, FINSEQ_1:1;
( x1 < x1 + 1 & x -' 1 = x1 ) by A26, NAT_1:13, XREAL_1:233;
then x -' 1 < dom G by A21, A32, XXREAL_0:2;
then x -' 1 in dom G by NAT_1:44;
then A35: ( ((P . (x -' 1)) + 1) -' 1 = P . (x -' 1) & (F * P) . (x -' 1) = F . (P . (x -' 1)) ) by A3, FUNCT_1:12, NAT_D:34;
1 <= (P . (x - 1)) + 1 by A31, A28, FINSEQ_1:1;
then (F * P) . (x -' 1) = (XFS2FS F) . ((P . (x - 1)) + 1) by A34, A27, A35, AFINSQ_1:def 9;
hence (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 by A30, A33, FUNCT_1:13; :: thesis: verum

end;

len (XFS2FS G) = len F by A21, A22, AFINSQ_1:def 9;
then XFS2FS G = (XFS2FS F) * P9 by A23, A20, A19, FUNCT_1:def 11;
then A36: b "**" (XFS2FS G) = b "**" (XFS2FS F) by A1, A4, FINSOP_1:7;
b "**" (XFS2FS G) = b "**" G by A2, A21, A22, Th56;
hence b "**" F = b "**" G by A2, A36, Th56; :: thesis: verum