let B1, B2 be finite natural-membered set ; :: thesis: for f being XFinSequence of st B1 <N< B2 holds
Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))
let f be XFinSequence of ; :: thesis: ( B1 <N< B2 implies Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2)) )
assume A1:
B1 <N< B2
; :: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))
set B10 = B1;
set B20 = B2;
set X0 = B1 /\ (len f);
set Y0 = B2 /\ (len f);
G55:
(B1 /\ (len f)) \/ (B2 /\ (len f)) = (B1 \/ B2) /\ (len f)
by XBOOLE_1:23;
(B1 /\ (len f)) /\ (B2 /\ (len f)) =
((B1 /\ (len f)) /\ (B2 /\ (len f))) /\ NAT
by MEMBERED:6, XBOOLE_1:28
.=
{}
by AE400, A1, AG110
;
then
B1 /\ (len f) misses B2 /\ (len f)
by XBOOLE_0:def 7;
then A92:
(card (B2 /\ (len f))) + (card (B1 /\ (len f))) = card ((B1 /\ (len f)) \/ (B2 /\ (len f)))
by CARD_2:53;
set f2 = SubXFinS f,(B1 \/ B2);
per cases
( len (SubXFinS f,(B1 \/ B2)) > 0 or len (SubXFinS f,(B1 \/ B2)) <= 0 )
;
suppose C1:
len (SubXFinS f,(B1 \/ B2)) > 0
;
:: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))set f3 =
SubXFinS f,
B1;
F3:
len (SubXFinS f,B1) = card (B1 /\ (len f))
by AC200;
per cases
( len (SubXFinS f,B1) > 0 or len (SubXFinS f,B1) <= 0 )
;
suppose D1:
len (SubXFinS f,B1) > 0
;
:: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))set f4 =
SubXFinS f,
B2;
F4:
len (SubXFinS f,B2) = card (B2 /\ (len f))
by AC200;
A1b:
B1 /\ (len f) <> {}
by D1, AC200, CARD_1:47;
per cases
( len (SubXFinS f,B2) > 0 or len (SubXFinS f,B2) <= 0 )
;
suppose E1:
len (SubXFinS f,B2) > 0
;
:: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))consider g1 being
XFinSequence of
such that E2:
(
len (SubXFinS f,B1) = len g1 &
(SubXFinS f,B1) . 0 = g1 . 0 & ( for
i being
Nat st
i + 1
< len (SubXFinS f,B1) holds
g1 . (i + 1) = (g1 . i) + ((SubXFinS f,B1) . (i + 1)) ) &
Sum (SubXFinS f,B1) = g1 . ((len (SubXFinS f,B1)) -' 1) )
by AC300;
consider g2 being
XFinSequence of
such that E3:
(
len (SubXFinS f,B2) = len g2 &
(SubXFinS f,B2) . 0 = g2 . 0 & ( for
i being
Nat st
i + 1
< len (SubXFinS f,B2) holds
g2 . (i + 1) = (g2 . i) + ((SubXFinS f,B2) . (i + 1)) ) &
Sum (SubXFinS f,B2) = g2 . ((len (SubXFinS f,B2)) -' 1) )
by AC300;
set a =
g1 . ((len g1) -' 1);
set g3 =
g2 + (g1 . ((len g1) -' 1));
E4:
(
len g2 = len (g2 + (g1 . ((len g1) -' 1))) & ( for
i being
Nat st
i < len g2 holds
(g2 + (g1 . ((len g1) -' 1))) . i = (g2 . i) + (g1 . ((len g1) -' 1)) ) )
by AC500;
E7:
B1 /\ (len f) misses B2 /\ (len f)
by AE101, A1, XBOOLE_1:76;
set g4 =
g1 ^ (g2 + (g1 . ((len g1) -' 1)));
E8b:
(len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) =
(card (card (B1 /\ (len f)))) + (len (SubXFinS f,B2))
by AC200, E2, E3, E4
.=
(card (B1 /\ (len f))) + (card (B2 /\ (len f)))
by AC200
.=
card ((B1 /\ (len f)) \/ (B2 /\ (len f)))
by E7, CARD_2:53
.=
card ((B1 \/ B2) /\ (len f))
by XBOOLE_1:23
.=
len (SubXFinS f,(B1 \/ B2))
by AC200
;
then E8:
len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) = len (SubXFinS f,(B1 \/ B2))
by AFINSQ_1:20;
F4h:
len (SubXFinS f,(B1 \/ B2)) = card ((B1 \/ B2) /\ (len f))
by AC200;
E44:
0 in len g1
by E2, D1, NAT_1:45;
E77n:
(Sgm0 (B1 /\ (len f))) . 0 = (Sgm0 ((B1 /\ (len f)) \/ (B2 /\ (len f)))) . 0
by AE220, A1b, AE400, A1;
E9:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . 0 =
g1 . 0
by E44, AFINSQ_1:def 4
.=
f . ((Sgm0 (B1 /\ (len f))) . 0 )
by AC200, D1, E2
.=
f . ((Sgm0 ((B1 \/ B2) /\ (len f))) . 0 )
by E77n, XBOOLE_1:23
.=
(SubXFinS f,(B1 \/ B2)) . 0
by AC200, C1
;
E89:
for
i being
Nat st
i + 1
< len (SubXFinS f,(B1 \/ B2)) holds
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))
proof
let i be
Nat;
:: thesis: ( i + 1 < len (SubXFinS f,(B1 \/ B2)) implies (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1)) )
assume F1:
i + 1
< len (SubXFinS f,(B1 \/ B2))
;
:: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))
per cases
( i + 1 < len g1 or i + 1 >= len g1 )
;
suppose G1:
i + 1
< len g1
;
:: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))then
i + 1
in dom g1
by NAT_1:45;
then G2:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = g1 . (i + 1)
by AFINSQ_1:def 4;
i < i + 1
by XREAL_1:31;
then
i < len g1
by G1, XXREAL_0:2;
then
i in dom g1
by NAT_1:45;
then G4:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = g1 . i
by AFINSQ_1:def 4;
i + 1
< len (Sgm0 (B1 /\ (len f)))
by Th44, G1, E2, F3;
then G20:
(Sgm0 (B1 /\ (len f))) . (i + 1) = (Sgm0 ((B1 \/ B2) /\ (len f))) . (i + 1)
by AE221, G55, AE400, A1;
(SubXFinS f,B1) . (i + 1) = f . ((Sgm0 (B1 /\ (len f))) . (i + 1))
by AC200, E2, G1;
then
(SubXFinS f,B1) . (i + 1) = (SubXFinS f,(B1 \/ B2)) . (i + 1)
by G20, AC200, F1;
hence
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))
by G2, G4, E2, G1;
:: thesis: verum end; suppose G1:
i + 1
>= len g1
;
:: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))set X0 =
B1 /\ (len f);
set Y0 =
B2 /\ (len f);
per cases
( i + 1 > len g1 or i + 1 = len g1 )
by G1, XXREAL_0:1;
suppose
i + 1
> len g1
;
:: thesis: (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (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
Nat ;
G67:
i + 1 =
(i1 + 1) + (len (SubXFinS f,B1))
by E2
.=
(i1 + 1) + (card (B1 /\ (len f)))
by AC200
;
G3dn:
(i + 1) - (len g1) < (len (SubXFinS f,(B1 \/ B2))) - (len g1)
by F1, XREAL_1:11;
then
i1 + 1
in dom (g2 + (g1 . ((len g1) -' 1)))
by E8b, NAT_1:45;
then G2n:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len g1) + (i1 + 1)) = (g2 + (g1 . ((len g1) -' 1))) . (i1 + 1)
by AFINSQ_1:def 4;
G3b:
(len g1) + i1 = i
;
i1 < i1 + 1
by XREAL_1:31;
then G3:
i1 < len (g2 + (g1 . ((len g1) -' 1)))
by E8b, G3dn, XXREAL_0:2;
then
i1 in dom (g2 + (g1 . ((len g1) -' 1)))
by NAT_1:45;
then G4:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = (g2 + (g1 . ((len g1) -' 1))) . i1
by G3b, AFINSQ_1:def 4;
G55:
(B1 /\ (len f)) \/ (B2 /\ (len f)) = (B1 \/ B2) /\ (len f)
by XBOOLE_1:23;
G20f:
len (Sgm0 (B1 /\ (len f))) = card (B1 /\ (len f))
by Th44;
i1 + 1
< len (Sgm0 (B2 /\ (len f)))
by Th44, E8b, G3dn, E3, E4, F4;
then G20:
(Sgm0 (B2 /\ (len f))) . (i1 + 1) = (Sgm0 ((B1 \/ B2) /\ (len f))) . (i + 1)
by G55, G67, G20f, AE222f, AE400, A1;
G21:
(SubXFinS f,B2) . (i1 + 1) = f . ((Sgm0 (B2 /\ (len f))) . (i1 + 1))
by AC200, E3, E4, E8b, G3dn;
G5:
(SubXFinS f,B2) . (i1 + 1) = (SubXFinS f,(B1 \/ B2)) . (i + 1)
by G20, G21, AC200, F1;
G51:
(g2 + (g1 . ((len g1) -' 1))) . i1 = (g2 . i1) + (g1 . ((len g1) -' 1))
by E4, G3;
G52:
(g2 + (g1 . ((len g1) -' 1))) . (i1 + 1) = (g2 . (i1 + 1)) + (g1 . ((len g1) -' 1))
by E4, E8b, G3dn;
g2 . (i1 + 1) = (g2 . i1) + ((SubXFinS f,B2) . (i1 + 1))
by E3, E4, E8b, G3dn;
hence
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))
by G2n, G4, G5, G51, G52;
:: 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) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))then H8:
i = (len g1) -' 1
by NAT_D:34;
H12:
len g1 = card (B1 /\ (len f))
by E2, AC200;
G55:
(B1 /\ (len f)) \/ (B2 /\ (len f)) = (B1 \/ B2) /\ (len f)
by XBOOLE_1:23;
G20f:
len (Sgm0 (B1 /\ (len f))) = card (B1 /\ (len f))
by Th44;
0 < len (Sgm0 (B2 /\ (len f)))
by Th44, E1, F4;
then
(Sgm0 (B2 /\ (len f))) . 0 = (Sgm0 ((B1 /\ (len f)) \/ (B2 /\ (len f)))) . (0 + (len (Sgm0 (B1 /\ (len f)))))
by AE222f, AE400, A1;
then G20:
(Sgm0 (B2 /\ (len f))) . 0 = (Sgm0 ((B1 \/ B2) /\ (len f))) . (len g1)
by G20f, H12, XBOOLE_1:23;
G2r:
0 in dom (g2 + (g1 . ((len g1) -' 1)))
by E1, E3, E4, 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 D1, E2, 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;
G21:
(SubXFinS f,B2) . 0 = f . ((Sgm0 (B2 /\ (len f))) . 0 )
by AC200, E1;
card (B2 /\ (len f)) > 0
by AC200, E1;
then
(SubXFinS f,B2) . 0 = (SubXFinS f,(B1 \/ B2)) . (i + 1)
by H0, G21, G20, AC200, E2, F3, F4h, G55, A92, XREAL_1:31;
hence
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))
by G2, G4, E3, AC500, E1;
:: thesis: verum end; end;
end; R4n:
len (g2 + (g1 . ((len g1) -' 1))) >= 0 + 1
by E3, E4, E1, NAT_1:13;
then R4:
(len (g2 + (g1 . ((len g1) -' 1)))) -' 1
= (len (g2 + (g1 . ((len g1) -' 1)))) - 1
by XREAL_1:235;
(len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) >= 0 + 1
by E8b, C1, NAT_1:13;
then R2:
((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 R4n, XREAL_1:235
;
(len (g2 + (g1 . ((len g1) -' 1)))) -' 1
< len (g2 + (g1 . ((len g1) -' 1)))
by R4, XREAL_1:46;
then R3:
(len (g2 + (g1 . ((len g1) -' 1)))) -' 1
in dom (g2 + (g1 . ((len g1) -' 1)))
by NAT_1:45;
R5:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len (SubXFinS f,(B1 \/ B2))) -' 1) = (g2 + (g1 . ((len g1) -' 1))) . ((len (g2 + (g1 . ((len g1) -' 1)))) -' 1)
by R2, R3, E8b, AFINSQ_1:def 4;
(g1 . ((len (SubXFinS f,B1)) -' 1)) + (g2 . ((len (SubXFinS f,B2)) -' 1)) = (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len (SubXFinS f,(B1 \/ B2))) -' 1)
by E2, R5, E3, E4, R4, XREAL_1:46;
hence
Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))
by AC300, E8, E9, E89, E2, E3;
:: thesis: verum end; end; end; suppose C1:
len (SubXFinS f,(B1 \/ B2)) <= 0
;
:: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))then C2:
SubXFinS f,
(B1 \/ B2) = {}
;
B1 /\ (len f) c= (B1 \/ B2) /\ (len f)
by XBOOLE_1:7, XBOOLE_1:26;
then
card (B1 /\ (len f)) c= card ((B1 \/ B2) /\ (len f))
by CARD_1:27;
then
card (B1 /\ (len f)) <= card ((B1 \/ B2) /\ (len f))
by NAT_1:40;
then C7:
card (B1 /\ (len f)) <= 0
by C1, AC200;
len (SubXFinS f,B1) = 0
by C7, AC200;
then
SubXFinS f,
B1 = 0
;
then C8:
Sum (SubXFinS f,B1) = 0
;
B2 /\ (len f) c= (B1 \/ B2) /\ (len f)
by XBOOLE_1:7, XBOOLE_1:26;
then
card (B2 /\ (len f)) c= card ((B1 \/ B2) /\ (len f))
by CARD_1:27;
then
card (B2 /\ (len f)) <= card ((B1 \/ B2) /\ (len f))
by NAT_1:40;
then
card (B2 /\ (len f)) <= 0
by C1, AC200;
then
len (SubXFinS f,B2) = 0
by AC200;
hence
Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))
by C2, C8, AFINSQ_1:18;
:: thesis: verum end;