let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for k being Nat
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let x be bound_QC-variable of A; :: thesis: for k being Nat
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let P be QC-pred_symbol of k,A; :: thesis: for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
let l be QC-variable_list of k,A; :: thesis: (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x)))
reconsider P9 = P as QC-pred_symbol of A ;
A1: P ! l is atomic by QC_LANG1:def 18;
then ( the_arguments_of (P ! l) = l & the_pred_symbol_of (P ! l) = P9 ) by QC_LANG1:def 22, QC_LANG1:def 23;
hence (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x))) by A1, Th16; :: thesis: verum