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₁[ object , object ] 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 ;
A6: for x being object st x in Seg d holds
ex y being object st
( y in Seg d & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Seg d implies ex y being object st
( y in Seg d & S₁[x,y] ) )
assume A7: x in Seg d ; :: thesis: ex y being object st
( y in Seg d & S₁[x,y] )
reconsider x9 = x as Element of NAT by A7;
1 + zz <= x9 by A7, FINSEQ_1:1;
then reconsider x91 = x9 - 1 as Element of NAT by NAT_1:21;
A8: x91 + 1 <= d by A7, FINSEQ_1:1;
then x91 < d by NAT_1:13;
then A9: x91 in Segm 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 A8, FUNCT_2:def 1;
then P . x91 in rng P by A9, FUNCT_1:def 3;
then P . x91 < d by AFINSQ_1:86;
then ( zz + 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
A10: for x being object st x in Seg d holds
S₁[x,P9 . x] from FUNCT_2:sch 1(A6);

now :: thesis: for x1, x2 being object st x1 in dom P9 & x2 in dom P9 & P9 . x1 = P9 . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom P9 & x2 in dom P9 & P9 . x1 = P9 . x2 implies x1 = x2 )
assume that
A11: x1 in dom P9 and
A12: x2 in dom P9 and
A13: 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 A11, A12;
( 1 + zz <= X1 & 1 + zz <= X2 ) by A11, A12, FINSEQ_1:1;
then reconsider X19 = X1 - 1, X29 = X2 - 1 as Element of NAT by NAT_1:21;
A14: ( X19 < X19 + 1 & X1 <= d ) by A11, FINSEQ_1:1, NAT_1:13;
then A15: dom P = dom F by FUNCT_2:def 1;
( X29 < X29 + 1 & X2 <= d ) by A12, FINSEQ_1:1, NAT_1:13;
then X29 < d by XXREAL_0:2;
then A16: X29 in dom P by A15, AFINSQ_1:86;
X19 < d by A14, XXREAL_0:2;
then A17: X19 in dom P by A15, AFINSQ_1:86;
P9 . X1 = (P . X19) + 1 by A10, A11;
then ((P . X19) + 1) - 1 = ((P . X29) + 1) - 1 by A10, A12, A13;
then (X1 - 1) + 1 = (X2 - 1) + 1 by A17, A16, FUNCT_1:def 4;
hence x1 = x2 ; :: thesis: verum

end;

then A18: P9 is one-to-one ;
card (Seg d) = card (Seg d) ;
then A19: ( P9 is one-to-one & P9 is onto ) by A18, Lm1;
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 A19;
A20: ( 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 A21: 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 A22: dom G = dom F by A3, FUNCT_2:52;
A24: for x9 being object st x9 in dom (XFS2FS G) holds
(XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9

proof

let x9 be object ; :: thesis: ( x9 in dom (XFS2FS G) implies (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 )
assume A25: x9 in dom (XFS2FS G) ; :: thesis: (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9
reconsider x = x9 as Element of NAT by A25;
A26: dom (XFS2FS G) = Seg (len (XFS2FS G)) by FINSEQ_1:def 3;
then A27: 1 <= x by A25, FINSEQ_1:1;
0 < x by A25, A26, FINSEQ_1:1;
then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
A29: dom (XFS2FS F) = Seg (len (XFS2FS F)) by FINSEQ_1:def 3;
A30: len (XFS2FS G) = len G by AFINSQ_1:def 9;
then A31: ( (P . (x - 1)) + 1 = P9 . x & x in dom P9 ) by A10, A22, A25, A26, FUNCT_2:52;
then A32: (P . (x - 1)) + 1 in rng P9 by FUNCT_1:def 3;
A33: x <= len F by A22, A25, A26, A30, FINSEQ_1:1;
then A34: (XFS2FS G) . x = (F * P) . (x - 1) by A3, A22, A27, AFINSQ_1:def 9;
len (XFS2FS F) = len F by AFINSQ_1:def 9;
then A35: (P . (x - 1)) + 1 <= len F by A32, A29, FINSEQ_1:1;
x1 < x1 + 1 by NAT_1:13;
then x1 < len G by A22, A33, XXREAL_0:2;
then x1 in dom G by AFINSQ_1:86;
then A36: ( ((P . (x - 1)) + 1) - 1 = P . (x - 1) & (F * P) . (x - 1) = F . (P . (x - 1)) ) by A3, FUNCT_1:12;
1 <= (P . (x - 1)) + 1 by A32, A29, FINSEQ_1:1;
then (F * P) . x1 = (XFS2FS F) . ((P . x1) + 1) by A35, A36, AFINSQ_1:def 9;
hence (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 by A31, A34, FUNCT_1:13; :: thesis: verum

end;

len (XFS2FS G) = len F by A22, AFINSQ_1:def 9;
then XFS2FS G = (XFS2FS F) * P9 by A24, A21, A20;
then A37: b "**" (XFS2FS G) = b "**" (XFS2FS F) by A1, A4, FINSOP_1:7;
b "**" (XFS2FS G) = b "**" G by A2, A22, Th43;
hence b "**" F = b "**" G by A2, A37, Th43; :: thesis: verum