let k be Element of NAT ; :: thesis: for x being bound_QC-variable
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds (P ! l) . x = P ! (Subst (l,((a. 0) .--> x)))
let x be bound_QC-variable; :: thesis: for P being QC-pred_symbol of k
for l being QC-variable_list of k holds (P ! l) . x = P ! (Subst (l,((a. 0) .--> x)))
let P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of k holds (P ! l) . x = P ! (Subst (l,((a. 0) .--> x)))
let l be QC-variable_list of k; :: thesis: (P ! l) . x = P ! (Subst (l,((a. 0) .--> x)))
reconsider P9 = P as QC-pred_symbol ;
A1: P ! l is atomic by QC_LANG1:def 16;
then ( the_arguments_of (P ! l) = l & the_pred_symbol_of (P ! l) = P9 ) by QC_LANG1:def 20, QC_LANG1:def 21;
hence (P ! l) . x = P ! (Subst (l,((a. 0) .--> x))) by A1, Th29; :: thesis: verum