reconsider F1 = (QC-pred_symbols Al) --> (empty_rel D) as Function of (QC-pred_symbols Al),(relations_on D) ;
take F1 ; :: thesis: for P being Element of QC-pred_symbols Al
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 Al; :: 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:7; :: thesis: verum