let F, G be Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ; :: thesis: ( ( for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . k,h & q = g . (k + n),h holds
F . k,h = p '&' q ) & ( for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . k,h & q = g . (k + n),h holds
G . k,h = p '&' q ) implies F = G )
assume A3: for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . k,h & q = g . (k + n),h holds
F . k,h = p '&' q ; :: thesis: ( ex k being Element of NAT ex h being Element of Funcs bound_QC-variables ,bound_QC-variables ex p, q being Element of CQC-WFF st
( p = f . k,h & q = g . (k + n),h & not G . k,h = p '&' q ) or F = G )
assume A4: for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . k,h & q = g . (k + n),h holds
G . k,h = p '&' q ; :: 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 , h being Element of Funcs bound_QC-variables ,bound_QC-variables such that
A5: a = [k,h] by DOMAIN_1:9;
reconsider p = f . k,h as Element of CQC-WFF ;
reconsider q = g . (k + n),h as Element of CQC-WFF ;
F . k,h = p '&' q by A3
.= G . k,h by A4 ;
hence F . a = G . a by A5; :: thesis: verum

end;

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

end;