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

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

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

then F = {} by NAT_1:13;
then F ^ <%d%> = <%d%> by AFINSQ_1:32;
then A3: b "**" (F ^ <%d%>) = d by Th49;
len F = 0 by A2, NAT_1:13;
then b "**" F = the_unity_wrt b by A1, Def9;
hence b "**" (F ^ <%d%>) = b . ((b "**" F),d) by A1, A2, A3, NAT_1:13, SETWISEO:23; :: thesis: verum

end;

suppose A4: 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 A4, NAT_1:21;
A5: (F ^ <%d%>) . (len F) = d by AFINSQ_1:40;
A6: len (F ^ <%d%>) = (len F) + (len <%d%>) by AFINSQ_1:20
.= (len F) + 1 by AFINSQ_1:36 ;
then 1 <= len (F ^ <%d%>) by NAT_1:12;
then consider f1 being Function of NAT,D such that
A7: f1 . 0 = (F ^ <%d%>) . 0 and
A8: for n being Nat st n + 1 < len (F ^ <%d%>) holds
f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) and
A9: b "**" (F ^ <%d%>) = f1 . ((len (F ^ <%d%>)) - 1) by Def9;
consider f being Function of NAT,D such that
A10: f . 0 = F . 0 and
A11: for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) and
A12: b "**" F = f . ((len F) - 1) by A4, Def9;
defpred S₁[ Nat] means ( $1 + 1 < len (F ^ <%d%>) implies f . $1 = f1 . $1 );
A13: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A14: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
assume A15: (n + 1) + 1 < len (F ^ <%d%>) ; :: thesis: f . (n + 1) = f1 . (n + 1)
then n + 1 < len (F ^ <%d%>) by NAT_1:13;
then A16: f1 . (n + 1) = b . ((f1 . n),((F ^ <%d%>) . (n + 1))) by A8;
A17: ((n + 1) + 1) + (- 1) < ((len F) + 1) + (- 1) by A6, A15, XREAL_1:10;
then A18: n + 1 in len F by NAT_1:45;
f . (n + 1) = b . ((f . n),(F . (n + 1))) by A11, A17;
hence f . (n + 1) = f1 . (n + 1) by A14, A15, A16, A18, AFINSQ_1:def 4, NAT_1:13; :: thesis: verum

end;

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

end;

end;

end;

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