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 b1 = b2 )
assume A2: ( x1 in dom (isoR (x,o)) & x2 in dom (isoR (x,o)) & (isoR (x,o)) . x1 = (isoR (x,o)) . x2 ) ; :: thesis: b1 = b2
per cases ( x1 = x or x1 <> x ) ;
suppose A3: x1 = x ; :: thesis: b1 = b2
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: b1 = b2
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 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