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