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);
(B1 /\ (len f)) /\ (B2 /\ (len f)) =
((B1 /\ (len f)) /\ (B2 /\ (len f))) /\ NAT
by MEMBERED:6, XBOOLE_1:28
.=
{}
by A1, Th34, Th36
;
then
B1 /\ (len f) misses B2 /\ (len f)
by XBOOLE_0:def 7;
then A2:
(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);
A3:
(B1 /\ (len f)) \/ (B2 /\ (len f)) = (B1 \/ B2) /\ (len f)
by XBOOLE_1:23;
per cases
( len (SubXFinS f,(B1 \/ B2)) > 0 or len (SubXFinS f,(B1 \/ B2)) <= 0 )
;
suppose A4:
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;
A5:
len (SubXFinS f,B1) = card (B1 /\ (len f))
by Th47;
per cases
( len (SubXFinS f,B1) > 0 or len (SubXFinS f,B1) <= 0 )
;
suppose A6:
len (SubXFinS f,B1) > 0
;
:: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))then A7:
B1 /\ (len f) <> {}
by Th47, CARD_1:47;
set f4 =
SubXFinS f,
B2;
A8:
len (SubXFinS f,B2) = card (B2 /\ (len f))
by Th47;
per cases
( len (SubXFinS f,B2) > 0 or len (SubXFinS f,B2) <= 0 )
;
suppose A9:
len (SubXFinS f,B2) > 0
;
:: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))A10:
B1 /\ (len f) misses B2 /\ (len f)
by A1, Th35, XBOOLE_1:76;
consider g2 being
XFinSequence of
such that A11:
len (SubXFinS f,B2) = len g2
and A12:
(SubXFinS f,B2) . 0 = g2 . 0
and A13:
for
i being
Nat st
i + 1
< len (SubXFinS f,B2) holds
g2 . (i + 1) = (g2 . i) + ((SubXFinS f,B2) . (i + 1))
and A14:
Sum (SubXFinS f,B2) = g2 . ((len (SubXFinS f,B2)) -' 1)
by Def4;
consider g1 being
XFinSequence of
such that A15:
len (SubXFinS f,B1) = len g1
and A16:
(SubXFinS f,B1) . 0 = g1 . 0
and A17:
for
i being
Nat st
i + 1
< len (SubXFinS f,B1) holds
g1 . (i + 1) = (g1 . i) + ((SubXFinS f,B1) . (i + 1))
and A18:
Sum (SubXFinS f,B1) = g1 . ((len (SubXFinS f,B1)) -' 1)
by Def4;
set a =
g1 . ((len g1) -' 1);
set g3 =
g2 + (g1 . ((len g1) -' 1));
set g4 =
g1 ^ (g2 + (g1 . ((len g1) -' 1)));
A19:
len g2 = len (g2 + (g1 . ((len g1) -' 1)))
by Th6;
then A20:
len (g2 + (g1 . ((len g1) -' 1))) >= 0 + 1
by A9, A11, NAT_1:13;
then A21:
(len (g2 + (g1 . ((len g1) -' 1)))) -' 1
= (len (g2 + (g1 . ((len g1) -' 1)))) - 1
by XREAL_1:235;
then
(len (g2 + (g1 . ((len g1) -' 1)))) -' 1
< len (g2 + (g1 . ((len g1) -' 1)))
by XREAL_1:46;
then A22:
(len (g2 + (g1 . ((len g1) -' 1)))) -' 1
in dom (g2 + (g1 . ((len g1) -' 1)))
by NAT_1:45;
A23:
(len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) =
(card (card (B1 /\ (len f)))) + (len (SubXFinS f,B2))
by A15, A11, A19, Th47
.=
(card (B1 /\ (len f))) + (card (B2 /\ (len f)))
by Th47
.=
card ((B1 /\ (len f)) \/ (B2 /\ (len f)))
by A10, CARD_2:53
.=
card ((B1 \/ B2) /\ (len f))
by XBOOLE_1:23
.=
len (SubXFinS f,(B1 \/ B2))
by Th47
;
then
(len g1) + (len (g2 + (g1 . ((len g1) -' 1)))) >= 0 + 1
by A4, NAT_1:13;
then ((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 A20, XREAL_1:235
;
then
(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 A23, A22, AFINSQ_1:def 4;
then A24:
(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 A15, A11, A19, A21, Th6, XREAL_1:46;
A25:
len (SubXFinS f,(B1 \/ B2)) = card ((B1 \/ B2) /\ (len f))
by Th47;
A26:
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 A27:
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 A28:
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
< len (Sgm0 (B1 /\ (len f)))
by A5, A15, Th31;
then A29:
(Sgm0 (B1 /\ (len f))) . (i + 1) = (Sgm0 ((B1 \/ B2) /\ (len f))) . (i + 1)
by A1, A3, Th36, Th40;
i + 1
in dom g1
by A28, NAT_1:45;
then A30:
(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 A28, XXREAL_0:2;
then
i in dom g1
by NAT_1:45;
then A31:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = g1 . i
by AFINSQ_1:def 4;
(SubXFinS f,B1) . (i + 1) = f . ((Sgm0 (B1 /\ (len f))) . (i + 1))
by A15, A28, Th47;
then
(SubXFinS f,B1) . (i + 1) = (SubXFinS f,(B1 \/ B2)) . (i + 1)
by A27, A29, Th47;
hence
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))
by A15, A17, A28, A30, A31;
:: 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) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))set Y0 =
B2 /\ (len f);
set X0 =
B1 /\ (len f);
per cases
( i + 1 > len g1 or i + 1 = len g1 )
by A32, 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 ;
A33:
(len g1) + i1 = i
;
A34:
(i + 1) - (len g1) < (len (SubXFinS f,(B1 \/ B2))) - (len g1)
by A27, XREAL_1:11;
then A35:
(SubXFinS f,B2) . (i1 + 1) = f . ((Sgm0 (B2 /\ (len f))) . (i1 + 1))
by A11, A19, A23, Th47;
A36:
len (Sgm0 (B1 /\ (len f))) = card (B1 /\ (len f))
by Th31;
A37:
i + 1 =
(i1 + 1) + (len (SubXFinS f,B1))
by A15
.=
(i1 + 1) + (card (B1 /\ (len f)))
by Th47
;
A38:
(B1 /\ (len f)) \/ (B2 /\ (len f)) = (B1 \/ B2) /\ (len f)
by XBOOLE_1:23;
i1 + 1
< len (Sgm0 (B2 /\ (len f)))
by A8, A11, A19, A23, A34, Th31;
then
(Sgm0 (B2 /\ (len f))) . (i1 + 1) = (Sgm0 ((B1 \/ B2) /\ (len f))) . (i + 1)
by A1, A37, A38, A36, Th36, Th42;
then A39:
(SubXFinS f,B2) . (i1 + 1) = (SubXFinS f,(B1 \/ B2)) . (i + 1)
by A27, A35, Th47;
i1 < i1 + 1
by XREAL_1:31;
then A40:
i1 < len (g2 + (g1 . ((len g1) -' 1)))
by A23, A34, XXREAL_0:2;
then A41:
(g2 + (g1 . ((len g1) -' 1))) . i1 = (g2 . i1) + (g1 . ((len g1) -' 1))
by A19, Th6;
A42:
(g2 + (g1 . ((len g1) -' 1))) . (i1 + 1) = (g2 . (i1 + 1)) + (g1 . ((len g1) -' 1))
by A19, A23, A34, Th6;
i1 + 1
in dom (g2 + (g1 . ((len g1) -' 1)))
by A23, A34, NAT_1:45;
then A43:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len g1) + (i1 + 1)) = (g2 + (g1 . ((len g1) -' 1))) . (i1 + 1)
by AFINSQ_1:def 4;
i1 in dom (g2 + (g1 . ((len g1) -' 1)))
by A40, NAT_1:45;
then A44:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = (g2 + (g1 . ((len g1) -' 1))) . i1
by A33, AFINSQ_1:def 4;
g2 . (i1 + 1) = (g2 . i1) + ((SubXFinS f,B2) . (i1 + 1))
by A11, A13, A19, A23, A34;
hence
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) = ((g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i) + ((SubXFinS f,(B1 \/ B2)) . (i + 1))
by A43, A44, A39, A41, A42;
:: thesis: verum end; suppose A45:
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))
len g1 < (len g1) + 1
by XREAL_1:31;
then A46:
(len g1) - 1
< len g1
by XREAL_1:21;
A47:
i = (len g1) -' 1
by A45, NAT_D:34;
0 + 1
<= len g1
by A6, A15, NAT_1:13;
then
(len g1) -' 1
= (len g1) - 1
by XREAL_1:235;
then
(len g1) -' 1
in dom g1
by A46, NAT_1:45;
then A48:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . i = g1 . ((len g1) -' 1)
by A47, AFINSQ_1:def 4;
A49:
len (Sgm0 (B1 /\ (len f))) = card (B1 /\ (len f))
by Th31;
0 < len (Sgm0 (B2 /\ (len f)))
by A8, A9, Th31;
then A50:
(Sgm0 (B2 /\ (len f))) . 0 = (Sgm0 ((B1 /\ (len f)) \/ (B2 /\ (len f)))) . (0 + (len (Sgm0 (B1 /\ (len f)))))
by A1, Th36, Th42;
A51:
(B1 /\ (len f)) \/ (B2 /\ (len f)) = (B1 \/ B2) /\ (len f)
by XBOOLE_1:23;
A52:
0 in dom (g2 + (g1 . ((len g1) -' 1)))
by A9, A11, A19, NAT_1:45;
A53:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . (i + 1) =
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . ((len g1) + 0 )
by A45
.=
(g2 + (g1 . ((len g1) -' 1))) . 0
by A52, AFINSQ_1:def 4
;
A54:
card (B2 /\ (len f)) > 0
by A9, Th47;
(SubXFinS f,B2) . 0 = f . ((Sgm0 (B2 /\ (len f))) . 0 )
by A9, Th47;
then
(SubXFinS f,B2) . 0 = (SubXFinS f,(B1 \/ B2)) . (i + 1)
by A2, A5, A15, A25, A45, A51, A49, A50, A54, Th47, 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 A9, A11, A12, A53, A48, Th6;
:: thesis: verum end; end;
end; A55:
(Sgm0 (B1 /\ (len f))) . 0 = (Sgm0 ((B1 /\ (len f)) \/ (B2 /\ (len f)))) . 0
by A1, A7, Th36, Th45;
0 in len g1
by A6, A15, NAT_1:45;
then A56:
(g1 ^ (g2 + (g1 . ((len g1) -' 1)))) . 0 =
g1 . 0
by AFINSQ_1:def 4
.=
f . ((Sgm0 (B1 /\ (len f))) . 0 )
by A6, A16, Th47
.=
f . ((Sgm0 ((B1 \/ B2) /\ (len f))) . 0 )
by A55, XBOOLE_1:23
.=
(SubXFinS f,(B1 \/ B2)) . 0
by A4, Th47
;
len (g1 ^ (g2 + (g1 . ((len g1) -' 1)))) = len (SubXFinS f,(B1 \/ B2))
by A23, AFINSQ_1:20;
hence
Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))
by A18, A14, A56, A26, A24, Def4;
:: thesis: verum end; end; end; suppose A63:
len (SubXFinS f,(B1 \/ B2)) <= 0
;
:: thesis: Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,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
card (B1 /\ (len f)) <= 0
by A63, Th47;
then
len (SubXFinS f,B1) = 0
by Th47;
then
SubXFinS f,
B1 = 0
;
then A64:
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 A63, Th47;
then A65:
len (SubXFinS f,B2) = 0
by Th47;
SubXFinS f,
(B1 \/ B2) = {}
by A63;
hence
Sum (SubXFinS f,(B1 \/ B2)) = (Sum (SubXFinS f,B1)) + (Sum (SubXFinS f,B2))
by A64, A65, AFINSQ_1:18;
:: thesis: verum end;