let f be Function; :: thesis: for a, y being set holds
( [a,y] in Trace f iff ( a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) )
let a', y' be set ; :: thesis: ( [a',y'] in Trace f iff ( a' in dom f & y' in f . a' & ( for b being set st b in dom f & b c= a' & y' in f . b holds
a' = b ) ) )

now

given a, y being set such that A1: ( [a',y'] = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) ; :: thesis: ( a' in dom f & y' in f . a' & ( for b being set st b in dom f & b c= a' & y' in f . b holds
a' = b ) )
( a' = a & y' = y ) by A1, ZFMISC_1:33;
hence ( a' in dom f & y' in f . a' & ( for b being set st b in dom f & b c= a' & y' in f . b holds
a' = b ) ) by A1; :: thesis: verum

end;

hence ( [a',y'] in Trace f iff ( a' in dom f & y' in f . a' & ( for b being set st b in dom f & b c= a' & y' in f . b holds
a' = b ) ) ) by Def18; :: thesis: verum