let Al be QC-alphabet ; :: thesis: for k being Nat
for P, P9 being QC-pred_symbol of k,Al
for ll, ll9 being CQC-variable_list of k,Al
for Sub, Sub9 being CQC_Substitution of Al st Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) holds
ll = ll9
let k be Nat; :: thesis: for P, P9 being QC-pred_symbol of k,Al
for ll, ll9 being CQC-variable_list of k,Al
for Sub, Sub9 being CQC_Substitution of Al st Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) holds
ll = ll9
let P, P9 be QC-pred_symbol of k,Al; :: thesis: for ll, ll9 being CQC-variable_list of k,Al
for Sub, Sub9 being CQC_Substitution of Al st Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) holds
ll = ll9
let ll, ll9 be CQC-variable_list of k,Al; :: thesis: for Sub, Sub9 being CQC_Substitution of Al st Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) holds
ll = ll9
let Sub, Sub9 be CQC_Substitution of Al; :: thesis: ( Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) implies ll = ll9 )
assume A1: Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) ; :: thesis: ll = ll9
consider k1 being Nat, P1 being QC-pred_symbol of k1,Al, ll1 being QC-variable_list of k1,Al, e1 being Element of vSUB Al such that
A2: Sub_the_arguments_of (Sub_P (P,ll,Sub)) = ll1 and
A3: Sub_P (P,ll,Sub) = Sub_P (P1,ll1,e1) by SUBSTUT1:def 29;
A4: ( P ! ll = <*P*> ^ ll & P1 ! ll1 = <*P1*> ^ ll1 ) by QC_LANG1:8;
Sub_P (P,ll,Sub) = [(P ! ll),Sub] by SUBSTUT1:9;
then [(P ! ll),Sub] = [(P1 ! ll1),e1] by A3, SUBSTUT1:9;
then A5: <*P1*> ^ ll1 = <*P*> ^ ll by A4, XTUPLE_0:1;
( (<*P1*> ^ ll1) . 1 = P1 & (<*P*> ^ ll) . 1 = P ) by FINSEQ_1:41;
then A6: ll1 = ll by A5, FINSEQ_1:33;
consider k2 being Nat, P2 being QC-pred_symbol of k2,Al, ll2 being QC-variable_list of k2,Al, e2 being Element of vSUB Al such that
A7: Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) = ll2 and
A8: Sub_P (P9,ll9,Sub9) = Sub_P (P2,ll2,e2) by SUBSTUT1:def 29;
A9: ( P9 ! ll9 = <*P9*> ^ ll9 & P2 ! ll2 = <*P2*> ^ ll2 ) by QC_LANG1:8;
Sub_P (P9,ll9,Sub9) = [(P9 ! ll9),Sub9] by SUBSTUT1:9;
then [(P9 ! ll9),Sub9] = [(P2 ! ll2),e2] by A8, SUBSTUT1:9;
then A10: <*P2*> ^ ll2 = <*P9*> ^ ll9 by A9, XTUPLE_0:1;
( (<*P2*> ^ ll2) . 1 = P2 & (<*P9*> ^ ll9) . 1 = P9 ) by FINSEQ_1:41;
hence ll = ll9 by A1, A2, A7, A6, A10, FINSEQ_1:33; :: thesis: verum