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 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 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 holds (P ! l) . x = P ! (Subst l,((a. 0 ) .--> x))
let l be QC-variable_list of ; :: thesis: (P ! l) . x = P ! (Subst l,((a. 0 ) .--> x))
reconsider P' = P as QC-pred_symbol ;
A1: P ! l is atomic by QC_LANG1:def 17;
then ( P' ! l = P ! l & the_arguments_of (P ! l) = l & the_pred_symbol_of (P ! l) = P' ) by QC_LANG1:def 21, QC_LANG1:def 22;
hence (P ! l) . x = P ! (Subst l,((a. 0 ) .--> x)) by A1, Th29; :: thesis: verum