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
thus F = G :: thesis: verum

proof

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:9;
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:113; :: thesis: verum

end;