let D be non empty set ; for F, G being PartFunc of D,REAL
for X being set
for Y being finite set st Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
let F, G be PartFunc of D,REAL; for X being set
for Y being finite set st Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
let X be set ; for Y being finite set st Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
let Y be finite set ; ( Y = dom (F | X) & dom (F | X) = dom (G | X) implies Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X)) )
assume A1:
Y = dom (F | X)
; ( not dom (F | X) = dom (G | X) or Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X)) )
defpred S2[ Nat] means for F, G being PartFunc of D,REAL
for X being set
for Y being finite set st card Y = $1 & Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X));
A2:
card Y = card Y
;
A3:
for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be
Nat;
( S2[n] implies S2[n + 1] )
assume A4:
S2[
n]
;
S2[n + 1]
let F,
G be
PartFunc of
D,
REAL;
for X being set
for Y being finite set st card Y = n + 1 & Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))let X be
set ;
for Y being finite set st card Y = n + 1 & Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))let dx be
finite set ;
( card dx = n + 1 & dx = dom (F | X) & dom (F | X) = dom (G | X) implies Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X)) )
set gx =
dom (G | X);
assume that A5:
card dx = n + 1
and A6:
dx = dom (F | X)
and A7:
dom (F | X) = dom (G | X)
;
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
set x = the
Element of
dx;
reconsider x = the
Element of
dx as
Element of
D by A5, A6, CARD_1:27, TARSKI:def 3;
A8:
dx = (dom F) /\ X
by A6, RELAT_1:61;
then A9:
x in dom F
by A5, CARD_1:27, XBOOLE_0:def 4;
set Y =
X \ {x};
set dy =
dom (F | (X \ {x}));
set gy =
dom (G | (X \ {x}));
A10:
dom (G | X) = (dom G) /\ X
by RELAT_1:61;
then
x in dom G
by A5, A6, A7, CARD_1:27, XBOOLE_0:def 4;
then
x in (dom F) /\ (dom G)
by A9, XBOOLE_0:def 4;
then A11:
x in dom (F + G)
by VALUED_1:def 1;
A12:
dom (F | (X \ {x})) = (dom F) /\ (X \ {x})
by RELAT_1:61;
A13:
dom (F | (X \ {x})) = dx \ {x}
then reconsider dy =
dom (F | (X \ {x})) as
finite set ;
A18:
dom (G | (X \ {x})) = (dom G) /\ (X \ {x})
by RELAT_1:61;
A19:
dy = dom (G | (X \ {x}))
proof
thus
dy c= dom (G | (X \ {x}))
XBOOLE_0:def 10 dom (G | (X \ {x})) c= dyproof
let y be
object ;
TARSKI:def 3 ( not y in dy or y in dom (G | (X \ {x})) )
assume A20:
y in dy
;
y in dom (G | (X \ {x}))
then
y in dom F
by A12, XBOOLE_0:def 4;
then
y in dom (G | X)
by A6, A7, A12, A8, A20, XBOOLE_0:def 4;
then A21:
y in dom G
by A10, XBOOLE_0:def 4;
y in X \ {x}
by A12, A20, XBOOLE_0:def 4;
hence
y in dom (G | (X \ {x}))
by A18, A21, XBOOLE_0:def 4;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in dom (G | (X \ {x})) or y in dy )
assume A22:
y in dom (G | (X \ {x}))
;
y in dy
then
y in dom G
by A18, XBOOLE_0:def 4;
then
y in dx
by A6, A7, A18, A10, A22, XBOOLE_0:def 4;
then A23:
y in dom F
by A8, XBOOLE_0:def 4;
y in X \ {x}
by A18, A22, XBOOLE_0:def 4;
hence
y in dy
by A12, A23, XBOOLE_0:def 4;
verum
end;
{x} c= dx
by A5, CARD_1:27, ZFMISC_1:31;
then card dy =
(card dx) - (card {x})
by A13, CARD_2:44
.=
(n + 1) - 1
by A5, CARD_1:30
.=
n
;
then A24:
Sum (
(F + G),
(X \ {x}))
= (Sum (F,(X \ {x}))) + (Sum (G,(X \ {x})))
by A4, A19;
A25:
dom ((F + G) | X) =
dom ((F | X) + (G | X))
by RFUNCT_1:44
.=
dx /\ (dom (G | X))
by A6, VALUED_1:def 1
;
then A26:
FinS (
(F + G),
X),
(F + G) | X are_fiberwise_equipotent
by Def13;
x in X
by A5, A8, CARD_1:27, XBOOLE_0:def 4;
then
x in (dom (F + G)) /\ X
by A11, XBOOLE_0:def 4;
then
x in dom ((F + G) | X)
by RELAT_1:61;
then A27:
(FinS ((F + G),(X \ {x}))) ^ <*((F + G) . x)*>,
(F + G) | X are_fiberwise_equipotent
by A25, Th66;
reconsider Fx =
<*(F . x)*>,
Gx =
<*(G . x)*>,
FGx =
<*((F + G) . x)*> as
FinSequence of
REAL by RVSUM_1:145;
(
(FinS (F,(X \ {x}))) ^ <*(F . x)*>,
F | X are_fiberwise_equipotent &
FinS (
F,
X),
F | X are_fiberwise_equipotent )
by A5, A6, Def13, Th66, CARD_1:27;
then A28:
Sum (
F,
X) =
Sum ((FinS (F,(X \ {x}))) ^ Fx)
by CLASSES1:76, RFINSEQ:9
.=
(Sum (F,(X \ {x}))) + (F . x)
by RVSUM_1:74
;
(
(FinS (G,(X \ {x}))) ^ <*(G . x)*>,
G | X are_fiberwise_equipotent &
FinS (
G,
X),
G | X are_fiberwise_equipotent )
by A5, A6, A7, Def13, Th66, CARD_1:27;
then Sum (
G,
X) =
Sum ((FinS (G,(X \ {x}))) ^ Gx)
by CLASSES1:76, RFINSEQ:9
.=
(Sum (G,(X \ {x}))) + (G . x)
by RVSUM_1:74
;
hence (Sum (F,X)) + (Sum (G,X)) =
(Sum (FinS ((F + G),(X \ {x})))) + ((F . x) + (G . x))
by A24, A28
.=
(Sum (FinS ((F + G),(X \ {x})))) + ((F + G) . x)
by A11, VALUED_1:def 1
.=
Sum ((FinS ((F + G),(X \ {x}))) ^ FGx)
by RVSUM_1:74
.=
Sum (
(F + G),
X)
by A27, A26, CLASSES1:76, RFINSEQ:9
;
verum
end;
A29:
S2[ 0 ]
proof
let F,
G be
PartFunc of
D,
REAL;
for X being set
for Y being finite set st card Y = 0 & Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))let X be
set ;
for Y being finite set st card Y = 0 & Y = dom (F | X) & dom (F | X) = dom (G | X) holds
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))let Y be
finite set ;
( card Y = 0 & Y = dom (F | X) & dom (F | X) = dom (G | X) implies Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X)) )
assume that A30:
card Y = 0
and A31:
Y = dom (F | X)
and A32:
dom (F | X) = dom (G | X)
;
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
dom (F | X) = {}
by A30, A31;
then A33:
rng (F | X) = {}
by RELAT_1:42;
(F + G) | X = (F | X) + (G | X)
by RFUNCT_1:44;
then dom ((F + G) | X) =
(dom (F | X)) /\ (dom (G | X))
by VALUED_1:def 1
.=
{}
by A30, A31, A32
;
then
(
rng ((F + G) | X) = {} &
FinS (
(F + G),
X),
(F + G) | X are_fiberwise_equipotent )
by Def13, RELAT_1:42;
then A34:
rng (FinS ((F + G),X)) = {}
by CLASSES1:75;
FinS (
F,
X),
F | X are_fiberwise_equipotent
by A31, Def13;
then
rng (FinS (F,X)) = {}
by A33, CLASSES1:75;
then A35:
Sum (
F,
X)
= 0
by RELAT_1:41, RVSUM_1:72;
dom (G | X) = {}
by A30, A31, A32;
then A36:
rng (G | X) = {}
by RELAT_1:42;
FinS (
G,
X),
G | X are_fiberwise_equipotent
by A31, A32, Def13;
then
rng (FinS (G,X)) = {}
by A36, CLASSES1:75;
then
(Sum (F,X)) + (Sum (G,X)) = 0 + 0
by A35, RELAT_1:41, RVSUM_1:72;
hence
Sum (
(F + G),
X)
= (Sum (F,X)) + (Sum (G,X))
by A34, RELAT_1:41, RVSUM_1:72;
verum
end;
A37:
for n being Nat holds S2[n]
from NAT_1:sch 2(A29, A3);
assume
dom (F | X) = dom (G | X)
; Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
hence
Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X))
by A1, A37, A2; verum