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

proof

let x be object ; :: 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 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 ; :: thesis: verum