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 set ; :: according to FUNCT_1:def 8 :: 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 & x2 in dom f ) and
f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider f = f as trivial Function by A1;
consider x being set such that
A3: dom f = {x} by A2, REALSET1:def 4;
( x1 = x & x2 = x ) by A2, A3, TARSKI:def 1;
hence x1 = x2 ; :: thesis: verum