let D be non empty set ; 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; 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; 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); ( 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
; 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 S1[ 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 & S1[x,y] )
consider P9 being Function of (Seg d),(Seg d) such that
A10:
for x being object st x in Seg d holds
S1[x,P9 . x]
from FUNCT_2:sch 1(A6);
now for x1, x2 being object st x1 in dom P9 & x2 in dom P9 & P9 . x1 = P9 . x2 holds
x1 = x2let x1,
x2 be
object ;
( 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
;
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
;
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 ;
( x9 in dom (XFS2FS G) implies (XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9 )
assume A25:
x9 in dom (XFS2FS G)
;
(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;
then A28:
x -' 1
= x - 1
by XREAL_1:233;
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 &
x -' 1
= x1 )
by A27, NAT_1:13, XREAL_1:233;
then
x -' 1
< len G
by A22, A33, XXREAL_0:2;
then
x -' 1
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, NAT_D:34;
1
<= (P . (x - 1)) + 1
by A32, A29, FINSEQ_1:1;
then
(F * P) . (x -' 1) = (XFS2FS F) . ((P . (x - 1)) + 1)
by A35, A28, A36, AFINSQ_1:def 9;
hence
(XFS2FS G) . x9 = ((XFS2FS F) * P9) . x9
by A31, A34, FUNCT_1:13;
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; verum