((Seg n) --> T) . i = T by FUNCOP_1:13;
hence proj ((Seg n) --> T),i is real-valued ; :: thesis: verum