let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: 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))
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; :: 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 that
A5: k + 1 in dom F and
A6: ( 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))
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; :: thesis: ( S2[m] implies S2[m + 1] )
assume A22: S2[m] ; :: thesis: S2[m + 1]
set m1 = m + 1;
assume A23: m + 1 < k + 1 ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: verum