A1: len p = n by CARD_1:def 7;
rng p c= REAL ;
hence p is Function of n,F_Real by A1, FUNCT_2:2; :: thesis: verum