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)
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)
let Z be finite Subset of X; :: thesis: ( Z = Y1 \/ Y2 implies setsum Z = (setsum Y1) + (setsum Y2) )
assume A3: Z = Y1 \/ Y2 ; :: thesis: setsum Z = (setsum Y1) + (setsum Y2)
reconsider I = id the carrier of X as Function of the carrier of X,the carrier of X ;
A4: for x being set st x in the carrier of X holds
I . x = x by FUNCT_1:35;
A5: dom I = the carrier of X by FUNCT_2:def 1;
then A6: setsum Y1 = setopfunc Y1,the carrier of X,the carrier of X,I,the addF of X by A1, A4, Th1;
A7: setsum Y2 = setopfunc Y2,the carrier of X,the carrier of X,I,the addF of X by A1, A4, A5, Th1;
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, A5, BHSP_5:14;
hence setsum Z = (setsum Y1) + (setsum Y2) by A1, A4, A5, A6, A7, Th1; :: thesis: verum