let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2
for W1 being b1 -defined Walk of G1 holds (F .: W1) .edges() = (F _E) .: (W1 .edges())

let F be non empty PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds (F .: W1) .edges() = (F _E) .: (W1 .edges())
let W1 be F -defined Walk of G1; :: thesis: (F .: W1) .edges() = (F _E) .: (W1 .edges())
A1: (F .: W1) .edges() = rng ((F .: W1) .edgeSeq()) by GLIB_001:def 17
.= rng ((F _E) * ()) by Def37 ;
for y being object holds
( y in rng ((F _E) * ()) iff y in (F _E) .: (W1 .edges()) )
proof
let y be object ; :: thesis: ( y in rng ((F _E) * ()) iff y in (F _E) .: (W1 .edges()) )
hereby :: thesis: ( y in (F _E) .: (W1 .edges()) implies y in rng ((F _E) * ()) )
assume y in rng ((F _E) * ()) ; :: thesis: y in (F _E) .: (W1 .edges())
then consider x being object such that
A2: ( x in dom ((F _E) * ()) & ((F _E) * ()) . x = y ) by FUNCT_1:def 3;
set v = () . x;
x in dom () by ;
then (W1 .edgeSeq()) . x in rng () by FUNCT_1:3;
then A3: (W1 .edgeSeq()) . x in W1 .edges() by GLIB_001:def 17;
A4: (W1 .edgeSeq()) . x in dom (F _E) by ;
(F _E) . (() . x) = y by ;
hence y in (F _E) .: (W1 .edges()) by ; :: thesis: verum
end;
assume y in (F _E) .: (W1 .edges()) ; :: thesis: y in rng ((F _E) * ())
then consider v being object such that
A5: ( v in dom (F _E) & v in W1 .edges() & (F _E) . v = y ) by FUNCT_1:def 6;
v in rng () by ;
then consider x being object such that
A6: ( x in dom () & () . x = v ) by FUNCT_1:def 3;
A7: ((F _E) * ()) . x = y by ;
x in dom ((F _E) * ()) by ;
hence y in rng ((F _E) * ()) by ; :: thesis: verum
end;
hence (F .: W1) .edges() = (F _E) .: (W1 .edges()) by ; :: thesis: verum