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 I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

(setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = 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 I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

let S be finite OrthogonalFamily of X; :: thesis: ( not S is empty implies for I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

assume A2: not S is empty ; :: thesis: for I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

let I be Function of the carrier of X, the carrier of X; :: thesis: ( S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

assume that

A3: S c= dom I and

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

I . y = y ; :: thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

consider p being FinSequence of the carrier of X such that

A5: ( p is one-to-one & rng p = S ) and

A6: setopfunc (S, the carrier of X, the carrier of X,I, the addF of X) = the addF of X "**" (Func_Seq (I,p)) by A1, BHSP_5:def 5;

let H be Function of the carrier of X,REAL; :: thesis: ( S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) implies (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume that

A7: S c= dom H and

A8: for y being Point of X st y in S holds

H . y = y .|. y ; :: thesis: (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)

A9: setopfunc (S, the carrier of X,REAL,H,addreal) = addreal "**" (Func_Seq (H,p)) by A5, BHSP_5:def 5;

A10: for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds

the scalar of X . [(I . y1),(I . y2)] = 0

H . y = the scalar of X . [(I . y),(I . y)]

hence (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) by A6, A9, BHSP_1:def 1; :: thesis: verum

for I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

(setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = 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 I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

let S be finite OrthogonalFamily of X; :: thesis: ( not S is empty implies for I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

assume A2: not S is empty ; :: thesis: for I being Function of the carrier of X, the carrier of X st S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) holds

for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

let I be Function of the carrier of X, the carrier of X; :: thesis: ( S c= dom I & ( for y being Point of X st y in S holds

I . y = y ) implies for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

assume that

A3: S c= dom I and

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

I . y = y ; :: thesis: for H being Function of the carrier of X,REAL st S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) holds

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

consider p being FinSequence of the carrier of X such that

A5: ( p is one-to-one & rng p = S ) and

A6: setopfunc (S, the carrier of X, the carrier of X,I, the addF of X) = the addF of X "**" (Func_Seq (I,p)) by A1, BHSP_5:def 5;

let H be Function of the carrier of X,REAL; :: thesis: ( S c= dom H & ( for y being Point of X st y in S holds

H . y = y .|. y ) implies (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) )

assume that

A7: S c= dom H and

A8: for y being Point of X st y in S holds

H . y = y .|. y ; :: thesis: (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal)

A9: setopfunc (S, the carrier of X,REAL,H,addreal) = addreal "**" (Func_Seq (H,p)) by A5, BHSP_5:def 5;

A10: for y1, y2 being Point of X st y1 in S & y2 in S & y1 <> y2 holds

the scalar of X . [(I . y1),(I . y2)] = 0

proof

for y being Point of X st y in S holds
let y1, y2 be Point of X; :: thesis: ( y1 in S & y2 in S & y1 <> y2 implies the scalar of X . [(I . y1),(I . y2)] = 0 )

assume that

A11: ( y1 in S & y2 in S ) and

A12: y1 <> y2 ; :: thesis: the scalar of X . [(I . y1),(I . y2)] = 0

A13: y1 .|. y2 = 0 by A11, A12, BHSP_5:def 8;

( I . y1 = y1 & I . y2 = y2 ) by A4, A11;

hence the scalar of X . [(I . y1),(I . y2)] = 0 by A13, BHSP_1:def 1; :: thesis: verum

end;assume that

A11: ( y1 in S & y2 in S ) and

A12: y1 <> y2 ; :: thesis: the scalar of X . [(I . y1),(I . y2)] = 0

A13: y1 .|. y2 = 0 by A11, A12, BHSP_5:def 8;

( I . y1 = y1 & I . y2 = y2 ) by A4, A11;

hence the scalar of X . [(I . y1),(I . y2)] = 0 by A13, BHSP_1:def 1; :: thesis: verum

H . y = the scalar of X . [(I . y),(I . y)]

proof

then
the scalar of X . [( the addF of X "**" (Func_Seq (I,p))),( the addF of X "**" (Func_Seq (I,p)))] = addreal "**" (Func_Seq (H,p))
by A2, A3, A7, A5, A10, BHSP_5:9;
let y be Point of X; :: thesis: ( y in S implies H . y = the scalar of X . [(I . y),(I . y)] )

assume A14: y in S ; :: thesis: H . y = the scalar of X . [(I . y),(I . y)]

then A15: I . y = y by A4;

H . y = y .|. y by A8, A14

.= the scalar of X . [(I . y),(I . y)] by A15, BHSP_1:def 1 ;

hence H . y = the scalar of X . [(I . y),(I . y)] ; :: thesis: verum

end;assume A14: y in S ; :: thesis: H . y = the scalar of X . [(I . y),(I . y)]

then A15: I . y = y by A4;

H . y = y .|. y by A8, A14

.= the scalar of X . [(I . y),(I . y)] by A15, BHSP_1:def 1 ;

hence H . y = the scalar of X . [(I . y),(I . y)] ; :: thesis: verum

hence (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) .|. (setopfunc (S, the carrier of X, the carrier of X,I, the addF of X)) = setopfunc (S, the carrier of X,REAL,H,addreal) by A6, A9, BHSP_1:def 1; :: thesis: verum