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

(IDEA_P_F (Key,n,r)) . x is Function

(IDEA_P_F (Key,n,r)) . x is Function

proof

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