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 k st
( ll1 = ll & F = P ! ll ) & ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( ll2 = ll & F = P ! ll ) implies ll1 = ll2 )
given k1 being Element of NAT , P1 being QC-pred_symbol of k1, ll19 being QC-variable_list of k1 such that A3: ll1 = ll19 and
A4: F = P1 ! ll19 ; :: thesis: ( for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds
( not ll2 = ll or not F = P ! ll ) or ll1 = ll2 )
A5: F = <*P1*> ^ ll19 by A4, Th23;
given k2 being Element of NAT , P2 being QC-pred_symbol of k2, ll29 being QC-variable_list of k2 such that A6: ll2 = ll29 and
A7: F = P2 ! ll29 ; :: thesis: ll1 = ll2
A8: F = <*P2*> ^ ll29 by A7, Th23;
P1 = the_pred_symbol_of F by A1, A4, Def21
.= P2 by A1, A7, Def21 ;
hence ll1 = ll2 by A3, A6, A5, A8, FINSEQ_1:46; :: thesis: verum