for x being set st x in dom (IDEA_P_F Key,n,r) holds
(IDEA_P_F Key,n,r) . x is Function

proof

let x be set ; :: thesis: ( x in dom (IDEA_P_F Key,n,r) implies (IDEA_P_F Key,n,r) . x is Function )
assume A1: x in dom (IDEA_P_F Key,n,r) ; :: thesis: (IDEA_P_F Key,n,r) . x is Function
then consider xx being Element of NAT such that
A2: xx = x ;
(IDEA_P_F Key,n,r) . xx = IDEA_P (Line Key,xx),n by A1, A2, Def17;
hence (IDEA_P_F Key,n,r) . x is Function by A2; :: thesis: verum

end;

hence IDEA_P_F Key,n,r is Function-yielding by FUNCOP_1:def 6; :: thesis: verum