theorem Th6: :: RUSUB_6:7

for H being RealUnitarySpace ex F being Function of [: the carrier of H,( the carrier of H *):],( the carrier of H *) st
for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F . (x,e) & Fe = (x .|. e) (*) e )