theorem Th6: :: CIRCLED1:6

for V being RealLinearSpace holds Up ((Omega). V) is circled