let n be Nat; for D being non empty set
for F being XFinSequence of D
for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
let D be non empty set ; for F being XFinSequence of D
for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
let F be XFinSequence of D; for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
let b be BinOp of D; ( n in dom F & ( b is having_a_unity or n <> 0 ) implies b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1)) )
assume that
A1:
n in dom F
and
A2:
( b is having_a_unity or n <> 0 )
; b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
len F > n
by A1, AFINSQ_1:86;
then A3:
len (F | n) = n
by AFINSQ_1:54;
defpred S1[ Nat] means ( $1 in dom F & ( b is having_a_unity or len (F | $1) >= 1 ) implies b . ((b "**" (F | $1)),(F . $1)) = b "**" (F | ($1 + 1)) );
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
set Fk1 =
F | (k + 1);
set Fk2 =
F | ((k + 1) + 1);
assume that A5:
k + 1
in dom F
and A6:
(
b is
having_a_unity or
len (F | (k + 1)) >= 1 )
;
b . ((b "**" (F | (k + 1))),(F . (k + 1))) = b "**" (F | ((k + 1) + 1))
0 < len F
by A5;
then A7:
0 in dom F
by AFINSQ_1:86;
0 in Segm (k + 1)
by NAT_1:44;
then
0 in (dom F) /\ (k + 1)
by A7, XBOOLE_0:def 4;
then
0 in dom (F | (k + 1))
by RELAT_1:61;
then A8:
(F | (k + 1)) . 0 = F . 0
by FUNCT_1:47;
A9:
k < k + 1
by NAT_1:13;
k + 1
< (k + 1) + 1
by NAT_1:13;
then
k + 1
in Segm ((k + 1) + 1)
by NAT_1:44;
then A10:
k + 1
in (dom F) /\ ((k + 1) + 1)
by A5, XBOOLE_0:def 4;
A12:
k + 1
< len F
by A5, AFINSQ_1:86;
then A13:
len (F | (k + 1)) = k + 1
by AFINSQ_1:54;
then consider f1 being
sequence of
D such that A14:
f1 . 0 = (F | (k + 1)) . 0
and A15:
for
n being
Nat st
n + 1
< len (F | (k + 1)) holds
f1 . (n + 1) = b . (
(f1 . n),
((F | (k + 1)) . (n + 1)))
and A16:
b "**" (F | (k + 1)) = f1 . ((k + 1) - 1)
by A6, Def8;
(k + 1) + 1
<= dom F
by A12, NAT_1:13;
then A17:
len (F | ((k + 1) + 1)) = (k + 1) + 1
by AFINSQ_1:54;
then
(
b is
having_a_unity or
len (F | ((k + 1) + 1)) >= 1 )
by A6, A13, NAT_1:13;
then consider f2 being
sequence of
D such that A18:
f2 . 0 = (F | ((k + 1) + 1)) . 0
and A19:
for
n being
Nat st
n + 1
< len (F | ((k + 1) + 1)) holds
f2 . (n + 1) = b . (
(f2 . n),
((F | ((k + 1) + 1)) . (n + 1)))
and A20:
b "**" (F | ((k + 1) + 1)) = f2 . (((k + 1) + 1) - 1)
by A17, Def8;
defpred S2[
Nat]
means ( $1
< k + 1 implies
f1 . $1
= f2 . $1 );
A21:
for
m being
Nat st
S2[
m] holds
S2[
m + 1]
proof
let m be
Nat;
( S2[m] implies S2[m + 1] )
assume A22:
S2[
m]
;
S2[m + 1]
set m1 =
m + 1;
assume A23:
m + 1
< k + 1
;
f1 . (m + 1) = f2 . (m + 1)
k + 1
< len F
by A5, AFINSQ_1:86;
then
m + 1
< len F
by A23, XXREAL_0:2;
then A24:
m + 1
in dom F
by AFINSQ_1:86;
m + 1
< (k + 1) + 1
by A23, NAT_1:13;
then
m + 1
in Segm ((k + 1) + 1)
by NAT_1:44;
then
m + 1
in (dom F) /\ (Segm ((k + 1) + 1))
by A24, XBOOLE_0:def 4;
then
m + 1
in dom (F | ((k + 1) + 1))
by RELAT_1:61;
then A25:
(F | ((k + 1) + 1)) . (m + 1) = F . (m + 1)
by FUNCT_1:47;
m + 1
in Segm (k + 1)
by A23, NAT_1:44;
then
m + 1
in (dom F) /\ (Segm (k + 1))
by A24, XBOOLE_0:def 4;
then
m + 1
in dom (F | (k + 1))
by RELAT_1:61;
then A26:
(F | (k + 1)) . (m + 1) = F . (m + 1)
by FUNCT_1:47;
m + 1
< len (F | ((k + 1) + 1))
by A17, A23, NAT_1:13;
then
f2 . (m + 1) = b . (
(f1 . m),
((F | (k + 1)) . (m + 1)))
by A19, A22, A23, A26, A25, NAT_1:13;
hence
f1 . (m + 1) = f2 . (m + 1)
by A13, A15, A23;
verum
end;
0 in Segm ((k + 1) + 1)
by NAT_1:44;
then
0 in (dom F) /\ ((k + 1) + 1)
by A7, XBOOLE_0:def 4;
then
0 in dom (F | ((k + 1) + 1))
by RELAT_1:61;
then A27:
S2[
0 ]
by A14, A18, A8, FUNCT_1:47;
for
m being
Nat holds
S2[
m]
from NAT_1:sch 2(A27, A21);
then A28:
(
(dom F) /\ ((k + 1) + 1) = dom (F | ((k + 1) + 1)) &
f1 . k = f2 . k )
by A9, RELAT_1:61;
k + 1
< (k + 1) + 1
by NAT_1:13;
then
f2 . (k + 1) = b . (
(f2 . k),
((F | ((k + 1) + 1)) . (k + 1)))
by A17, A19;
hence
b . (
(b "**" (F | (k + 1))),
(F . (k + 1)))
= b "**" (F | ((k + 1) + 1))
by A16, A20, A10, A28, FUNCT_1:47;
verum
end;
A29:
S1[ 0 ]
proof
assume that A30:
0 in dom F
and A31:
(
b is
having_a_unity or
len (F | 0) >= 1 )
;
b . ((b "**" (F | 0)),(F . 0)) = b "**" (F | (0 + 1))
A32:
F . 0 in rng F
by A30, FUNCT_1:def 3;
len F > 0
by A30;
then A33:
len (F | 1) = 1
by AFINSQ_1:54, NAT_1:14;
then A34:
F | 1
= <%((F | 1) . 0)%>
by AFINSQ_1:34;
0 in Segm 1
by NAT_1:44;
then A35:
F . 0 = (F | 1) . 0
by A33, FUNCT_1:47;
len (F | 0) = 0
;
then
b "**" (F | 0) = the_unity_wrt b
by A31, Def8;
then
b . (
(b "**" (F | 0)),
(F . 0))
= F . 0
by A31, A32, SETWISEO:15;
hence
b . (
(b "**" (F | 0)),
(F . 0))
= b "**" (F | (0 + 1))
by A32, A34, A35, Th37;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A29, A4);
hence
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
by A1, A2, A3, NAT_1:14; verum