set R = Polish-expression-set (P,A);
set Q = (Polish-expression-set (P,A)) ^^ n;
let f, g be Function of ((Polish-expression-set (P,A)) ^^ n),(P *); :: thesis: ( ( for q being FinSequence st q in dom f holds
f . q = t ^ q ) & ( for q being FinSequence st q in dom g holds
g . q = t ^ q ) implies f = g )
assume that
A1: for q being FinSequence st q in dom f holds
f . q = t ^ q and
A2: for q being FinSequence st q in dom g holds
g . q = t ^ q ; :: thesis: f = g
A3: dom f = (Polish-expression-set (P,A)) ^^ n by FUNCT_2:def 1;
then A4: dom f = 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 A5: a in dom f ; :: thesis: f . a = g . a
then reconsider a = a as FinSequence by A3;
f . a = t ^ a by A1, A5
.= g . a by A2, A4, A5 ;
hence f . a = g . a ; :: thesis: verum

end;

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