set W = Polish-WFF-set (L,E);
set R = Polish-recursion-domain (E,(Polish-WFF-set (L,E)));
let f, g be Function of (Polish-recursion-domain (E,(Polish-WFF-set (L,E)))),(Polish-WFF-set (L,E)); :: thesis: ( ( for t being Element of L
for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds
( ( t in dom s implies f . (t,p) = s . t ) & ( not t in dom s implies f . (t,p) = t ^ (FlattenSeq p) ) ) ) & ( for t being Element of L
for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds
( ( t in dom s implies g . (t,p) = s . t ) & ( not t in dom s implies g . (t,p) = t ^ (FlattenSeq p) ) ) ) implies f = g )
assume that
A1: for t being Element of L
for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds
( ( t in dom s implies f . (t,p) = s . t ) & ( not t in dom s implies f . (t,p) = t ^ (FlattenSeq p) ) ) and
A2: for t being Element of L
for p being FinSequence of Polish-WFF-set (L,E) st len p = E . t holds
( ( t in dom s implies g . (t,p) = s . t ) & ( not t in dom s implies g . (t,p) = t ^ (FlattenSeq p) ) ) ; :: thesis: f = g
A3: dom f = Polish-recursion-domain (E,(Polish-WFF-set (L,E))) by FUNCT_2:def 1
.= dom g by FUNCT_2:def 1 ;
for a being object st a in dom f holds
f . a = g . a

proof

let a be object ; :: thesis: ( a in dom f implies f . a = g . a )
assume a in dom f ; :: thesis: f . a = g . a
then a in Polish-recursion-domain (E,(Polish-WFF-set (L,E))) by FUNCT_2:def 1;
then consider t being Element of L, p being FinSequence of Polish-WFF-set (L,E) such that
A6: a = [t,p] and
A7: len p = E . t ;
A8: f . a = f . (t,p) by A6, BINOP_1:def 1;
A9: g . a = g . (t,p) by A6, BINOP_1:def 1;

per cases ( t in dom s or not t in dom s ) ;

suppose A20: t in dom s ; :: thesis: f . a = g . a

hence f . a = s . t by A1, A7, A8
.= g . a by A2, A7, A9, A20 ;
:: thesis: verum

end;

suppose A22: not t in dom s ; :: thesis: f . a = g . a

hence f . a = t ^ (FlattenSeq p) by A1, A7, A8
.= g . a by A2, A7, A9, A22 ;
:: thesis: verum

end;

end;

end;

hence f = g by A3, FUNCT_1:2; :: thesis: verum