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