let f be Function; :: thesis: ( f is trivial implies f is one-to-one )

assume A1: f is trivial ; :: thesis: f is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A2: x1 in dom f and

A3: x2 in dom f and

f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider f = f as trivial Function by A1;

consider x being object such that

A4: dom f = {x} by A2, ZFMISC_1:131;

x1 = x by A2, A4, TARSKI:def 1;

hence x1 = x2 by A3, A4, TARSKI:def 1; :: thesis: verum

assume A1: f is trivial ; :: thesis: f is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A2: x1 in dom f and

A3: x2 in dom f and

f . x1 = f . x2 ; :: thesis: x1 = x2

reconsider f = f as trivial Function by A1;

consider x being object such that

A4: dom f = {x} by A2, ZFMISC_1:131;

x1 = x by A2, A4, TARSKI:def 1;

hence x1 = x2 by A3, A4, TARSKI:def 1; :: thesis: verum