let f be Function; :: thesis: for x, y being object st [x,y] in LinTrace f holds
( {x} in dom f & y in f . {x} )
let x, y be object ; :: 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 Th50;
hence ( {x} in dom f & y in f . {x} ) by Th31; :: thesis: verum