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 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 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 Nat st k in dom F holds
F . k = g . ((G . k),(H . k)) ) implies g "**" F = g . ((g "**" G),(g "**" H)) )
A1: ( dom F = Seg (len F) & dom G = Seg (len G) ) by FINSEQ_1:def 3;
A2: ( len F = 0 or len F >= 1 ) by NAT_1:14;
assume ( 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 Nat st
( k in dom F & not F . k = g . ((G . k),(H . k)) ) or g "**" F = g . ((g "**" G),(g "**" H)) )
hence ( not len F = len G or not len F = len H or ex k being 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