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 a9, y9 be set ; :: thesis: ( [a9,y9] in Trace f iff ( a9 in dom f & y9 in f . a9 & ( for b being set st b in dom f & b c= a9 & y9 in f . b holds
a9 = b ) ) )

now

given a, y being set such that A1: [a9,y9] = [a,y] and
A2: ( 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: ( a9 in dom f & y9 in f . a9 & ( for b being set st b in dom f & b c= a9 & y9 in f . b holds
a9 = b ) )
( a9 = a & y9 = y ) by A1, ZFMISC_1:33;
hence ( a9 in dom f & y9 in f . a9 & ( for b being set st b in dom f & b c= a9 & y9 in f . b holds
a9 = b ) ) by A2; :: thesis: verum

end;

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