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