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 by A2, FINSEQ_1:65;
then ( g "**" F = the_unity_wrt g & g "**" G = the_unity_wrt g ) by A1, Def1;
hence g "**" F = g "**" G ; :: thesis: verum