let F be non almost_trivial Field; :: thesis: for x being non trivial Element of F
for o being object st not o in [#] F holds
isoR (x,o) is one-to-one
let x be non trivial Element of F; :: thesis: for o being object st not o in [#] F holds
isoR (x,o) is one-to-one
let o be object ; :: thesis: ( not o in [#] F implies isoR (x,o) is one-to-one )
assume not o in [#] F ; :: thesis: isoR (x,o) is one-to-one
then A1: for a being Element of F holds a <> o ;
set f = isoR (x,o);

now :: thesis: for x1, x2 being object st x1 in dom (isoR (x,o)) & x2 in dom (isoR (x,o)) & (isoR (x,o)) . x1 = (isoR (x,o)) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (isoR (x,o)) & x2 in dom (isoR (x,o)) & (isoR (x,o)) . x1 = (isoR (x,o)) . x2 implies b₁ = b₂ )
assume A2: ( x1 in dom (isoR (x,o)) & x2 in dom (isoR (x,o)) & (isoR (x,o)) . x1 = (isoR (x,o)) . x2 ) ; :: thesis: b₁ = b₂

per cases ( x1 = x or x1 <> x ) ;

suppose A3: x1 = x ; :: thesis: b₁ = b₂

now :: thesis: not x2 <> x

assume A4: x2 <> x ; :: thesis: contradiction
reconsider a = x2 as Element of F by A2;
a = (isoR (x,o)) . a by A4, Def9
.= o by A3, A2, Def9 ;
hence contradiction by A1; :: thesis: verum

end;

hence x1 = x2 by A3; :: thesis: verum

end;

suppose A5: x1 <> x ; :: thesis: b₁ = b₂

reconsider a = x1 as Element of F by A2;
A6: (isoR (x,o)) . a = a by A5, Def9;

now :: thesis: not x2 <> x1

assume A7: x2 <> x1 ; :: thesis: contradiction

per cases ( x2 = x or x2 <> x ) ;

suppose x2 = x ; :: thesis: contradiction

hence contradiction by A6, A1, A2, Def9; :: thesis: verum

end;

suppose A8: x2 <> x ; :: thesis: contradiction

reconsider b = x2 as Element of F by A2;
thus contradiction by A2, A6, A8, A7, Def9; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence isoR (x,o) is one-to-one ; :: thesis: verum