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