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