ex x, y being object st
( x in NAT & y in REAL & T . p = [x,y] ) by ZFMISC_1:def 2;
hence (T . p) `2 is Real ; :: thesis: verum