let A be QC-alphabet ; 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; 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; 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; 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; (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; verum