let D be non empty set ; :: thesis:
let F, G be PartFunc of D,REAL; :: thesis:
let X be set ; :: thesis:
let Y be finite set ; :: thesis:
assume A1: Y = dom (F | X) ; :: thesis:
defpred S₂[ 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 S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A4: S₂[n] ; :: thesis:
let F, G be PartFunc of D,REAL; :: thesis:
let X be set ; :: thesis:
let dx be finite set ; :: thesis:
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) ; :: thesis:
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}

proof

thus dom (F | (X \ {x})) c= dx \ {x} :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: y in dom (F | (X \ {x})) ; :: thesis:
then y in X \ {x} by A12, XBOOLE_0:def 4;
then A15: not y in {x} by XBOOLE_0:def 5;
y in dom F by A12, A14, XBOOLE_0:def 4;
then y in dx by A12, A8, A14, XBOOLE_0:def 4;
hence y in dx \ {x} by A15, XBOOLE_0:def 5; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A16: y in dx \ {x} ; :: thesis:
then ( not y in {x} & y in X ) by A8, XBOOLE_0:def 4, XBOOLE_0:def 5;
then A17: y in X \ {x} by XBOOLE_0:def 5;
y in dom F by A8, A16, XBOOLE_0:def 4;
hence y in dom (F | (X \ {x})) by A12, A17, XBOOLE_0:def 4; :: thesis:

end;

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})) :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A20: y in dy ; :: thesis:
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; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A22: y in dom (G | (X \ {x})) ; :: thesis:
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; :: thesis:

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 ;
:: thesis:

end;

A29: S₂[ 0 ]

proof

let F, G be PartFunc of D,REAL; :: thesis:
let X be set ; :: thesis:
let Y be finite set ; :: thesis:
assume that
A30: card Y = 0 and
A31: Y = dom (F | X) and
A32: dom (F | X) = dom (G | X) ; :: thesis:
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; :: thesis:

end;

A37: for n being Nat holds S₂[n] from NAT_1:sch 2(A29, A3);
assume dom (F | X) = dom (G | X) ; :: thesis:
hence Sum ((F + G),X) = (Sum (F,X)) + (Sum (G,X)) by A1, A37, A2; :: thesis: