let f, g, h be Function; 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 ; 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;
A9:
( <*a,b,c*> . 1 = a & <*a,b,c*> . 2 = b & <*a,b,c*> . 3 = c & <*f,g,h*> . 1 = f & <*f,g,h*> . 2 = g & <*f,g,h*> . 3 = h )
by FINSEQ_1:45;
thus
NDentry (<*f,g,h*>,<*a,b,c*>,d) c= {[a,(f . d)],[b,(g . d)],[c,(h . d)]}
XBOOLE_0:def 10 {[a,(f . d)],[b,(g . d)],[c,(h . d)]} c= NDentry (<*f,g,h*>,<*a,b,c*>,d)proof
let y be
object ;
TARSKI:def 3 ( 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)
;
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, A9, A11, ENUMSET1:def 1;
verum
end;
let y, z be object ; RELAT_1:def 3 ( 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)]}
; [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, A9, FUNCT_1:def 3; verum