let D be non empty set ; :: thesis: for F, G being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & 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 ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & 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: ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G )
( len F >= 1 or len F = 0 ) by NAT_1:14;
hence ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G ) by Lm9, Lm10; :: thesis: verum