thus proj (((Seg n) --> T),i) is real-valued ; :: thesis: verum