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 ;
( 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))
;
(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;
verum
end;
hence
IDEA_P_F (Key,n,r) is Function-yielding
; verum