let v be object ; :: thesis: for V, A being set
for f being SCBinominativeFunction of V,A
for d being NonatomicND of V,A st v in V & not d in A & not naming (V,A,v,(f . d)) in A & 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
for d being NonatomicND of V,A st v in V & not d in A & not naming (V,A,v,(f . d)) in A & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}
let f be SCBinominativeFunction of V,A; :: thesis: for d being NonatomicND of V,A st v in V & not d in A & not naming (V,A,v,(f . d)) in A & d in dom f holds
dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}
set a = SC_assignment (f,v);
let d be NonatomicND of V,A; :: thesis: ( v in V & not d in A & not naming (V,A,v,(f . d)) in A & d in dom f implies dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v} )
assume that
A1: ( v in V & not d in A & not naming (V,A,v,(f . d)) in A ) and
A2: d in dom f ; :: thesis: dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v}
A3: dom (SC_assignment (f,v)) = dom f by Def7;
reconsider d1 = d as TypeSCNominativeData of V,A ;
reconsider d2 = f . d1 as TypeSCNominativeData of V,A by A2, PARTFUN1:4, NOMIN_1:39;
dom (local_overlapping (V,A,d,d2,v)) = {v} \/ (dom d) by A1, Th14;
hence dom ((SC_assignment (f,v)) . d) = (dom d) \/ {v} by A2, A3, Def7; :: thesis: verum