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
set P = (F " ) * G;
A6: len F = len G by A2, A3, A4, FINSEQ_1:65;
A7: dom (F " ) = rng F by A2, FUNCT_1:55;
then A8: dom ((F " ) * G) = dom G by A4, RELAT_1:46
.= Seg (len F) by A6, FINSEQ_1:def 3
.= dom F by FINSEQ_1:def 3 ;
rng (F " ) = dom F by A2, FUNCT_1:55;
then A9: rng ((F " ) * G) c= dom F by RELAT_1:45;
dom F = Seg (len F) by FINSEQ_1:def 3;
then dom F <> {} by A5;
then reconsider P = (F " ) * G as Function of (dom F),(dom F) by A8, A9, FUNCT_2:def 1, RELSET_1:11;
A10: rng P = rng (F " ) by A4, A7, RELAT_1:47
.= dom F by A2, FUNCT_1:55 ;
F " is one-to-one by A2;
then P is one-to-one by A3;
then reconsider P = P as Permutation of (dom F) by A10, FUNCT_2:83;
F * P = (F * (F " )) * G by RELAT_1:55
.= (id (rng G)) * G by A2, A4, FUNCT_1:61
.= G by RELAT_1:80 ;
hence g "**" F = g "**" G by A1, A5, Th8; :: thesis: verum