set W = Polish-WFF-set (T,A);
let f, g be Function of [:(Polish-WFF-set (T,A)),(Polish-WFF-set (T,A)):],(Polish-WFF-set (T,A)); :: thesis: ( ( for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds
f . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ) & ( for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds
g . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ) implies f = g )
assume that
A10: for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds
f . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) and
A11: for u, v being FinSequence st u in Polish-WFF-set (T,A) & v in Polish-WFF-set (T,A) holds
g . (u,v) = (Polish-operation (T,A,t)) . (u ^ v) ; :: thesis: f = g
A12: dom f = [:(Polish-WFF-set (T,A)),(Polish-WFF-set (T,A)):] by FUNCT_2:def 1;
A13: dom g = [:(Polish-WFF-set (T,A)),(Polish-WFF-set (T,A)):] by FUNCT_2:def 1;
for a, b being object st a in Polish-WFF-set (T,A) & b in Polish-WFF-set (T,A) holds
f . (a,b) = g . (a,b)

proof

let a, b be object ; :: thesis: ( a in Polish-WFF-set (T,A) & b in Polish-WFF-set (T,A) implies f . (a,b) = g . (a,b) )
assume that
A20: a in Polish-WFF-set (T,A) and
A21: b in Polish-WFF-set (T,A) ; :: thesis: f . (a,b) = g . (a,b)
reconsider u = a as FinSequence by A20;
reconsider v = b as FinSequence by A21;
thus f . (a,b) = (Polish-operation (T,A,t)) . (u ^ v) by A10, A20, A21
.= g . (a,b) by A11, A20, A21 ; :: thesis: verum

end;

hence f = g by A12, A13, FUNCT_3:6; :: thesis: verum