let D be non empty set ; 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; 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; 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; ( ( 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 )
; b "**" (F ^ <%d%>) = b . ((b "**" F),d)
now b "**" (F ^ <%d%>) = b . ((b "**" F),d)per cases
( len F < zz + 1 or len F >= 1 )
;
suppose A5:
len F >= 1
;
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 S1[
Nat]
means ( $1
+ 1
< len (F ^ <%d%>) implies
f . $1
= f1 . $1 );
A14:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A15:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
assume A16:
(n + 1) + 1
< len (F ^ <%d%>)
;
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;
verum
end;
0 in len F
by A5, AFINSQ_1:86;
then A20:
S1[
0 ]
by A11, A8, AFINSQ_1:def 3;
A21:
for
n being
Nat holds
S1[
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;
verum end;
hence
b "**" (F ^ <%d%>) = b . ((b "**" F),d)
; verum