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

proof

let x be set ; :: thesis: ( x in dom (IDEA_Q_F (Key,n,r)) implies (IDEA_Q_F (Key,n,r)) . x is Function )
assume A1: x in dom (IDEA_Q_F (Key,n,r)) ; :: thesis: (IDEA_Q_F (Key,n,r)) . x is Function
then consider xx being Element of NAT such that
A2: xx = x ;
(IDEA_Q_F (Key,n,r)) . xx = IDEA_Q ((Line (Key,((r -' xx) + 1))),n) by A1, A2, Def18;
hence (IDEA_Q_F (Key,n,r)) . x is Function by A2; :: thesis: verum

end;

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