let h1, h2 be XFinSequence of REAL ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

per cases ( len (h1 ^ h2) > 0 or len (h1 ^ h2) <= 0 ) ;

suppose A0: len (h1 ^ h2) > 0 ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

per cases ( len h1 > 0 or len h1 <= 0 ) ;

suppose A71: len h1 > 0 ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

consider g1 being XFinSequence of REAL such that
A1: ( len h1 = len g1 & h1 . 0 = g1 . 0 & ( for i being Nat st i + 1 < len h1 holds
g1 . (i + 1) = (g1 . i) + (h1 . (i + 1)) ) & Sum h1 = g1 . ((len h1) -' 1) ) by AC300;

per cases ( len h2 > 0 or len h2 <= 0 ) ;

suppose A72: len h2 > 0 ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

consider g2 being XFinSequence of REAL such that
A2: ( len h2 = len g2 & h2 . 0 = g2 . 0 & ( for i being Nat st i + 1 < len h2 holds
g2 . (i + 1) = (g2 . i) + (h2 . (i + 1)) ) & Sum h2 = g2 . ((len h2) -' 1) ) by AC300;
set a = g1 . ((len g1) -' 1);
set g2b = g2 + (g1 . ((len g1) -' 1));
E4b: ( len (g2 + (g1 . ((len g1) -' 1))) = len g2 & ( for i being Nat st i < len g2 holds
(g2 + (g1 . ((len g1) -' 1))) . i = (g2 . i) + (g1 . ((len g1) -' 1)) ) ) by AC500;
set g4 = g1 ^ (g2 + (g1 . ((len g1) -' 1)));
E10: len (h1 ^ h2) = (len g1) + (len g2) by A1, A2, AFINSQ_1:20
.= len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) by E4b, AFINSQ_1:20 ;
E34: (h1 ^ h2) . 0 = h1 . 0 by AE359, A71
.= (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . 0 by AE359, A1, A71 ;
E93: len (h1 ^ h2) = (len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) by A1, E4b, A2, AFINSQ_1:20;
E94: len (h1 ^ h2) = (len h1) + (len h2) by AFINSQ_1:20
.= len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) by A1, E4b, A2, AFINSQ_1:20 ;
E95: len g1 < len (h1 ^ h2) by E93, E4b, A2, A72, XREAL_1:31;
E35: for i being Nat st i + 1 < len (h1 ^ h2) holds
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1))

proof

let i be Nat; :: thesis: ( i + 1 < len (h1 ^ h2) implies (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1)) )
assume G1: i + 1 < len (h1 ^ h2) ; :: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1))
reconsider i0 = i as Element of NAT by ORDINAL1:def 13;

per cases ( i + 1 < len g1 or i + 1 >= len g1 ) ;

suppose H0: i + 1 < len g1 ; :: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1))

then G2: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = g1 . (i + 1) by AE359;
i < i + 1 by XREAL_1:31;
then i < len g1 by H0, XXREAL_0:2;
then G4: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = g1 . i by AE359;
(h1 ^ h2) . (i + 1) = h1 . (i + 1) by AE359, A1, H0;
hence (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1)) by G2, G4, A1, H0; :: thesis: verum

end;

suppose H0: i + 1 >= len g1 ; :: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1))

per cases ( i + 1 > len g1 or i + 1 = len g1 ) by H0, XXREAL_0:1;

suppose J0: i + 1 > len g1 ; :: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1))

