let v be object ; :: thesis: for V, A being set
for D being TypeSCNominativeData of V,A st v in V holds
denaming (v,(naming (V,A,v,D))) = D
let V, A be set ; :: thesis: for D being TypeSCNominativeData of V,A st v in V holds
denaming (v,(naming (V,A,v,D))) = D
let D be TypeSCNominativeData of V,A; :: thesis: ( v in V implies denaming (v,(naming (V,A,v,D))) = D )
assume A1: v in V ; :: thesis: denaming (v,(naming (V,A,v,D))) = D
naming (V,A,v,D) = v .--> D by A1, Def13;
then v in dom (naming (V,A,v,D)) by TARSKI:def 1;
hence denaming (v,(naming (V,A,v,D))) = (naming (V,A,v,D)) . v by Def12
.= (v .--> D) . v by A1, Def13
.= D by FUNCOP_1:72 ;
:: thesis: verum