theorem :: PDIFF_1:1

( ( for i, n being Nat st i in Seg n holds
( dom (proj (i,n)) = REAL n & rng (proj (i,n)) = REAL ) ) & ( for x being Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )