let v be object ; :: thesis: for V, A being set
for D being NonatomicND of V,A st v in dom D holds
naming (V,A,v,(denaming (v,D))) = v .--> (D . v)
let V, A be set ; :: thesis: for D being NonatomicND of V,A st v in dom D holds
naming (V,A,v,(denaming (v,D))) = v .--> (D . v)
let D be NonatomicND of V,A; :: thesis: ( v in dom D implies naming (V,A,v,(denaming (v,D))) = v .--> (D . v) )
assume A1: v in dom D ; :: thesis: naming (V,A,v,(denaming (v,D))) = v .--> (D . v)
ex n being Nat st D is TypeSSNominativeData of V,(A \/ ((FNDSC (V,A)) . n)) by Th33;
then dom D c= V by RELAT_1:def 18;
hence naming (V,A,v,(denaming (v,D))) = v .--> (denaming (v,D)) by A1, Def13
.= v .--> (D . v) by A1, Def12 ;
:: thesis: verum