let f, g be Function; :: thesis: ( 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) ) ; :: thesis: f = g
defpred S₁[ Nat] means f . $1 = g . $1;
A10: S₁[ 0 ] by A2, A5;
A11: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]
consider U being Subset of (P *) such that
A13: U = f . k and
A14: f . (k + 1) = Polish-expression-layer (P,A,U) by A3;
consider V being Subset of (P *) such that
A15: V = g . k and
A16: g . (k + 1) = Polish-expression-layer (P,A,V) by A6;
thus S₁[k + 1] by A12, A13, A14, A15, A16; :: thesis: verum

end;

for k being Nat holds S₁[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; :: thesis: verum