set f = NDdataSeq (g,X,d);
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in NDentry (g,X,d) or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in NDentry (g,X,d) ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then consider z being object such that
A1: z in dom (NDdataSeq (g,X,d)) and
A2: (NDdataSeq (g,X,d)) . z = x by FUNCT_1:def 3;
dom (NDdataSeq (g,X,d)) = dom X by Def4;
then (NDdataSeq (g,X,d)) . z = [(X . z),((g . z) . d)] by A1, Def4;
hence ex b₁, b₂ being object st x = [b₁,b₂] by A2; :: thesis: verum