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₂[ Element of 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: S₂[ 0 ]

proof

let F, G be PartFunc of D,REAL ; :: thesis:
let X be set ; :: thesis:
let Y be finite set ; :: thesis:
assume A3: ( card Y = 0 & Y = dom (F | X) & dom (F | X) = dom (G | X) ) ; :: thesis:
then ( dom (F | X) = {} & dom (G | X) = {} ) ;
then A4: ( rng (F | X) = {} & rng (G | X) = {} ) by RELAT_1:65;
FinS F,X,F | X are_fiberwise_equipotent by A3, Def14;
then rng (FinS F,X) = {} by A4, CLASSES1:83;
then A5: Sum F,X = 0 by RELAT_1:64, RVSUM_1:102;
FinS G,X,G | X are_fiberwise_equipotent by A3, Def14;
then rng (FinS G,X) = {} by A4, CLASSES1:83;
then A6: (Sum F,X) + (Sum G,X) = 0 + 0 by A5, RELAT_1:64, RVSUM_1:102;
(F + G) | X = (F | X) + (G | X) by RFUNCT_1:60;
then A7: dom ((F + G) | X) = (dom (F | X)) /\ (dom (G | X)) by VALUED_1:def 1
.= {} by A3 ;
then A8: ( rng ((F + G) | X) = {} & dom ((F + G) | X) is finite ) by RELAT_1:65;
FinS (F + G),X,(F + G) | X are_fiberwise_equipotent by A7, Def14;
then rng (FinS (F + G),X) = {} by A8, CLASSES1:83;
hence Sum (F + G),X = (Sum F,X) + (Sum G,X) by A6, RELAT_1:64, RVSUM_1:102; :: thesis:

end;

A9: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A10: 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 A11: ( card dx = n + 1 & dx = dom (F | X) & dom (F | X) = dom (G | X) ) ; :: thesis:
consider x being Element of dx;
reconsider x = x as Element of D by A11, CARD_1:47, TARSKI:def 3;
set Y = X \ {x};
set dy = dom (F | (X \ {x}));
set gy = dom (G | (X \ {x}));
A12: ( {x} c= dx & dom (F | (X \ {x})) = (dom F) /\ (X \ {x}) & dx = (dom F) /\ X & dom (G | (X \ {x})) = (dom G) /\ (X \ {x}) & dom (G | X) = (dom G) /\ X ) by A11, CARD_1:47, RELAT_1:90, ZFMISC_1:37;
then A13: ( x in dom F & x in X & x in dom G ) by A11, CARD_1:47, XBOOLE_0:def 4;
then ( {x} c= X & x in (dom F) /\ (dom G) ) by XBOOLE_0:def 4, ZFMISC_1:37;
then A14: x in dom (F + G) by VALUED_1:def 1;
then x in (dom (F + G)) /\ X by A13, XBOOLE_0:def 4;
then A15: x in dom ((F + G) | X) by RELAT_1:90;
A16: dom ((F + G) | X) = dom ((F | X) + (G | X)) by RFUNCT_1:60
.= dx /\ (dom (G | X)) by A11, VALUED_1:def 1 ;
A17: 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 set ; :: according to TARSKI:def 3 :: thesis:
assume y in dom (F | (X \ {x})) ; :: thesis:
then A18: ( y in dom F & y in X \ {x} ) by A12, XBOOLE_0:def 4;
then A19: ( y in X & not y in {x} ) by XBOOLE_0:def 5;
y in dx by A12, A18, XBOOLE_0:def 4;
hence y in dx \ {x} by A19, XBOOLE_0:def 5; :: thesis:

end;

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

end;

then reconsider dy = dom (F | (X \ {x})) as finite set ;
A23: card dy = (card dx) - (card {x}) by A12, A17, CARD_2:63
.= (n + 1) - 1 by A11, CARD_1:50
.= n ;
dy = dom (G | (X \ {x}))

proof

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in dy ; :: thesis:
then A24: ( y in dom F & y in X \ {x} ) by A12, XBOOLE_0:def 4;
then y in dom (G | X) by A11, A12, XBOOLE_0:def 4;
then y in dom G by A12, XBOOLE_0:def 4;
hence y in dom (G | (X \ {x})) by A12, A24, XBOOLE_0:def 4; :: thesis:

end;

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in dom (G | (X \ {x})) ; :: thesis:
then A25: ( y in dom G & y in X \ {x} ) by A12, XBOOLE_0:def 4;
then y in dx by A11, A12, XBOOLE_0:def 4;
then y in dom F by A12, XBOOLE_0:def 4;
hence y in dy by A12, A25, XBOOLE_0:def 4; :: thesis:

end;

then A26: Sum (F + G),(X \ {x}) = (Sum F,(X \ {x})) + (Sum G,(X \ {x})) by A10, A23;
A27: (FinS F,(X \ {x})) ^ <*(F . x)*>,F | X are_fiberwise_equipotent by A11, Th69, CARD_1:47;
FinS F,X,F | X are_fiberwise_equipotent by A11, Def14;
then A28: Sum F,X = Sum ((FinS F,(X \ {x})) ^ <*(F . x)*>) by A27, CLASSES1:84, RFINSEQ:22
.= (Sum F,(X \ {x})) + (F . x) by RVSUM_1:104 ;
A29: (FinS G,(X \ {x})) ^ <*(G . x)*>,G | X are_fiberwise_equipotent by A11, Th69, CARD_1:47;
A30: FinS G,X,G | X are_fiberwise_equipotent by A11, Def14;
A31: (FinS (F + G),(X \ {x})) ^ <*((F + G) . x)*>,(F + G) | X are_fiberwise_equipotent by A15, A16, Th69;
A32: FinS (F + G),X,(F + G) | X are_fiberwise_equipotent by A16, Def14;
Sum G,X = Sum ((FinS G,(X \ {x})) ^ <*(G . x)*>) by A29, A30, CLASSES1:84, RFINSEQ:22
.= (Sum G,(X \ {x})) + (G . x) by RVSUM_1:104 ;
hence (Sum F,X) + (Sum G,X) = (Sum (FinS (F + G),(X \ {x}))) + ((F . x) + (G . x)) by A26, A28
.= (Sum (FinS (F + G),(X \ {x}))) + ((F + G) . x) by A14, VALUED_1:def 1
.= Sum ((FinS (F + G),(X \ {x})) ^ <*((F + G) . x)*>) by RVSUM_1:104
.= Sum (F + G),X by A31, A32, CLASSES1:84, RFINSEQ:22 ;
:: thesis:

end;

A33: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A2, A9);
assume A34: dom (F | X) = dom (G | X) ; :: thesis:
card Y = card Y ;
hence Sum (F + G),X = (Sum F,X) + (Sum G,X) by A1, A33, A34; :: thesis: