let D be non empty set ; :: thesis: for F being XFinSequence of D
for b being BinOp of D
for n being Element of NAT 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; :: thesis: for b being BinOp of D
for n being Element of NAT 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; :: thesis: for n being Element of NAT 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 n be Element of NAT ; :: thesis: ( 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 )
; :: thesis: b . (b "**" (F | n)),(F . n) = b "**" (F | (n + 1))
defpred S1[ Element of 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)) );
A3:
S1[ 0 ]
proof
assume A4:
(
0 in dom F & (
b is
having_a_unity or
len (F | 0 ) >= 1 ) )
;
:: thesis: b . (b "**" (F | 0 )),(F . 0 ) = b "**" (F | (0 + 1))
then
dom F > 0
;
then
len F > 0
;
then
(
len F > 0 &
len F >= 1 )
by NAT_1:14;
then
(
len (F | 0 ) = 0 &
F . 0 in rng F &
rng F c= D &
len (F | 1) = 1 &
0 in 1 )
by A4, Lm2, FUNCT_1:def 5, NAT_1:45, ORDINAL1:def 8;
then
(
b is
having_a_unity &
b "**" (F | 0 ) = the_unity_wrt b &
F . 0 in D &
F | 1
= <%((F | 1) . 0 )%> &
F . 0 = (F | 1) . 0 )
by A4, AFINSQ_1:38, FUNCT_1:68, STIRL2_1:def 3;
then
(
b . (b "**" (F | 0 )),
(F . 0 ) = F . 0 &
b "**" (F | (0 + 1)) = F . 0 )
by SETWISEO:23, STIRL2_1:44;
hence
b . (b "**" (F | 0 )),
(F . 0 ) = b "**" (F | (0 + 1))
;
:: thesis: verum
end;
A5:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume
S1[
k]
;
:: thesis: S1[k + 1]
set k1 =
k + 1;
set Fk1 =
F | (k + 1);
set Fk2 =
F | ((k + 1) + 1);
assume A6:
(
k + 1
in dom F & (
b is
having_a_unity or
len (F | (k + 1)) >= 1 ) )
;
:: thesis: b . (b "**" (F | (k + 1))),(F . (k + 1)) = b "**" (F | ((k + 1) + 1))
then
k + 1
< dom F
by NAT_1:45;
then
(
k + 1
< dom F &
(k + 1) + 1
<= dom F &
dom F = len F )
by NAT_1:13;
then A7:
(
len (F | (k + 1)) = k + 1 &
len (F | ((k + 1) + 1)) = (k + 1) + 1 )
by Lm2;
then consider f1 being
Function of
NAT ,
D such that A8:
f1 . 0 = (F | (k + 1)) . 0
and A9:
for
n being
Element of
NAT st
n + 1
< len (F | (k + 1)) holds
f1 . (n + 1) = b . (f1 . n),
((F | (k + 1)) . (n + 1))
and A10:
b "**" (F | (k + 1)) = f1 . ((k + 1) - 1)
by A6, STIRL2_1:def 3;
(
b is
having_a_unity or
len (F | ((k + 1) + 1)) >= 1 )
by A6, A7, NAT_1:13;
then consider f2 being
Function of
NAT ,
D such that A11:
f2 . 0 = (F | ((k + 1) + 1)) . 0
and A12:
for
n being
Element of
NAT st
n + 1
< len (F | ((k + 1) + 1)) holds
f2 . (n + 1) = b . (f2 . n),
((F | ((k + 1) + 1)) . (n + 1))
and A13:
b "**" (F | ((k + 1) + 1)) = f2 . (((k + 1) + 1) - 1)
by A7, STIRL2_1:def 3;
defpred S2[
Element of
NAT ]
means ( $1
< k + 1 implies
f1 . $1
= f2 . $1 );
(
0 < k + 1 &
0 < (k + 1) + 1 &
dom F > 0 )
by A6;
then
(
0 in k + 1 &
0 in (k + 1) + 1 &
0 in dom F )
by NAT_1:45;
then
(
0 in (dom F) /\ (k + 1) &
0 in (dom F) /\ ((k + 1) + 1) )
by XBOOLE_0:def 4;
then
(
0 in dom (F | (k + 1)) &
0 in dom (F | ((k + 1) + 1)) )
by FUNCT_1:68;
then
(
(F | (k + 1)) . 0 = F . 0 &
(F | ((k + 1) + 1)) . 0 = F . 0 )
by FUNCT_1:68;
then A14:
S2[
0 ]
by A8, A11;
A15:
for
m being
Element of
NAT st
S2[
m] holds
S2[
m + 1]
proof
let m be
Element of
NAT ;
:: thesis: ( S2[m] implies S2[m + 1] )
assume A16:
S2[
m]
;
:: thesis: S2[m + 1]
set m1 =
m + 1;
assume A17:
m + 1
< k + 1
;
:: thesis: f1 . (m + 1) = f2 . (m + 1)
then
(
m + 1
< k + 1 &
m + 1
< (k + 1) + 1 &
k + 1
< dom F )
by A6, NAT_1:13, NAT_1:45;
then
(
m + 1
in k + 1 &
m + 1
in (k + 1) + 1 &
m + 1
< dom F )
by NAT_1:45, XXREAL_0:2;
then
(
m + 1
in k + 1 &
m + 1
in (k + 1) + 1 &
m + 1
in dom F )
by NAT_1:45;
then
(
m + 1
in (dom F) /\ (k + 1) &
m + 1
in (dom F) /\ ((k + 1) + 1) )
by XBOOLE_0:def 4;
then
(
m + 1
in dom (F | (k + 1)) &
m + 1
in dom (F | ((k + 1) + 1)) )
by FUNCT_1:68;
then
(
m + 1
< len (F | (k + 1)) &
m + 1
< len (F | ((k + 1) + 1)) &
f1 . m = f2 . m &
(F | (k + 1)) . (m + 1) = F . (m + 1) &
(F | ((k + 1) + 1)) . (m + 1) = F . (m + 1) )
by A7, A16, A17, FUNCT_1:68, NAT_1:13;
then
(
f1 . (m + 1) = b . (f1 . m),
((F | (k + 1)) . (m + 1)) &
f2 . (m + 1) = b . (f1 . m),
((F | (k + 1)) . (m + 1)) )
by A9, A12;
hence
f1 . (m + 1) = f2 . (m + 1)
;
:: thesis: verum
end;
A18:
for
m being
Element of
NAT holds
S2[
m]
from NAT_1:sch 1(A14, A15);
k + 1
< (k + 1) + 1
by NAT_1:13;
then
k + 1
in (k + 1) + 1
by NAT_1:45;
then
(
k < k + 1 &
k + 1
< (k + 1) + 1 &
k + 1
in (dom F) /\ ((k + 1) + 1) &
(dom F) /\ ((k + 1) + 1) = dom (F | ((k + 1) + 1)) )
by A6, FUNCT_1:68, NAT_1:13, XBOOLE_0:def 4;
then
(
f1 . k = f2 . k &
f2 . (k + 1) = b . (f2 . k),
((F | ((k + 1) + 1)) . (k + 1)) &
F . (k + 1) = (F | ((k + 1) + 1)) . (k + 1) )
by A7, A12, A18, FUNCT_1:68;
hence
b . (b "**" (F | (k + 1))),
(F . (k + 1)) = b "**" (F | ((k + 1) + 1))
by A10, A13;
:: thesis: verum
end;
A19:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A3, A5);
dom F > n
by A1, NAT_1:45;
then
len F > n
;
then
len (F | n) = n
by Lm2;
then
( n <> 0 implies len (F | n) >= 1 )
by NAT_1:14;
hence
b . (b "**" (F | n)),(F . n) = b "**" (F | (n + 1))
by A1, A2, A19; :: thesis: verum