let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 (IDEA_Q_F (Key,n,r)) or (IDEA_Q_F (Key,n,r)) . x is set )
assume A1: x in dom (IDEA_Q_F (Key,n,r)) ; :: thesis: (IDEA_Q_F (Key,n,r)) . x is set
then consider xx being 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 set by A2; :: thesis: verum