let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum