let T be Polish-language; for A being Polish-arity-function of T
for D being non empty set
for f being Polish-recursion-function of A,D
for K1, K2 being Function of (Polish-WFF-set (T,A)),D
for F being Polish-WFF of T,A st K1 is f -recursive & K2 is f -recursive & F in Polish-atoms (T,A) holds
K1 . F = K2 . F
let A be Polish-arity-function of T; for D being non empty set
for f being Polish-recursion-function of A,D
for K1, K2 being Function of (Polish-WFF-set (T,A)),D
for F being Polish-WFF of T,A st K1 is f -recursive & K2 is f -recursive & F in Polish-atoms (T,A) holds
K1 . F = K2 . F
let D be non empty set ; for f being Polish-recursion-function of A,D
for K1, K2 being Function of (Polish-WFF-set (T,A)),D
for F being Polish-WFF of T,A st K1 is f -recursive & K2 is f -recursive & F in Polish-atoms (T,A) holds
K1 . F = K2 . F
let f be Polish-recursion-function of A,D; for K1, K2 being Function of (Polish-WFF-set (T,A)),D
for F being Polish-WFF of T,A st K1 is f -recursive & K2 is f -recursive & F in Polish-atoms (T,A) holds
K1 . F = K2 . F
let K1, K2 be Function of (Polish-WFF-set (T,A)),D; for F being Polish-WFF of T,A st K1 is f -recursive & K2 is f -recursive & F in Polish-atoms (T,A) holds
K1 . F = K2 . F
let F be Polish-WFF of T,A; ( K1 is f -recursive & K2 is f -recursive & F in Polish-atoms (T,A) implies K1 . F = K2 . F )
assume that
A1:
K1 is f -recursive
and
A2:
K2 is f -recursive
and
A3:
F in Polish-atoms (T,A)
; K1 . F = K2 . F
F in T
by A3, Def9;
then A5:
Polish-WFF-head F = F
by Th18;
then
Polish-arity F = 0
by A3, Def9;
then
Polish-WFF-args F = {}
by Th51;
then
( K1 . F = f . [F,(K1 * {})] & K2 . F = f . [F,(K2 * {})] )
by A1, A2, A5;
hence
K1 . F = K2 . F
; verum