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