let f be Function; :: thesis: ( f . {} = {} implies for x, y being object st {x} in dom f & y in f . {x} holds
[x,y] in LinTrace f )
assume A1: f . {} = {} ; :: thesis: for x, y being object st {x} in dom f & y in f . {x} holds
[x,y] in LinTrace f
let x, y be object ; :: thesis: ( {x} in dom f & y in f . {x} implies [x,y] in LinTrace f )
set a = {x};
( [x,y] in LinTrace f iff [{x},y] in Trace f ) by Th50;
then ( [x,y] in LinTrace f iff ( {x} in dom f & y in f . {x} & ( for b being set st b in dom f & b c= {x} & y in f . b holds
{x} = b ) ) ) by Th31;
hence ( {x} in dom f & y in f . {x} implies [x,y] in LinTrace f ) by A1, ZFMISC_1:33; :: thesis: verum