let a be object ; 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 ; 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; 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; ( 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 )
; 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
; verum