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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in NDentry (<*f,g,h*>,<*a,b,c*>,d) or y in {[a,(f . d)],[b,(g . d)],[c,(h . d)]} )
assume y in NDentry (<*f,g,h*>,<*a,b,c*>,d) ; :: thesis: y in {[a,(f . d)],[b,(g . d)],[c,(h . d)]}
then consider z being object such that
A10: z in dom (NDdataSeq (<*f,g,h*>,<*a,b,c*>,d)) and
A11: (NDdataSeq (<*f,g,h*>,<*a,b,c*>,d)) . z = y by FUNCT_1:def 3;
( z = 1 or z = 2 or z = 3 ) by A1, A2, A10, ENUMSET1:def 1;
hence y in {[a,(f . d)],[b,(g . d)],[c,(h . d)]} by A4, A6, A8, A11, ENUMSET1:def 1; :: 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)],[c,(h . d)]} or [y,z] in NDentry (<*f,g,h*>,<*a,b,c*>,d) )
assume [y,z] in {[a,(f . d)],[b,(g . d)],[c,(h . d)]} ; :: thesis: [y,z] in NDentry (<*f,g,h*>,<*a,b,c*>,d)
then ( [y,z] = [a,(f . d)] or [y,z] = [b,(g . d)] or [y,z] = [c,(h . d)] ) by ENUMSET1:def 1;
hence [y,z] in NDentry (<*f,g,h*>,<*a,b,c*>,d) by A1, A2, A3, A4, A5, A6, A7, A8, FUNCT_1:def 3; :: thesis: verum