let a be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A
let d be TypeSCNominativeData of V,A; :: thesis: for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A
let f be SCBinominativeFunction of V,A; :: thesis: ( a in V & d in dom f implies NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A )
assume ( a in V & d in dom f ) ; :: thesis: NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A
then NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d)) by Th26;
hence NDentry (<*f*>,<*a*>,d) is NonatomicND of V,A ; :: thesis: verum