let ll1, ll2 be FinSequence of QC-variables ; :: thesis: ( ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of ex e being Element of vSUB st
( ll1 = ll & S = Sub_P P,ll,e ) & ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of ex e being Element of vSUB 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, ll1' being QC-variable_list of , e1 being Element of vSUB such that A3: ( ll1 = ll1' & S = Sub_P P1,ll1',e1 ) ; :: thesis: ( for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of
for e being Element of vSUB holds
( not ll2 = ll or not S = Sub_P P,ll,e ) or ll1 = ll2 )
given 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 A4: ( ll2 = ll2' & S = Sub_P P2,ll2',e2 ) ; :: thesis: ll1 = ll2
A5: ( <*P1*> ^ ll1' = P1 ! ll1' & <*P2*> ^ ll2' = P2 ! ll2' ) by QC_LANG1:23;
( S = [(P1 ! ll1'),e1] & S = [(P2 ! ll2'),e2] ) by A3, A4, Th9;
then A6: ( S `1 = <*P1*> ^ ll1' & S `1 = P1 ! ll1' & S `1 = <*P2*> ^ ll2' & S `1 = P2 ! ll2' ) by A5, MCART_1:7;
A7: S `1 is atomic by A1, Th11;
then P1 = the_pred_symbol_of (S `1 ) by A6, QC_LANG1:def 21
.= P2 by A6, A7, QC_LANG1:def 21 ;
hence ll1 = ll2 by A3, A4, A6, FINSEQ_1:46; :: thesis: verum