let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for t being Element of L holds Polish-operation (L,E,t) is one-to-one
let E be Polish-arity-function of L; :: thesis: for t being Element of L holds Polish-operation (L,E,t) is one-to-one
let t be Element of L; :: thesis: Polish-operation (L,E,t) is one-to-one
set f = Polish-operation (L,E,t);
for a, b being object st a in dom (Polish-operation (L,E,t)) & b in dom (Polish-operation (L,E,t)) & (Polish-operation (L,E,t)) . a = (Polish-operation (L,E,t)) . b holds
a = b

proof

let a, b be object ; :: thesis: ( a in dom (Polish-operation (L,E,t)) & b in dom (Polish-operation (L,E,t)) & (Polish-operation (L,E,t)) . a = (Polish-operation (L,E,t)) . b implies a = b )
assume that
A1: a in dom (Polish-operation (L,E,t)) and
A2: b in dom (Polish-operation (L,E,t)) and
A3: (Polish-operation (L,E,t)) . a = (Polish-operation (L,E,t)) . b ; :: thesis: a = b
A4: dom (Polish-operation (L,E,t)) = (Polish-WFF-set (L,E)) ^^ (E . t) by FUNCT_2:def 1;
reconsider a1 = a as FinSequence by A1, A4;
reconsider b1 = b as FinSequence by A2, A4;
t ^ a1 = (Polish-operation (L,E,t)) . a1 by A1, Def12
.= t ^ b1 by A2, A3, Def12 ;
hence a = b by FINSEQ_1:33; :: thesis: verum

end;

hence Polish-operation (L,E,t) is one-to-one by FUNCT_1:def 4; :: thesis: verum