reconsider F1 = QC-pred_symbols --> (empty_rel D) as Function of QC-pred_symbols,(relations_on D) ;
take F1 ; :: thesis: for P being Element of QC-pred_symbols
for r being Element of relations_on D holds
( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )
let P be Element of QC-pred_symbols ; :: thesis: for r being Element of relations_on D holds
( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )
thus for r being Element of relations_on D holds
( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) by FUNCOP_1:13; :: thesis: verum