let f be Function; :: thesis: for a, d being object holds NDentry (<*f*>,<*a*>,d) = {[a,(f . d)]}
let a, d be object ; :: thesis: NDentry (<*f*>,<*a*>,d) = {[a,(f . d)]}
set X = <*a*>;
set G = <*f*>;
set A = {[a,(f . d)]};
set N = NDdataSeq (<*f*>,<*a*>,d);
set F = NDentry (<*f*>,<*a*>,d);
A1: dom (NDdataSeq (<*f*>,<*a*>,d)) = dom <*a*> by Def4;
A2: dom <*a*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A3: 1 in {1} by TARSKI:def 1;
then A4: (NDdataSeq (<*f*>,<*a*>,d)) . 1 = [(<*a*> . 1),((<*f*> . 1) . d)] by A2, Def4;
A5: ( <*a*> . 1 = a & <*f*> . 1 = f ) by FINSEQ_1:40;
thus NDentry (<*f*>,<*a*>,d) c= {[a,(f . d)]} :: according to XBOOLE_0:def 10 :: thesis: {[a,(f . d)]} c= NDentry (<*f*>,<*a*>,d)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in NDentry (<*f*>,<*a*>,d) or y in {[a,(f . d)]} )
assume y in NDentry (<*f*>,<*a*>,d) ; :: thesis: y in {[a,(f . d)]}
then consider z being object such that
A6: z in dom (NDdataSeq (<*f*>,<*a*>,d)) and
A7: (NDdataSeq (<*f*>,<*a*>,d)) . z = y by FUNCT_1:def 3;
z = 1 by A1, A2, A6, TARSKI:def 1;
hence y in {[a,(f . d)]} by A4, A5, A7, TARSKI:def 1; :: thesis: verum
end;
let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in {[a,(f . d)]} or [y,z] in NDentry (<*f*>,<*a*>,d) )
assume [y,z] in {[a,(f . d)]} ; :: thesis: [y,z] in NDentry (<*f*>,<*a*>,d)
then [y,z] = [a,(f . d)] by TARSKI:def 1;
hence [y,z] in NDentry (<*f*>,<*a*>,d) by A1, A2, A3, A4, A5, FUNCT_1:def 3; :: thesis: verum