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

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