let f, g be Function; :: thesis: for a, b, d being object holds NDentry (<*f,g*>,<*a,b*>,d) = {[a,(f . d)],[b,(g . d)]}
let a, b, d be object ; :: thesis: NDentry (<*f,g*>,<*a,b*>,d) = {[a,(f . d)],[b,(g . d)]}
set X = <*a,b*>;
set G = <*f,g*>;
set A = {[a,(f . d)],[b,(g . d)]};
set N = NDdataSeq (<*f,g*>,<*a,b*>,d);
set F = NDentry (<*f,g*>,<*a,b*>,d);
A1: dom (NDdataSeq (<*f,g*>,<*a,b*>,d)) = dom <*a,b*> by Def4;
A2: dom <*a,b*> = {1,2} by FINSEQ_1:92;
A3: 1 in {1,2} by TARSKI:def 2;
then A4: (NDdataSeq (<*f,g*>,<*a,b*>,d)) . 1 = [(<*a,b*> . 1),((<*f,g*> . 1) . d)] by A2, Def4;
A5: 2 in {1,2} by TARSKI:def 2;
then A6: (NDdataSeq (<*f,g*>,<*a,b*>,d)) . 2 = [(<*a,b*> . 2),((<*f,g*> . 2) . d)] by A2, Def4;
thus NDentry (<*f,g*>,<*a,b*>,d) c= {[a,(f . d)],[b,(g . d)]} :: according to XBOOLE_0:def 10 :: thesis: {[a,(f . d)],[b,(g . d)]} c= NDentry (<*f,g*>,<*a,b*>,d)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in NDentry (<*f,g*>,<*a,b*>,d) or y in {[a,(f . d)],[b,(g . d)]} )
assume y in NDentry (<*f,g*>,<*a,b*>,d) ; :: thesis: y in {[a,(f . d)],[b,(g . d)]}
then consider z being object such that
A8: z in dom (NDdataSeq (<*f,g*>,<*a,b*>,d)) and
A9: (NDdataSeq (<*f,g*>,<*a,b*>,d)) . z = y by FUNCT_1:def 3;
( z = 1 or z = 2 ) by A1, A2, A8, TARSKI:def 2;
hence y in {[a,(f . d)],[b,(g . d)]} by A4, A6, A9, TARSKI:def 2; :: thesis: verum

end;

let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in {[a,(f . d)],[b,(g . d)]} or [y,z] in NDentry (<*f,g*>,<*a,b*>,d) )
assume [y,z] in {[a,(f . d)],[b,(g . d)]} ; :: thesis: [y,z] in NDentry (<*f,g*>,<*a,b*>,d)
then ( [y,z] = [a,(f . d)] or [y,z] = [b,(g . d)] ) by TARSKI:def 2;
hence [y,z] in NDentry (<*f,g*>,<*a,b*>,d) by A1, A2, A3, A4, A5, A6, FUNCT_1:def 3; :: thesis: verum