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

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