let k, n be Nat; :: thesis: for g, h being complex-valued FinSequence holds ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))
let g, h be complex-valued FinSequence; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))
set gh = g ^ h;

per cases ( k > n or k <= n ) ;

suppose A1: k > n ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

then A2: ( ((g ^ h),k) +...+ ((g ^ h),n) = 0 & (g,k) +...+ (g,n) = 0 ) by Def1;

per cases ( ( k -' (len g) = n -' (len g) & k -' (len g) = 0 ) or ( k -' (len g) = n -' (len g) & k -' (len g) > 0 ) or n -' (len g) < k -' (len g) or n -' (len g) > k -' (len g) ) by XXREAL_0:1;

suppose ( k -' (len g) = n -' (len g) & k -' (len g) = 0 ) ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

then A3: (h,(k -' (len g))) +...+ (h,(n -' (len g))) = h . 0 by Th11;
not 0 in dom h by FINSEQ_3:25;
hence ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g)))) by A3, A2, FUNCT_1:def 2; :: thesis: verum

end;

suppose A4: ( k -' (len g) = n -' (len g) & k -' (len g) > 0 ) ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

then ( k -' (len g) = k - (len g) & n -' (len g) = n - (len g) ) by XREAL_0:def 2;
hence ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g)))) by A1, A4; :: thesis: verum

end;

suppose n -' (len g) < k -' (len g) ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

hence ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g)))) by Def1, A2; :: thesis: verum

end;

suppose A5: n -' (len g) > k -' (len g) ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

then ( n -' (len g) = n - (len g) & n - (len g) > 0 & 0 = (len g) - (len g) ) by XREAL_0:def 2;
then n > len g by XREAL_1:6;
hence ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g)))) by A5, A1, NAT_D:56; :: thesis: verum

end;

end;

end;

suppose A6: k <= n ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

set w = the complex-valued FinSequence;

per cases ( n <= len g or k > len g or ( n > len g & k <= len g ) ) ;

suppose A7: n <= len g ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

then k <= len g by A6, XXREAL_0:2;
then ( n - (len g) <= 0 & k - (len g) <= 0 ) by A7, XREAL_1:47;
then ( n -' (len g) = 0 & k -' (len g) = 0 ) by XREAL_0:def 2;
then A8: (h,(k -' (len g))) +...+ (h,(n -' (len g))) = h . 0 by Th11;
not 0 in dom h by FINSEQ_3:25;
then (h,(k -' (len g))) +...+ (h,(n -' (len g))) = 0 by FUNCT_1:def 2, A8;
hence ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g)))) by A7, Lm2, A6; :: thesis: verum

end;

suppose A9: k > len g ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

then (g,k) +...+ (g,n) = 0 by Th15;
hence ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g)))) by Lm3, A9, A6; :: thesis: verum

end;

suppose A10: ( n > len g & k <= len g ) ; :: thesis: ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))

then A11: ((g ^ h),k) +...+ ((g ^ h),(len g)) = (g,k) +...+ (g,(len g)) by Lm2
.= (g,k) +...+ (g,n) by Th16, A10 ;
k - (len g) <= (len g) - (len g) by A10, XREAL_1:7;
then A12: k -' (len g) = 0 by XREAL_0:def 2;
A13: ((len g) + 1) -' (len g) = ((len g) + 1) - (len g) by NAT_D:37;
( (len g) + 1 > len g & n >= (len g) + 1 ) by A10, NAT_1:13;
then ((g ^ h),((len g) + 1)) +...+ ((g ^ h),n) = (h,(((len g) + 1) -' (len g))) +...+ (h,(n -' (len g))) by Lm3
.= (h,(k -' (len g))) +...+ (h,(n -' (len g))) by A13, Th17, A12 ;
hence ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g)))) by A10, Th14, A11; :: thesis: verum

end;

end;

end;

end;