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 having_a_unity & len F = 0 & 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 having_a_unity & len F = 0 & 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 having_a_unity & len F = 0 & G = F * P holds
g "**" F = g "**" G
let P be Permutation of (dom F); :: thesis: ( g is having_a_unity & len F = 0 & G = F * P implies g "**" F = g "**" G )
assume that
A1: g is having_a_unity and
A2: len F = 0 ; :: thesis: ( not G = F * P or g "**" F = g "**" G )
assume A3: G = F * P ; :: thesis: g "**" F = g "**" G
F = {} by A2;
then G = {} by A3, RELAT_1:39;
then A4: len G = 0 ;
thus g "**" F = the_unity_wrt g by A1, A2, Def1
.= g "**" G by A1, A4, Def1 ; :: thesis: verum