let T be Polish-language; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: K1 . F = K2 . F
F in T by A3, Def7;
then A5: Polish-WFF-head F = F by Th53;
then Polish-arity F = 0 by A3, Def7;
then Polish-WFF-args F = {} by Th61;
then ( K1 . F = f . [F,(K1 * {})] & K2 . F = f . [F,(K2 * {})] ) by A1, A2, A5;
hence K1 . F = K2 . F ; :: thesis: verum