let a be object ; :: thesis: for A being set
for V being non empty set
for v1, v2 being Element of V st a is TypeSCNominativeData of V,A holds
naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)
let A be set ; :: thesis: for V being non empty set
for v1, v2 being Element of V st a is TypeSCNominativeData of V,A holds
naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)
let V be non empty set ; :: thesis: for v1, v2 being Element of V st a is TypeSCNominativeData of V,A holds
naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)
let v1, v2 be Element of V; :: thesis: ( a is TypeSCNominativeData of V,A implies naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a) )
assume A1: a is TypeSCNominativeData of V,A ; :: thesis: naming (V,A,<*v1,v2*>,a) = v1 .--> (v2 .--> a)
set f = <*v1,v2*>;
set g = namingSeq (V,A,<*v1,v2*>,a);
A2: len <*v1,v2*> = 2 by FINSEQ_1:44;
A5: len (namingSeq (V,A,<*v1,v2*>,a)) = len <*v1,v2*> by Def14;
A6: (namingSeq (V,A,<*v1,v2*>,a)) . 1 is NonatomicND of V,A by A2, Th58;
A7: (namingSeq (V,A,<*v1,v2*>,a)) . 1 = naming (V,A,(<*v1,v2*> . (len <*v1,v2*>)),a) by Def14
.= v2 .--> a by A2, A1, Def13 ;
thus naming (V,A,<*v1,v2*>,a) = naming (V,A,(<*v1,v2*> . ((len <*v1,v2*>) - 1)),((namingSeq (V,A,<*v1,v2*>,a)) . 1)) by A2, A5, Def14
.= v1 .--> (v2 .--> a) by A2, A6, A7, Def13 ; :: thesis: verum