let X be RealUnitarySpace; :: thesis: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity implies for Y1, Y2 being finite Subset of X st Y1 misses Y2 holds
for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2) )
assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for Y1, Y2 being finite Subset of X st Y1 misses Y2 holds
for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2)
reconsider I = id the carrier of X as Function of the carrier of X, the carrier of X ;
let Y1, Y2 be finite Subset of X; :: thesis: ( Y1 misses Y2 implies for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2) )
assume A2: Y1 misses Y2 ; :: thesis: for Z being finite Subset of X st Z = Y1 \/ Y2 holds
setsum Z = (setsum Y1) + (setsum Y2)
A3: dom I = the carrier of X by FUNCT_2:def 1;
let Z be finite Subset of X; :: thesis: ( Z = Y1 \/ Y2 implies setsum Z = (setsum Y1) + (setsum Y2) )
assume Z = Y1 \/ Y2 ; :: thesis: setsum Z = (setsum Y1) + (setsum Y2)
then A4: setopfunc (Z, the carrier of X, the carrier of X,I, the addF of X) = (setopfunc (Y1, the carrier of X, the carrier of X,I, the addF of X)) + (setopfunc (Y2, the carrier of X, the carrier of X,I, the addF of X)) by A1, A2, A3, BHSP_5:14;
A5: for x being set st x in the carrier of X holds
I . x = x by FUNCT_1:18;
then ( setsum Y1 = setopfunc (Y1, the carrier of X, the carrier of X,I, the addF of X) & setsum Y2 = setopfunc (Y2, the carrier of X, the carrier of X,I, the addF of X) ) by A1, A3, Th1;
hence setsum Z = (setsum Y1) + (setsum Y2) by A1, A5, A3, A4, Th1; :: thesis: verum