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 S being finite OrthogonalFamily of X st not S is empty holds

for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for S being finite OrthogonalFamily of X st not S is empty holds

for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)

reconsider I = id the carrier of X as Function of the carrier of X, the carrier of X ;

let S be finite OrthogonalFamily of X; :: thesis: ( not S is empty implies for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume A2: not S is empty ; :: thesis: for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)

let H be Functional of X; :: thesis: ( S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) implies (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume A3: ( S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) ) ; :: thesis: (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)

A4: for x being Point of X st x in S holds

I . x = x ;

A5: dom I = the carrier of X by FUNCT_2:def 1;

for x being set st x in the carrier of X holds

I . x = x by FUNCT_1:18;

then setsum S = setopfunc (S, the carrier of X, the carrier of X,I, the addF of X) by A1, A5, BHSP_6:1;

hence (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) by A1, A2, A3, A5, A4, Th2; :: thesis: verum

for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume A1: ( the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity ) ; :: thesis: for S being finite OrthogonalFamily of X st not S is empty holds

for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)

reconsider I = id the carrier of X as Function of the carrier of X, the carrier of X ;

let S be finite OrthogonalFamily of X; :: thesis: ( not S is empty implies for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume A2: not S is empty ; :: thesis: for H being Functional of X st S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) holds

(setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)

let H be Functional of X; :: thesis: ( S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) implies (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume A3: ( S c= dom H & ( for x being Point of X st x in S holds

H . x = x .|. x ) ) ; :: thesis: (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal)

A4: for x being Point of X st x in S holds

I . x = x ;

A5: dom I = the carrier of X by FUNCT_2:def 1;

for x being set st x in the carrier of X holds

I . x = x by FUNCT_1:18;

then setsum S = setopfunc (S, the carrier of X, the carrier of X,I, the addF of X) by A1, A5, BHSP_6:1;

hence (setsum S) .|. (setsum S) = setopfunc (S, the carrier of X,REAL,H,addreal) by A1, A2, A3, A5, A4, Th2; :: thesis: verum