let f be Function; :: thesis: for x, y being set st [x,y] in LinTrace f holds
( {x} in dom f & y in f . {x} )
let x, y be set ; :: thesis: ( [x,y] in LinTrace f implies ( {x} in dom f & y in f . {x} ) )
assume [x,y] in LinTrace f ; :: thesis: ( {x} in dom f & y in f . {x} )
then [{x},y] in Trace f by Th51;
hence ( {x} in dom f & y in f . {x} ) by Th32; :: thesis: verum