let a, b be object ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( {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 ) ; :: thesis: 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; :: thesis: verum