let A be QC-alphabet ; :: thesis: for e being Element of vSUB A
for k being Nat
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let e be Element of vSUB A; :: thesis: for k being Nat
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let P be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e]
let ll be QC-variable_list of k,A; :: thesis: Sub_P (P,ll,e) = [(P ! ll),e]
set QCP = { QP where QP is QC-pred_symbol of A : the_arity_of QP = k } ;
P in { QP where QP is QC-pred_symbol of A : the_arity_of QP = k } ;
then A1: ex Q being QC-pred_symbol of A st
( P = Q & the_arity_of Q = k ) ;
len ll = k by CARD_1:def 7;
hence Sub_P (P,ll,e) = [(P ! ll),e] by A1, Def18; :: thesis: verum