let A, B be Polish-arity-function of T; :: thesis: ( V = Polish-WFF-set (T,A) & V = Polish-WFF-set (T,B) implies A = B )
assume that
A1: V = Polish-WFF-set (T,A) and
A2: V = Polish-WFF-set (T,B) ; :: thesis: A = B
for a being object st a in T holds
A . a = B . a

proof

let a be object ; :: thesis: ( a in T implies A . a = B . a )
assume a in T ; :: thesis: A . a = B . a
then reconsider t = a as Element of T ;

per cases ( T is trivial or not T is trivial ) ;

suppose T is trivial ; :: thesis: A . a = B . a

then ( A . t = 0 & B . t = 0 ) by Lm5;
hence A . a = B . a ; :: thesis: verum

end;

suppose A20: not T is trivial ; :: thesis: A . a = B . a

set n = A . t;
set u = the Element of V ^^ (A . t);
set F = t ^ the Element of V ^^ (A . t);
t ^ the Element of V ^^ (A . t) in V by A1, Lm4;
then ( the Element of V ^^ (A . t) in V ^^ (B . t) & the Element of V ^^ (A . t) in V ^^ (A . t) ) by A2, Lm4;
hence A . a = B . a by A1, A20, Lm3; :: thesis: verum

end;

end;

end;

hence A = B by FUNCT_2:12; :: thesis: verum