let P1, P2 be QC-pred_symbol of A; :: thesis: ( ex k being Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( P1 = P & F = P ! ll ) & ex k being Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( P2 = P & F = P ! ll ) implies P1 = P2 )
given k1 being Nat, ll1 being QC-variable_list of k1,A, P19 being QC-pred_symbol of k1,A such that A2: ( P1 = P19 & F = P19 ! ll1 ) ; :: thesis: ( for k being Nat
for ll being QC-variable_list of k,A
for P being QC-pred_symbol of k,A holds
( not P2 = P or not F = P ! ll ) or P1 = P2 )
given k2 being Nat, ll2 being QC-variable_list of k2,A, P29 being QC-pred_symbol of k2,A such that A3: ( P2 = P29 & F = P29 ! ll2 ) ; :: thesis: P1 = P2
A4: <*P1*> ^ ll1 = F by A2, Th8
.= <*P2*> ^ ll2 by A3, Th8 ;
thus P1 = (<*P1*> ^ ll1) . 1 by FINSEQ_1:41
.= P2 by A4, FINSEQ_1:41 ; :: thesis: verum