let D be non empty set ; :: thesis: for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
F . k = g . (G . k),(H . k) ) holds
g "**" F = g . (g "**" G),(g "**" H)
let F, G, H be FinSequence of D; :: thesis: for g being BinOp of D st g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
F . k = g . (G . k),(H . k) ) holds
g "**" F = g . (g "**" G),(g "**" H)
let g be BinOp of D; :: thesis: ( g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
F . k = g . (G . k),(H . k) ) implies g "**" F = g . (g "**" G),(g "**" H) )
assume A1: ( g is associative & g is commutative & ( g is having_a_unity or len F >= 1 ) ) ; :: thesis: ( not len F = len G or not len F = len H or ex k being Element of NAT st
( k in dom F & not F . k = g . (G . k),(H . k) ) or g "**" F = g . (g "**" G),(g "**" H) )
A2: ( dom F = Seg (len F) & dom G = Seg (len G) & dom H = Seg (len H) ) by FINSEQ_1:def 3;
( len F = 0 or len F >= 1 ) by NAT_1:14;
hence ( not len F = len G or not len F = len H or ex k being Element of NAT st
( k in dom F & not F . k = g . (G . k),(H . k) ) or g "**" F = g . (g "**" G),(g "**" H) ) by A1, A2, Lm12, Lm13; :: thesis: verum