let ll1, ll2 be FinSequence of QC-variables A; :: thesis: ( ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( ll1 = ll & F = P ! ll ) & ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( ll2 = ll & F = P ! ll ) implies ll1 = ll2 )
given k1 being Nat, P1 being QC-pred_symbol of k1,A, ll19 being QC-variable_list of k1,A such that A2: ll1 = ll19 and
A3: F = P1 ! ll19 ; :: thesis: ( for k being Nat
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds
( not ll2 = ll or not F = P ! ll ) or ll1 = ll2 )
A4: F = <*P1*> ^ ll19 by A3, Th8;
given k2 being Nat, P2 being QC-pred_symbol of k2,A, ll29 being QC-variable_list of k2,A such that A5: ll2 = ll29 and
A6: F = P2 ! ll29 ; :: thesis: ll1 = ll2
A7: F = <*P2*> ^ ll29 by A6, Th8;
P1 = the_pred_symbol_of F by A1, A3, Def22
.= P2 by A1, A6, Def22 ;
hence ll1 = ll2 by A2, A5, A4, A7, FINSEQ_1:33; :: thesis: verum