theorem Th15: :: ANPROJ10:28

for p being Tuple of 1, REAL holds - p is Tuple of 1, REAL