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 A7: 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 A8: 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
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
A9: a = [k,h] by DOMAIN_1:1;
reconsider q = g . ((k + n),h) as Element of CQC-WFF ;
reconsider p = f . (k,h) as Element of CQC-WFF ;
F . (k,h) = p '&' q by A7
.= G . (k,h) by A8 ;
hence F . a = G . a by A9; :: thesis: verum

end;

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