let ll1, ll2 be FinSequence of QC-variables A; ( 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
; ( 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
; 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; verum