let F, G be Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF); :: thesis: ( ( for n being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds F . (n,h) = P ! (h * l) ) & ( for n being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds G . (n,h) = P ! (h * l) ) implies F = G )
assume A2: for n being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds F . (n,h) = P ! (h * l) ; :: thesis: ( ex n being Element of NAT ex h being Element of Funcs (bound_QC-variables,bound_QC-variables) st not G . (n,h) = P ! (h * l) or F = G )
assume A3: for n being Element of NAT
for h being Element of Funcs (bound_QC-variables,bound_QC-variables) holds G . (n,h) = P ! (h * l) ; :: thesis: F = G
for a being Element of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] holds F . a = G . a

proof

let a be Element of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):]; :: thesis: F . a = G . a
consider k being Element of NAT , f being Element of Funcs (bound_QC-variables,bound_QC-variables) such that
A4: a = [k,f] by DOMAIN_1:1;
F . (k,f) = P ! (f * l) by A2
.= G . (k,f) by A3 ;
hence F . a = G . a by A4; :: thesis: verum

end;

hence F = G by FUNCT_2:63; :: thesis: verum