let f, g be Function; ( dom f = NAT & f . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = f . n & f . (n + 1) = Polish-expression-layer (P,A,U) ) ) & dom g = NAT & g . 0 = Polish-atoms (P,A) & ( for n being Nat ex U being Subset of (P *) st
( U = g . n & g . (n + 1) = Polish-expression-layer (P,A,U) ) ) implies f = g )
assume that
A1:
dom f = NAT
and
A2:
f . 0 = Polish-atoms (P,A)
and
A3:
for n being Nat ex U being Subset of (P *) st
( U = f . n & f . (n + 1) = Polish-expression-layer (P,A,U) )
and
A4:
dom g = NAT
and
A5:
g . 0 = Polish-atoms (P,A)
and
A6:
for n being Nat ex U being Subset of (P *) st
( U = g . n & g . (n + 1) = Polish-expression-layer (P,A,U) )
; f = g
defpred S1[ Nat] means f . $1 = g . $1;
A10:
S1[ 0 ]
by A2, A5;
A11:
for k being Nat st S1[k] holds
S1[k + 1]
for k being Nat holds S1[k]
from NAT_1:sch 2(A10, A11);
then
for a being object st a in dom f holds
f . a = g . a
by A1;
hence
f = g
by A1, A4, FUNCT_1:2; verum