let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2

for W1 being b_{1} -defined Walk of G1

for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

let F be non empty PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1

for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

let W1 be F -defined Walk of G1; :: thesis: for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

let n be odd Element of NAT ; :: thesis: ( n <= len W1 implies (F _V) . (W1 . n) = (F .: W1) . n )

assume A1: n <= len W1 ; :: thesis: (F _V) . (W1 . n) = (F .: W1) . n

then A2: n <= len (F .: W1) by Th125;

A3: ( 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W1 .vertexSeq()) ) by A1, GLIB_001:68;

A4: (n + 1) div 2 in dom (W1 .vertexSeq()) by A3, FINSEQ_3:25;

W1 . n = W1 .vertexAt n by A1, GLIB_001:def 8

.= (W1 .vertexSeq()) . ((n + 1) div 2) by A1, GLIB_001:72 ;

hence (F _V) . (W1 . n) = ((F _V) * (W1 .vertexSeq())) . ((n + 1) div 2) by A4, FUNCT_1:13

.= ((F .: W1) .vertexSeq()) . ((n + 1) div 2) by Def37

.= (F .: W1) .vertexAt n by A2, GLIB_001:72

.= (F .: W1) . n by A2, GLIB_001:def 8 ;

:: thesis: verum

for W1 being b

for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

let F be non empty PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1

for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

let W1 be F -defined Walk of G1; :: thesis: for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

let n be odd Element of NAT ; :: thesis: ( n <= len W1 implies (F _V) . (W1 . n) = (F .: W1) . n )

assume A1: n <= len W1 ; :: thesis: (F _V) . (W1 . n) = (F .: W1) . n

then A2: n <= len (F .: W1) by Th125;

A3: ( 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W1 .vertexSeq()) ) by A1, GLIB_001:68;

A4: (n + 1) div 2 in dom (W1 .vertexSeq()) by A3, FINSEQ_3:25;

W1 . n = W1 .vertexAt n by A1, GLIB_001:def 8

.= (W1 .vertexSeq()) . ((n + 1) div 2) by A1, GLIB_001:72 ;

hence (F _V) . (W1 . n) = ((F _V) * (W1 .vertexSeq())) . ((n + 1) div 2) by A4, FUNCT_1:13

.= ((F .: W1) .vertexSeq()) . ((n + 1) div 2) by Def37

.= (F .: W1) .vertexAt n by A2, GLIB_001:72

.= (F .: W1) . n by A2, GLIB_001:def 8 ;

:: thesis: verum