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