let D be non empty set ; :: thesis: for F, G being XFinSequence of
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 ; :: 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 ] means for F being XFinSequence of
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: S₁[ <%> D]

proof

let F be XFinSequence of ; :: 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 A2: ( b is associative & ( 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 A2, SETWISEO:23
.= b . (b "**" F),(b "**" (<%> D)) by A2, Def3, CARD_1:47 ; :: thesis: verum

end;

A3: for G being XFinSequence of
for d being Element of D st S₁[G] holds
S₁[G ^ <%d%>]

proof

let G be XFinSequence of ; :: 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 A4: S₁[G] ; :: thesis: S₁[G ^ <%d%>]
let F be XFinSequence of ; :: 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 A5: ( b is associative & ( 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 A6: len G <> 0 ; :: thesis: b "**" (F ^ (G ^ <%d%>)) = b . (b "**" F),(b "**" (G ^ <%d%>))

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

proof

( b is having_a_unity or ( len F >= 1 & len (F ^ G) = (len F) + (len G) & (len F) + (len G) > (len F) + 0 ) ) by A5, A6, AFINSQ_1:20, XREAL_1:10;
then b . (b "**" (F ^ G)),d = b "**" ((F ^ G) ^ <%d%>) by Th45;
hence b "**" (F ^ (G ^ <%d%>)) = b . (b "**" (F ^ G)),d by AFINSQ_1:30; :: thesis: verum

end;

len G >= 1 by A6, NAT_1:14;
then b "**" (F ^ (G ^ <%d%>)) = b . (b . (b "**" F),(b "**" G)),d by A4, A5, A7
.= b . (b "**" F),(b . (b "**" G),d) by A5, BINOP_1:def 3
.= b . (b "**" F),(b "**" (G ^ <%d%>)) by A6, Th45 ;
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 A9: G = {} ;
hence b "**" (F ^ (G ^ <%d%>)) = b "**" (F ^ <%d%>) by AFINSQ_1:32
.= b . (b "**" F),d by A5, Th45
.= b . (b "**" F),(b "**" <%d%>) by Th44
.= b . (b "**" F),(b "**" (G ^ <%d%>)) by A9, AFINSQ_1:32 ;
:: thesis: verum

end;

end;

end;

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

end;

for G being XFinSequence of holds S₁[G] from STIRL2_1:sch 5(A1, A3);
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