let e be Element of vSUB ; :: thesis: for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds Sub_P (P,ll,e) = [(P ! ll),e]
let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds Sub_P (P,ll,e) = [(P ! ll),e]
let P be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k holds Sub_P (P,ll,e) = [(P ! ll),e]
let ll be QC-variable_list of k; :: thesis: Sub_P (P,ll,e) = [(P ! ll),e]
set QCP = { QP where QP is QC-pred_symbol : the_arity_of QP = k } ;
P in { QP where QP is QC-pred_symbol : the_arity_of QP = k } ;
then A1: ex Q being QC-pred_symbol 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