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 A1: len (h1 ^ h2) > 0 ; :: thesis: Sum (h1 ^ h2) = (Sum h1) + (Sum h2)

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

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

consider g1 being XFinSequence of REAL such that
A3: len h1 = len g1 and
A4: h1 . 0 = g1 . 0 and
A5: for i being Nat st i + 1 < len h1 holds
g1 . (i + 1) = (g1 . i) + (h1 . (i + 1)) and
A6: Sum h1 = g1 . ((len h1) -' 1) by Def4;

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

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

set a = g1 . ((len g1) -' 1);
consider g2 being XFinSequence of REAL such that
A8: len h2 = len g2 and
A9: h2 . 0 = g2 . 0 and
A10: for i being Nat st i + 1 < len h2 holds
g2 . (i + 1) = (g2 . i) + (h2 . (i + 1)) and
A11: Sum h2 = g2 . ((len h2) -' 1) by Def4;
set g2b = g2 + (g1 . ((len g1) -' 1));
A12: len (g2 + (g1 . ((len g1) -' 1))) = len g2 by Th6;
then A13: len (g2 + (g1 . ((len g1) -' 1))) >= 0 + 1 by A7, A8, NAT_1:13;
then A14: (len (g2 + (g1 . ((len g1) -' 1)))) -' 1 = (len (g2 + (g1 . ((len g1) -' 1)))) - 1 by XREAL_1:235;
set g4 = g1 ^ (g2 + (g1 . ((len g1) -' 1)));
A15: len (h1 ^ h2) = (len h1) + (len h2) by AFINSQ_1:20
.= len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) by A3, A8, A12, AFINSQ_1:20 ;
A16: len (h1 ^ h2) = (len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) by A3, A8, A12, AFINSQ_1:20;
then A17: len g1 < len (h1 ^ h2) by A7, A8, A12, XREAL_1:31;
A18: 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 A19: 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 A20: i + 1 < len g1 ; :: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1))

i < i + 1 by XREAL_1:31;
then i < len g1 by A20, XXREAL_0:2;
then A21: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = g1 . i by Th7;
A22: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = g1 . (i + 1) by A20, Th7;
(h1 ^ h2) . (i + 1) = h1 . (i + 1) by A3, A20, Th7;
hence (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1)) by A3, A5, A20, A22, A21; :: thesis: verum

end;

suppose A23: 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 A23, XXREAL_0:1;

suppose A24: 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 A19, XREAL_1:11;
then A25: i1 + 1 < ((len g1) + (len (g2 + (g1 . ((len g1) -' 1))))) - (len g1) by A3, A8, A12, AFINSQ_1:20;
then A26: (g2 + (g1 . ((len g1) -' 1))) . (i1 + 1) = (g2 . (i1 + 1)) + (g1 . ((len g1) -' 1)) by A12, Th6;
A27: len g1 <= i0 by A24, NAT_1:13;
i0 < len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) by A15, A19, NAT_1:13;
then A28: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i0 = (g2 + (g1 . ((len g1) -' 1))) . i1 by A27, AFINSQ_1:22;
i1 < i1 + 1 by XREAL_1:31;
then i1 < len (g2 + (g1 . ((len g1) -' 1))) by A25, XXREAL_0:2;
then A29: (g2 + (g1 . ((len g1) -' 1))) . i1 = (g2 . i1) + (g1 . ((len g1) -' 1)) by A12, Th6;
A30: g2 . (i1 + 1) = (g2 . i1) + (h2 . (i1 + 1)) by A8, A10, A12, A25;
A31: i1 + 1 = (i0 + 1) - (len h1) by A3;
then (h1 ^ h2) . (i0 + 1) = h2 . (i1 + 1) by A19, A23, AFINSQ_1:22;
hence (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1)) by A15, A19, A23, A31, A28, A29, A26, A30, AFINSQ_1:22; :: thesis: verum

end;

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

len g1 < (len g1) + 1 by XREAL_1:31;
then A33: (len g1) - 1 < len g1 by XREAL_1:21;
A34: i = (len g1) -' 1 by A32, NAT_D:34;
0 + 1 <= len g1 by A2, A3, NAT_1:13;
then (len g1) -' 1 = (len g1) - 1 by XREAL_1:235;
then (len g1) -' 1 in dom g1 by A33, NAT_1:45;
then A35: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = g1 . ((len g1) -' 1) by A34, AFINSQ_1:def 4;
A36: 0 in dom (g2 + (g1 . ((len g1) -' 1))) by A7, A8, A12, NAT_1:45;
(len g1) - (len h1) = 0 by A3;
then A37: h2 . 0 = (h1 ^ h2) . (i + 1) by A17, A32, AFINSQ_1:22;
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len g1) + 0 ) by A32
.= (g2 + (g1 . ((len g1) -' 1))) . 0 by A36, AFINSQ_1:def 4 ;
hence (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((h1 ^ h2) . (i + 1)) by A7, A8, A9, A35, A37, Th6; :: thesis: verum

end;

end;

end;

end;

end;

A38: len (h1 ^ h2) = (len g1) + (len g2) by A3, A8, AFINSQ_1:20
.= len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) by A12, AFINSQ_1:20 ;
A39: (h1 ^ h2) . 0 = h1 . 0 by A2, Th7
.= (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . 0 by A2, A3, A4, Th7 ;
len (h1 ^ h2) >= 0 + 1 by A1, NAT_1:13;
then (len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) >= 1 by A3, A8, A12, AFINSQ_1:20;
then A40: ((len g1) + (len (g2 + (g1 . ((len g1) -' 1))))) -' 1 = ((len g1) + (len (g2 + (g1 . ((len g1) -' 1))))) - 1 by XREAL_1:235
.= (len g1) + ((len (g2 + (g1 . ((len g1) -' 1)))) - 1)
.= (len g1) + ((len (g2 + (g1 . ((len g1) -' 1)))) -' 1) by A13, XREAL_1:235 ;
(len (g2 + (g1 . ((len g1) -' 1)))) - 1 < len (g2 + (g1 . ((len g1) -' 1))) by XREAL_1:46;
then (len (g2 + (g1 . ((len g1) -' 1)))) -' 1 in dom (g2 + (g1 . ((len g1) -' 1))) by A14, NAT_1:45;
then A41: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len (h1 ^ h2)) -' 1) = (g2 + (g1 . ((len g1) -' 1))) . ((len (g2 + (g1 . ((len g1) -' 1)))) -' 1) by A16, A40, AFINSQ_1:def 4;
(g1 . ((len g1) -' 1)) + (g2 . ((len h2) -' 1)) = (g2 + (g1 . ((len g1) -' 1))) . ((len h2) -' 1) by A8, A12, A14, Th6, XREAL_1:46;
hence Sum (h1 ^ h2) = (Sum h1) + (Sum h2) by A3, A6, A8, A11, A12, A38, A39, A18, A41, Def4; :: thesis: verum

end;

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

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

end;

end;

end;

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

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

end;

end;

end;

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

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

end;

end;