let D be non empty set ; :: thesis: for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
let F, G be XFinSequence of D; :: thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
let b be BinOp of D; :: thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) )
defpred S₁[ XFinSequence of D] means for F being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len $1 >= 1 ) ) holds
b "**" (F ^ $1) = b . ((b "**" F),(b "**" $1));
A1: for G being XFinSequence of D
for d being Element of D st S₁[G] holds
S₁[G ^ <%d%>]

proof

let G be XFinSequence of D; :: thesis: for d being Element of D st S₁[G] holds
S₁[G ^ <%d%>]
let d be Element of D; :: thesis: ( S₁[G] implies S₁[G ^ <%d%>] )
assume A2: S₁[G] ; :: thesis: S₁[G ^ <%d%>]
let F be XFinSequence of D; :: thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) holds
b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))
let b be BinOp of D; :: thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) implies b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) )
assume that
A3: b is associative and
A4: ( b is having_a_unity or ( len F >= 1 & len (G ^ <%d%>) >= 1 ) ) ; :: thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))

now :: thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))

per cases ( len G <> 0 or len G = 0 ) ;

suppose A5: len G <> 0 ; :: thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))

then ( b is having_a_unity or ( len F >= 1 & len (F ^ G) = (len F) + (len G) & (len F) + (len G) > (len F) + zz ) ) by A4, AFINSQ_1:17, XREAL_1:8;
then b . ((b "**" (F ^ G)),d) = b "**" ((F ^ G) ^ <%d%>) by Th40;
then A6: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" (F ^ G)),d) by AFINSQ_1:27;
len G >= 1 by A5, NAT_1:14;
then b "**" (F ^ (G ^ <%d%>)) = b . ((b . ((b "**" F),(b "**" G))),d) by A2, A3, A4, A6
.= b . ((b "**" F),(b . ((b "**" G),d))) by A3
.= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A5, Th40 ;
hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; :: thesis: verum

end;

suppose len G = 0 ; :: thesis: b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>)))

then A7: G = {} ;
hence b "**" (F ^ (G ^ <%d%>)) = b "**" (F ^ ({} ^ <%d%>))
.= b "**" (F ^ <%d%>)
.= b . ((b "**" F),d) by A4, Th40
.= b . ((b "**" F),(b "**" ({} ^ <%d%>))) by Th37
.= b . ((b "**" F),(b "**" (G ^ <%d%>))) by A7 ;
:: thesis: verum

end;

end;

end;

hence b "**" (F ^ (G ^ <%d%>)) = b . ((b "**" F),(b "**" (G ^ <%d%>))) ; :: thesis: verum

end;

A8: S₁[ <%> D]

proof

let F be XFinSequence of D; :: thesis: for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) holds
b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D)))
let b be BinOp of D; :: thesis: ( b is associative & ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) implies b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D))) )
assume that
b is associative and
A9: ( b is having_a_unity or ( len F >= 1 & len (<%> D) >= 1 ) ) ; :: thesis: b "**" (F ^ (<%> D)) = b . ((b "**" F),(b "**" (<%> D)))
thus b "**" (F ^ (<%> D)) = b "**" (F ^ {})
.= b . ((b "**" F),(the_unity_wrt b)) by A9, SETWISEO:15
.= b . ((b "**" F),(b "**" (<%> D))) by A9, Def8, CARD_1:27 ; :: thesis: verum

end;

for G being XFinSequence of D holds S₁[G] from AFINSQ_2:sch 2(A8, A1);
hence ( b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies b "**" (F ^ G) = b . ((b "**" F),(b "**" G)) ) ; :: thesis: verum