let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for t, u being Element of L st rng (Polish-operation (L,E,t)) meets rng (Polish-operation (L,E,u)) holds
t = u
let E be Polish-arity-function of L; :: thesis: for t, u being Element of L st rng (Polish-operation (L,E,t)) meets rng (Polish-operation (L,E,u)) holds
t = u
let t, u be Element of L; :: thesis: ( rng (Polish-operation (L,E,t)) meets rng (Polish-operation (L,E,u)) implies t = u )
set f = Polish-operation (L,E,t);
set g = Polish-operation (L,E,u);
assume rng (Polish-operation (L,E,t)) meets rng (Polish-operation (L,E,u)) ; :: thesis: t = u
then not (rng (Polish-operation (L,E,t))) /\ (rng (Polish-operation (L,E,u))) is empty ;
then consider a being object such that
A2: a in (rng (Polish-operation (L,E,t))) /\ (rng (Polish-operation (L,E,u))) ;
A3: ( a in rng (Polish-operation (L,E,t)) & a in rng (Polish-operation (L,E,u)) ) by A2, XBOOLE_0:def 4;
consider b being object such that
A4: b in dom (Polish-operation (L,E,t)) and
A5: (Polish-operation (L,E,t)) . b = a by A3, FUNCT_1:def 3;
dom (Polish-operation (L,E,t)) = (Polish-WFF-set (L,E)) ^^ (E . t) by FUNCT_2:def 1;
then reconsider b = b as FinSequence by A4;
consider c being object such that
A6: c in dom (Polish-operation (L,E,u)) and
A7: (Polish-operation (L,E,u)) . c = a by A3, FUNCT_1:def 3;
dom (Polish-operation (L,E,u)) = (Polish-WFF-set (L,E)) ^^ (E . u) by FUNCT_2:def 1;
then reconsider c = c as FinSequence by A6;
t ^ b = (Polish-operation (L,E,t)) . b by A4, Def12
.= u ^ c by A5, A6, A7, Def12 ;
hence t = u by Th43; :: thesis: verum