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

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