let v be object ; :: thesis: for V, A being set
for f being SCBinominativeFunction of V,A st A is_without_nonatomicND_wrt V holds
for d being NonatomicND of V,A st v in V & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}
let V, A be set ; :: thesis: for f being SCBinominativeFunction of V,A st A is_without_nonatomicND_wrt V holds
for d being NonatomicND of V,A st v in V & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}
let f be SCBinominativeFunction of V,A; :: thesis: ( A is_without_nonatomicND_wrt V implies for d being NonatomicND of V,A st v in V & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v} )
assume A1: A is_without_nonatomicND_wrt V ; :: thesis: for d being NonatomicND of V,A st v in V & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}
let d be NonatomicND of V,A; :: thesis: ( v in V & d in dom f implies dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v} )
( not d in A & not naming (V,A,v,(f . d)) in A ) by A1, Th3;
hence ( v in V & d in dom f implies dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v} ) by NOMIN_2:33; :: thesis: verum