let a, b, c be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for f, g, h being SCBinominativeFunction of V,A st {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h holds
NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for f, g, h being SCBinominativeFunction of V,A st {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h holds
NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A
let d be TypeSCNominativeData of V,A; :: thesis: for f, g, h being SCBinominativeFunction of V,A st {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h holds
NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A
let f, g, h be SCBinominativeFunction of V,A; :: thesis: ( {a,b,c} c= V & a,b,c are_mutually_distinct & d in dom f & d in dom g & d in dom h implies NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A )
assume that
A1: {a,b,c} c= V and
A2: a,b,c are_mutually_distinct and
A3: ( d in dom f & d in dom g & d in dom h ) ; :: thesis: NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A
reconsider O = <*a,b,c*> as one-to-one FinSequence by A2, FINSEQ_3:95;
set F = NDentry (<*f,g,h*>,O,d);
A4: NDentry (<*f,g,h*>,O,d) = {[a,(f . d)],[b,(g . d)],[c,(h . d)]} by Th23;
then A5: dom (NDentry (<*f,g,h*>,O,d)) = {a,b,c} by Th2;
A6: rng (NDentry (<*f,g,h*>,O,d)) = {(f . d),(g . d),(h . d)} by A4, Th3;
( f . d in ND (V,A) & g . d in ND (V,A) & h . d in ND (V,A) ) by A3, PARTFUN1:4;
then rng (NDentry (<*f,g,h*>,O,d)) c= ND (V,A) by A6, Th1;
hence NDentry (<*f,g,h*>,<*a,b,c*>,d) is NonatomicND of V,A by A1, A5, Th6; :: thesis: verum