let ll1, ll2 be FinSequence of QC-variables A; :: thesis: ( ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll1 = ll & S = Sub_P (P,ll,e) ) & ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st
( ll2 = ll & S = Sub_P (P,ll,e) ) implies ll1 = ll2 )
given k1 being Element of NAT , P1 being QC-pred_symbol of k1,A, ll19 being QC-variable_list of k1,A, e1 being Element of vSUB A such that A2: ll1 = ll19 and
A3: S = Sub_P (P1,ll19,e1) ; :: thesis: ( for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A
for e being Element of vSUB A holds
( not ll2 = ll or not S = Sub_P (P,ll,e) ) or ll1 = ll2 )
A4: S = [(P1 ! ll19),e1] by A3, Th9;
given k2 being Element of NAT , P2 being QC-pred_symbol of k2,A, ll29 being QC-variable_list of k2,A, e2 being Element of vSUB A such that A5: ll2 = ll29 and
A6: S = Sub_P (P2,ll29,e2) ; :: thesis: ll1 = ll2
<*P1*> ^ ll19 = P1 ! ll19 by QC_LANG1:8;
then A7: ( <*P2*> ^ ll29 = P2 ! ll29 & S `1 = <*P1*> ^ ll19 ) by A4, MCART_1:7, QC_LANG1:8;
A8: S `1 is atomic by B1, Th11;
A9: S = [(P2 ! ll29),e2] by A6, Th9;
then A10: S `1 = P2 ! ll29 by MCART_1:7;
S `1 = P1 ! ll19 by A4, MCART_1:7;
then P1 = the_pred_symbol_of (S `1) by A8, QC_LANG1:def 22
.= P2 by A10, A8, QC_LANG1:def 22 ;
hence ll1 = ll2 by A2, A5, A9, A7, FINSEQ_1:33, MCART_1:7; :: thesis: verum