let L be non trivial Polish-language; 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; for t being Element of L holds Polish-operation (L,E,t) is one-to-one
let t be Element of L; 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 ;
( 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
;
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, Def13
.=
t ^ b1
by A2, A3, Def13
;
hence
a = b
by FINSEQ_1:33;
verum
end;
hence
Polish-operation (L,E,t) is one-to-one
by FUNCT_1:def 4; verum