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