let a be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))
let d be TypeSCNominativeData of V,A; :: thesis: for f being SCBinominativeFunction of V,A st a in V & d in dom f holds
NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))
let f be SCBinominativeFunction of V,A; :: thesis: ( a in V & d in dom f implies NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d)) )
set g = <*f*>;
set X = <*a*>;
assume A1: a in V ; :: thesis: ( not d in dom f or NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d)) )
assume d in dom f ; :: thesis: NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d))
then A2: f . d is TypeSCNominativeData of V,A by NOMIN_1:39, PARTFUN1:4;
rng (NDdataSeq (<*f*>,<*a*>,d)) = a .--> (f . d) by Th25;
hence NDentry (<*f*>,<*a*>,d) = naming (V,A,a,(f . d)) by A1, A2, NOMIN_1:def 13; :: thesis: verum