let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2 being 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 Nat st k1 < k2 & k1 in dom f holds
mid (f,k1,k2) = <*(f . k1)*> ^ (mid (f,(k1 + 1),k2))
let k1, k2 be 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:6;
hence k2 <= 1 + k1 by A1, XREAL_1:235; :: thesis: verum

end;

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

end;

end;

end;

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