let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for W1 being b₁ -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