set f = NDdataSeq (g,X,d);
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in NDentry (g,X,d) or not [x,y2] in NDentry (g,X,d) or y1 = y2 )
assume that
A1: [x,y1] in NDentry (g,X,d) and
A2: [x,y2] in NDentry (g,X,d) ; :: thesis: y1 = y2
consider a being object such that
A3: a in dom (NDdataSeq (g,X,d)) and
A4: (NDdataSeq (g,X,d)) . a = [x,y1] by A1, FUNCT_1:def 3;
consider b being object such that
A5: b in dom (NDdataSeq (g,X,d)) and
A6: (NDdataSeq (g,X,d)) . b = [x,y2] by A2, FUNCT_1:def 3;
A7: dom (NDdataSeq (g,X,d)) = dom X by Def4;
A8: (NDdataSeq (g,X,d)) . a = [(X . a),((g . a) . d)] by A3, A7, Def4;
(NDdataSeq (g,X,d)) . b = [(X . b),((g . b) . d)] by A5, A7, Def4;
then ( x = X . a & x = X . b ) by A4, A6, A8, XTUPLE_0:1;
then a = b by A3, A5, A7, FUNCT_1:def 4;
hence y1 = y2 by A4, A6, XTUPLE_0:1; :: thesis: verum