let D be non empty set ; :: thesis: for F, G being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
let F, G be FinSequence of D; :: thesis: for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
let g be BinOp of D; :: thesis: ( len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G )
assume that
A1: ( len F = 0 & g is having_a_unity ) and
A2: ( F is one-to-one & G is one-to-one & rng F = rng G ) ; :: thesis: g "**" F = g "**" G
( len G = len F & g "**" F = the_unity_wrt g ) by A1, A2, Def1, FINSEQ_1:48;
hence g "**" F = g "**" G by A1, Def1; :: thesis: verum