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 even Element of NAT st 1 <= n & n <= len W1 holds

(F _E) . (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 even Element of NAT st 1 <= n & n <= len W1 holds

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

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

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

let n be even Element of NAT ; :: thesis: ( 1 <= n & n <= len W1 implies (F _E) . (W1 . n) = (F .: W1) . n )

assume A1: ( 1 <= n & n <= len W1 ) ; :: thesis: (F _E) . (W1 . n) = (F .: W1) . n

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

A3: ( n div 2 in dom (W1 .edgeSeq()) & W1 . n = (W1 .edgeSeq()) . (n div 2) ) by A1, GLIB_001:77;

thus (F _E) . (W1 . n) = ((F _E) * (W1 .edgeSeq())) . (n div 2) by A3, FUNCT_1:13

.= ((F .: W1) .edgeSeq()) . (n div 2) by Def37

.= (F .: W1) . n by A1, A2, GLIB_001:77 ; :: thesis: verum

for W1 being b

for n being even Element of NAT st 1 <= n & n <= len W1 holds

(F _E) . (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 even Element of NAT st 1 <= n & n <= len W1 holds

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

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

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

let n be even Element of NAT ; :: thesis: ( 1 <= n & n <= len W1 implies (F _E) . (W1 . n) = (F .: W1) . n )

assume A1: ( 1 <= n & n <= len W1 ) ; :: thesis: (F _E) . (W1 . n) = (F .: W1) . n

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

A3: ( n div 2 in dom (W1 .edgeSeq()) & W1 . n = (W1 .edgeSeq()) . (n div 2) ) by A1, GLIB_001:77;

thus (F _E) . (W1 . n) = ((F _E) * (W1 .edgeSeq())) . (n div 2) by A3, FUNCT_1:13

.= ((F .: W1) .edgeSeq()) . (n div 2) by Def37

.= (F .: W1) . n by A1, A2, GLIB_001:77 ; :: thesis: verum