let k be Element of NAT ; :: thesis: for P, P' being QC-pred_symbol of k
for ll, ll' being CQC-variable_list of
for Sub, Sub' being CQC_Substitution st Sub_the_arguments_of (Sub_P P,ll,Sub) = Sub_the_arguments_of (Sub_P P',ll',Sub') holds
ll = ll'
let P, P' be QC-pred_symbol of k; :: thesis: for ll, ll' being CQC-variable_list of
for Sub, Sub' being CQC_Substitution st Sub_the_arguments_of (Sub_P P,ll,Sub) = Sub_the_arguments_of (Sub_P P',ll',Sub') holds
ll = ll'
let ll, ll' be CQC-variable_list of ; :: thesis: for Sub, Sub' being CQC_Substitution st Sub_the_arguments_of (Sub_P P,ll,Sub) = Sub_the_arguments_of (Sub_P P',ll',Sub') holds
ll = ll'
let Sub, Sub' be CQC_Substitution; :: thesis: ( Sub_the_arguments_of (Sub_P P,ll,Sub) = Sub_the_arguments_of (Sub_P P',ll',Sub') implies ll = ll' )
assume A1: Sub_the_arguments_of (Sub_P P,ll,Sub) = Sub_the_arguments_of (Sub_P P',ll',Sub') ; :: thesis: ll = ll'
consider k1 being Element of NAT , P1 being QC-pred_symbol of k1, ll1 being QC-variable_list of , e1 being Element of vSUB such that
A2: ( Sub_the_arguments_of (Sub_P P,ll,Sub) = ll1 & Sub_P P,ll,Sub = Sub_P P1,ll1,e1 ) by SUBSTUT1:def 29;
consider k2 being Element of NAT , P2 being QC-pred_symbol of k2, ll2 being QC-variable_list of , e2 being Element of vSUB such that
A3: ( Sub_the_arguments_of (Sub_P P',ll',Sub') = ll2 & Sub_P P',ll',Sub' = Sub_P P2,ll2,e2 ) by SUBSTUT1:def 29;
Sub_P P,ll,Sub = [(P ! ll),Sub] by SUBSTUT1:9;
then A4: [(P ! ll),Sub] = [(P1 ! ll1),e1] by A2, SUBSTUT1:9;
( P ! ll = <*P*> ^ ll & P1 ! ll1 = <*P1*> ^ ll1 ) by QC_LANG1:23;
then A5: <*P1*> ^ ll1 = <*P*> ^ ll by A4, ZFMISC_1:33;
( (<*P1*> ^ ll1) . 1 = P1 & (<*P*> ^ ll) . 1 = P ) by FINSEQ_1:58;
then A6: ll1 = ll by A5, FINSEQ_1:46;
Sub_P P',ll',Sub' = [(P' ! ll'),Sub'] by SUBSTUT1:9;
then A7: [(P' ! ll'),Sub'] = [(P2 ! ll2),e2] by A3, SUBSTUT1:9;
( P' ! ll' = <*P'*> ^ ll' & P2 ! ll2 = <*P2*> ^ ll2 ) by QC_LANG1:23;
then A8: <*P2*> ^ ll2 = <*P'*> ^ ll' by A7, ZFMISC_1:33;
( (<*P2*> ^ ll2) . 1 = P2 & (<*P'*> ^ ll') . 1 = P' ) by FINSEQ_1:58;
hence ll = ll' by A1, A2, A3, A6, A8, FINSEQ_1:46; :: thesis: verum