then i >= len g1 by NAT_1:13;
then i -' (len g1) = i - (len g1) by XREAL_1:235;
then reconsider i1 = i - (len g1) as Element of NAT ;
(i + 1) - (len g1) < (len (h1 ^ h2)) - (len g1) by G1, XREAL_1:11;
then G1en: i1 + 1 < ((len g1) + (len (g2 + (g1 . ((len g1) -' 1))))) - (len g1) by A1, E4b, A2, AFINSQ_1:20;
i1 < i1 + 1 by XREAL_1:31;
then G3: i1 < len (g2 + (g1 . ((len g1) -' 1))) by G1en, XXREAL_0:2;
G5p: i1 + 1 = (i0 + 1) - (len h1) by A1;
( len g1 <= i0 & i0 < len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) ) by J0, E94, G1, NAT_1:13;
then G4: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i0 = (g2 + (g1 . ((len g1) -' 1))) . i1 by AFINSQ_1:22;
G5: (h1 ^ h2) . (i0 + 1) = h2 . (i1 + 1) by G5p, H0, G1, AFINSQ_1:22;
G51: (g2 + (g1 . ((len g1) -' 1))) . i1 = (g2 . i1) + (g1 . ((len g1) -' 1)) by E4b, G3;
G52: (g2 + (g1 . ((len g1) -' 1))) . (i1 + 1) = (g2 . (i1 + 1)) + (g1 . ((len g1) -' 1)) by E4b, G1en;
g2 . (i1 + 1) = (g2 . i1) + (h2 . (i1 + 1)) by A2, E4b, G1en;
hence (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1)) by G5p, H0, E94, G1, G4, G5, G51, G52, AFINSQ_1:22; :: thesis: verum

end;

suppose H0: i + 1 = len g1 ; :: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1))

then H8: i = (len g1) -' 1 by NAT_D:34;
G2r: 0 in dom (g2 + (g1 . ((len g1) -' 1))) by A72, A2, E4b, NAT_1:45;
G2: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len g1) + 0 ) by H0
.= (g2 + (g1 . ((len g1) -' 1))) . 0 by G2r, AFINSQ_1:def 4 ;
0 + 1 <= len g1 by A71, A1, NAT_1:13;
then G34: (len g1) -' 1 = (len g1) - 1 by XREAL_1:235;
len g1 < (len g1) + 1 by XREAL_1:31;
then (len g1) - 1 < len g1 by XREAL_1:21;
then (len g1) -' 1 in dom g1 by G34, NAT_1:45;
then G4: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = g1 . ((len g1) -' 1) by H8, AFINSQ_1:def 4;
G65: (len g1) - (len h1) = 0 by A1;
h2 . 0 = (h1 ^ h2) . (i + 1) by H0, G65, E95, AFINSQ_1:22;
hence (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1)) by G2, G4, AC500, A72, A2; :: thesis: verum

end;

end;

end;

end;

end;

len (h1 ^ h2) >= 0 + 1 by A0, NAT_1:13;
then R50: (len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) >= 1 by A1, A2, E4b, AFINSQ_1:20;
R4n: len (g2 + (g1 . ((len g1) -' 1))) >= 0 + 1 by A2, E4b, A72, NAT_1:13;
then R4: (len (g2 + (g1 . ((len g1) -' 1)))) -' 1 = (len (g2 + (g1 . ((len g1) -' 1)))) - 1 by XREAL_1:235;
R2: ((len g1) + (len (g2 + (g1 . ((len g1) -' 1))))) -' 1 = ((len g1) + (len (g2 + (g1 . ((len g1) -' 1))))) - 1 by R50, XREAL_1:235
.= (len g1) + ((len (g2 + (g1 . ((len g1) -' 1)))) - 1)
.= (len g1) + ((len (g2 + (g1 . ((len g1) -' 1)))) -' 1) by R4n, XREAL_1:235 ;
R7n: (len (g2 + (g1 . ((len g1) -' 1)))) - 1 < len (g2 + (g1 . ((len g1) -' 1))) by XREAL_1:46;
R3: (len (g2 + (g1 . ((len g1) -' 1)))) -' 1 in dom (g2 + (g1 . ((len g1) -' 1))) by R4, R7n, NAT_1:45;
R5: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len (h1 ^ h2)) -' 1) = (g2 + (g1 . ((len g1) -' 1))) . ((len (g2 + (g1 . ((len g1) -' 1)))) -' 1) by E93, R2, R3, AFINSQ_1:def 4;
(g1 . ((len g1) -' 1)) + (g2 . ((len h2) -' 1)) = (g2 + (g1 . ((len g1) -' 1))) . ((len h2) -' 1) by E4b, A2, R4, XREAL_1:46;
hence Sum (h1 ^ h2) = (Sum h1) + (Sum h2) by AC300, E10, E34, E35, A1, A2, R5, E4b; :: thesis: verum

end;

suppose len h2 <= 0 ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

then A73: h2 = {} ;
then Sum h2 = 0 ;
hence Sum (h1 ^ h2) = (Sum h1) + (Sum h2) by A73, AFINSQ_1:32; :: thesis: verum

end;

end;

end;

suppose len h1 <= 0 ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

then A73: h1 = {} ;
then Sum h1 = 0 ;
hence Sum (h1 ^ h2) = (Sum h1) + (Sum h2) by A73, AFINSQ_1:32; :: thesis: verum

end;

end;

end;

suppose A0: len (h1 ^ h2) <= 0 ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

then A80n: h1 ^ h2 = {} ;
len h1 <= (len h1) + (len h2) by NAT_1:11;
then h1 = {} by A0, AFINSQ_1:20;
then A81: Sum h1 = 0 ;
len h2 <= (len h1) + (len h2) by NAT_1:11;
then len h2 = 0 by A0, AFINSQ_1:20;
hence Sum (h1 ^ h2) = (Sum h1) + (Sum h2) by A80n, A81, AFINSQ_1:18; :: thesis: verum

end;

end;