let D be non empty set ; :: thesis: for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G
let F, G be FinSequence of D; :: thesis: for g being BinOp of D
for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G
let g be BinOp of D; :: thesis: for P being Permutation of (dom F) st g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P holds
g "**" F = g "**" G
let P be Permutation of (dom F); :: thesis: ( g is commutative & g is associative & ( g is having_a_unity or len F >= 1 ) & G = F * P implies g "**" F = g "**" G )
assume that
A1: ( g is commutative & g is associative ) and
A2: ( g is having_a_unity or len F >= 1 ) ; :: thesis: ( not G = F * P or g "**" F = g "**" G )
assume A3: G = F * P ; :: thesis: g "**" F = g "**" G
now :: thesis: g "**" F = g "**" G
per cases ( len F = 0 or len F <> 0 ) ;
suppose len F = 0 ; :: thesis: g "**" F = g "**" G
hence g "**" F = g "**" G by A2, A3, Lm8; :: thesis: verum
end;
suppose A4: len F <> 0 ; :: thesis: g "**" F = g "**" G
( len F = len G & ( for i being Nat st i in dom G holds
G . i = F . (P . i) ) ) by A3, FINSEQ_2:44, FUNCT_1:12;
hence g "**" F = g "**" G by A1, A4, Lm7, NAT_1:14; :: thesis: verum
end;
end;
end;
hence g "**" F = g "**" G ; :: thesis: verum