let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2 being Element of NAT st k1 < k2 & k1 in dom f holds
mid f,k1,k2 = <*(f . k1)*> ^ (mid f,(k1 + 1),k2)
let f be FinSequence of D; :: thesis: for k1, k2 being Element of NAT st k1 < k2 & k1 in dom f holds
mid f,k1,k2 = <*(f . k1)*> ^ (mid f,(k1 + 1),k2)
let k1, k2 be Element of NAT ; :: thesis: ( k1 < k2 & k1 in dom f implies mid f,k1,k2 = <*(f . k1)*> ^ (mid f,(k1 + 1),k2) )
assume A1: k1 < k2 ; :: thesis: ( not k1 in dom f or mid f,k1,k2 = <*(f . k1)*> ^ (mid f,(k1 + 1),k2) )
then A2: k1 + 1 <= k2 by NAT_1:13;
A3: 1 <= k2 -' k1

proof

per cases ( k1 + 1 = k2 or k1 + 1 < k2 ) by A2, XXREAL_0:1;

suppose k1 + 1 = k2 ; :: thesis: 1 <= k2 -' k1

hence 1 <= k2 -' k1 by NAT_D:34; :: thesis: verum

end;

suppose A4: k1 + 1 < k2 ; :: thesis: 1 <= k2 -' k1

( k2 -' k1 <= 1 implies k2 <= 1 + k1 )

proof

assume k2 -' k1 <= 1 ; :: thesis: k2 <= 1 + k1
then (k2 -' k1) + k1 <= 1 + k1 by XREAL_1:8;
hence k2 <= 1 + k1 by A1, XREAL_1:237; :: thesis: verum

end;

hence 1 <= k2 -' k1 by A4; :: thesis: verum

end;

end;

end;

assume A5: k1 in dom f ; :: thesis: mid f,k1,k2 = <*(f . k1)*> ^ (mid f,(k1 + 1),k2)
then A6: f . k1 = f /. k1 by PARTFUN1:def 8;
k2 -' k1 = k2 - k1 by A3, NAT_D:39;
then A7: (k2 -' k1) -' 1 = (k2 - k1) - 1 by A3, XREAL_1:235
.= k2 - (k1 + 1)
.= k2 -' (k1 + 1) by A2, XREAL_1:235 ;
1 <= k1 by A5, FINSEQ_3:27;
then (k1 -' 1) + 1 = k1 by XREAL_1:237;
then f /^ (k1 -' 1) = <*(f /. k1)*> ^ (f /^ k1) by A5, FINSEQ_5:34;
hence mid f,k1,k2 = (<*(f /. k1)*> ^ (f /^ k1)) | ((k2 -' k1) + 1) by A1, Def1
.= <*(f . k1)*> ^ ((f /^ k1) | (k2 -' k1)) by A6, Th55
.= <*(f . k1)*> ^ ((f /^ k1) | ((k2 -' (k1 + 1)) + 1)) by A3, A7, XREAL_1:237
.= <*(f . k1)*> ^ ((f /^ ((k1 + 1) -' 1)) | ((k2 -' (k1 + 1)) + 1)) by NAT_D:34
.= <*(f . k1)*> ^ (mid f,(k1 + 1),k2) by A2, Def1 ;
:: thesis: verum