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