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

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) + 0 ) ) by A4, AFINSQ_1:20, XREAL_1:10;
then b . (b "**" (F ^ G)),d = b "**" ((F ^ G) ^ <%d%>) by Th53;
then A6: b "**" (F ^ (G ^ <%d%>)) = b . (b "**" (F ^ G)),d by AFINSQ_1:30;
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, BINOP_1:def 3
.= b . (b "**" F),(b "**" (G ^ <%d%>)) by A5, Th53 ;
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%>) by AFINSQ_1:32
.= b . (b "**" F),d by A4, Th53
.= b . (b "**" F),(b "**" <%d%>) by Th49
.= b . (b "**" F),(b "**" (G ^ <%d%>)) by A7, AFINSQ_1:32 ;
:: 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 by AFINSQ_1:32
.= b . (b "**" F),(the_unity_wrt b) by A9, SETWISEO:23
.= b . (b "**" F),(b "**" (<%> D)) by A9, Def9, CARD_1:47 ; :: 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