let D be non empty set ; for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds
g "**" F = g "**" G
let F, G be FinSequence of D; for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds
g "**" F = g "**" G
let g be BinOp of D; ( g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 implies g "**" F = g "**" G )
assume that
A1:
( g is associative & g is commutative )
and
A2:
F is one-to-one
and
A3:
G is one-to-one
and
A4:
rng F = rng G
and
A5:
len F >= 1
; g "**" F = g "**" G
A6:
len F = len G
by A2, A3, A4, FINSEQ_1:48;
set P = (F ") * G;
A7:
dom (F ") = rng F
by A2, FUNCT_1:33;
then A8: dom ((F ") * G) =
dom G
by A4, RELAT_1:27
.=
Seg (len F)
by A6, FINSEQ_1:def 3
.=
dom F
by FINSEQ_1:def 3
;
rng (F ") = dom F
by A2, FUNCT_1:33;
then A9:
rng ((F ") * G) c= dom F
by RELAT_1:26;
dom F = Seg (len F)
by FINSEQ_1:def 3;
then reconsider P = (F ") * G as Function of (dom F),(dom F) by A5, A8, A9, FUNCT_2:def 1, RELSET_1:4;
rng P =
rng (F ")
by A4, A7, RELAT_1:28
.=
dom F
by A2, FUNCT_1:33
;
then reconsider P = P as Permutation of (dom F) by A2, A3, FUNCT_2:57;
F * P =
(F * (F ")) * G
by RELAT_1:36
.=
(id (rng G)) * G
by A2, A4, FUNCT_1:39
.=
G
by RELAT_1:54
;
hence
g "**" F = g "**" G
by A1, A5, Th7; verum