let D be non empty set ; :: thesis: for F being XFinSequence of D
for b being BinOp of D
for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
let F be XFinSequence of D; :: thesis: for b being BinOp of D
for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
let b be BinOp of D; :: thesis: for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
let d be Element of D; :: thesis: ( ( b is having_a_unity or len F > 0 ) implies b "**" (F ^ <%d%>) = b . ((b "**" F),d) )
assume A1: ( b is having_a_unity or len F > 0 ) ; :: thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d)

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

per cases ( len F < zz + 1 or len F >= 1 ) ;

suppose A2: len F < zz + 1 ; :: thesis: b "**" (F ^ <%d%>) = b . ((b "**" F),d)

then A3: F = {} by NAT_1:13;
A4: b "**" (F ^ <%d%>) = d by Th37, A3;
len F = 0 by A2, NAT_1:13;
then b "**" F = the_unity_wrt b by A1, Def8;
hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) by A1, A2, A4, NAT_1:13, SETWISEO:15; :: thesis: verum

end;

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

set G = F ^ <%d%>;
reconsider lenF1 = (len F) - 1 as Element of NAT by A5, NAT_1:21;
A6: (F ^ <%d%>) . (len F) = d by AFINSQ_1:36;
A7: len (F ^ <%d%>) = (len F) + (len <%d%>) by AFINSQ_1:17
.= (len F) + 1 by AFINSQ_1:33 ;
then 1 <= len (F ^ <%d%>) by NAT_1:12;
then consider f1 being sequence of D such that
A8: f1 . 0 = (F ^ <%d%>) . 0 and
A9: for n being Nat st n + 1 < len (F ^ <%d%>) holds
f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) and
A10: b "**" (F ^ <%d%>) = f1 . ((len (F ^ <%d%>)) - 1) by Def8;
consider f being sequence of D such that
A11: f . 0 = F . 0 and
A12: for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) and
A13: b "**" F = f . ((len F) - 1) by A5, Def8;
defpred S₁[ Nat] means ( $1 + 1 < len (F ^ <%d%>) implies f . $1 = f1 . $1 );
A14: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A15: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A16: (n + 1) + 1 < len (F ^ <%d%>) ; :: thesis: f . (n + 1) = f1 . (n + 1)
then A17: f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) by A9, NAT_1:13;
A18: ((n + 1) + 1) + (- 1) < ((len F) + 1) + (- 1) by A7, A16, XREAL_1:8;
then A19: n + 1 in len F by AFINSQ_1:86;
f . (n + 1) = b . ((f . n),(F . (n + 1))) by A12, A18;
hence f . (n + 1) = f1 . (n + 1) by A15, A16, A17, A19, AFINSQ_1:def 3, NAT_1:13; :: thesis: verum

end;

0 in len F by A5, AFINSQ_1:86;
then A20: S₁[ 0 ] by A11, A8, AFINSQ_1:def 3;
A21: for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A14);
A22: lenF1 + 1 < len (F ^ <%d%>) by A7, NAT_1:13;
then b "**" (F ^ <%d%>) = b . ((f1 . lenF1),((F ^ <%d%>) . (lenF1 + 1))) by A7, A9, A10;
hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) by A13, A21, A22, A6; :: thesis: verum

end;

end;

end;

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