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

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