let D be non empty set ; for F being BinOp of D
for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & len p = len q holds
F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q))
let F be BinOp of D; for p, q being FinSequence of D st F is commutative & F is associative & F is having_a_unity & len p = len q holds
F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q))
let p, q be FinSequence of D; ( F is commutative & F is associative & F is having_a_unity & len p = len q implies F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q)) )
set e = the_unity_wrt F;
assume A1:
( F is commutative & F is associative & F is having_a_unity )
; ( not len p = len q or F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q)) )
then
( F . ((the_unity_wrt F),(the_unity_wrt F)) = the_unity_wrt F & ( for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4))) ) )
by Lm3, SETWISEO:15;
hence
( not len p = len q or F . ((F "**" p),(F "**" q)) = F "**" (F .: (p,q)) )
by A1, Th32; verum