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

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, XTUPLE_0:1;
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 Def17; :: thesis: verum