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);

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

hence
isoR (x,o) is one-to-one
; :: thesis: verumx1 = 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_{1} = b_{2} )

assume A2: ( x1 in dom (isoR (x,o)) & x2 in dom (isoR (x,o)) & (isoR (x,o)) . x1 = (isoR (x,o)) . x2 ) ; :: thesis: b_{1} = b_{2}

end;assume A2: ( x1 in dom (isoR (x,o)) & x2 in dom (isoR (x,o)) & (isoR (x,o)) . x1 = (isoR (x,o)) . x2 ) ; :: thesis: b

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

end;

suppose A3:
x1 = x
; :: thesis: b_{1} = b_{2}

end;

now :: thesis: not x2 <> x

hence
x1 = x2
by A3; :: thesis: verumassume 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;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

suppose A5:
x1 <> x
; :: thesis: b_{1} = b_{2}

reconsider a = x1 as Element of F by A2;

A6: (isoR (x,o)) . a = a by A5, Def9;

end;A6: (isoR (x,o)) . a = a by A5, Def9;

now :: thesis: not x2 <> x1

hence
x1 = x2
; :: thesis: verumassume A7:
x2 <> x1
; :: thesis: contradiction

end;