let a be object ; :: thesis: for A being set
for V being non empty set
for v being Element of V holds naming (V,A,<*v*>,a) = naming (V,A,v,a)
let A be set ; :: thesis: for V being non empty set
for v being Element of V holds naming (V,A,<*v*>,a) = naming (V,A,v,a)
let V be non empty set ; :: thesis: for v being Element of V holds naming (V,A,<*v*>,a) = naming (V,A,v,a)
let v be Element of V; :: thesis: naming (V,A,<*v*>,a) = naming (V,A,v,a)
set f = <*v*>;
A1: ( len <*v*> = 1 & <*v*> . 1 = v ) by FINSEQ_1:40;
len (namingSeq (V,A,<*v*>,a)) = len <*v*> by Def14;
hence naming (V,A,<*v*>,a) = naming (V,A,v,a) by A1, Def14; :: thesis: verum