let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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:23;
hence ( not len p = len q or F . (F "**" p),(F "**" q) = F "**" (F .: p,q) ) by A1, Th43; :: thesis: verum