let F, G be Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)); :: thesis: ( ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds F . (t,h) = P ! (h * l) ) & ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds G . (t,h) = P ! (h * l) ) implies F = G )
assume A2: for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds F . (t,h) = P ! (h * l) ; :: thesis: ( ex t being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st not G . (t,h) = P ! (h * l) or F = G )
assume A3: for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds G . (t,h) = P ! (h * l) ; :: thesis: F = G
for a being Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds F . a = G . a
proof
let a be Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]; :: thesis: F . a = G . a
consider k being Element of QC-symbols A, f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) 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