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) * (W1 .edgeSeq())) by Def37 ;
for y being object holds
( y in rng ((F _E) * (W1 .edgeSeq())) iff y in (F _E) .: (W1 .edges()) )
proof
let y be object ; :: thesis: ( y in rng ((F _E) * (W1 .edgeSeq())) iff y in (F _E) .: (W1 .edges()) )
hereby :: thesis: ( y in (F _E) .: (W1 .edges()) implies y in rng ((F _E) * (W1 .edgeSeq())) )
assume y in rng ((F _E) * (W1 .edgeSeq())) ; :: thesis: y in (F _E) .: (W1 .edges())
then consider x being object such that
A2: ( x in dom ((F _E) * (W1 .edgeSeq())) & ((F _E) * (W1 .edgeSeq())) . x = y ) by FUNCT_1:def 3;
set v = (W1 .edgeSeq()) . x;
x in dom (W1 .edgeSeq()) by A2, FUNCT_1:11;
then (W1 .edgeSeq()) . x in rng (W1 .edgeSeq()) 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 A2, FUNCT_1:11;
(F _E) . ((W1 .edgeSeq()) . x) = y by A2, FUNCT_1:12;
hence y in (F _E) .: (W1 .edges()) by A3, A4, FUNCT_1:def 6; :: thesis: verum
end;
assume y in (F _E) .: (W1 .edges()) ; :: thesis: y in rng ((F _E) * (W1 .edgeSeq()))
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 (W1 .edgeSeq()) by A5, GLIB_001:def 17;
then consider x being object such that
A6: ( x in dom (W1 .edgeSeq()) & (W1 .edgeSeq()) . x = v ) by FUNCT_1:def 3;
A7: ((F _E) * (W1 .edgeSeq())) . x = y by A5, A6, FUNCT_1:13;
x in dom ((F _E) * (W1 .edgeSeq())) by A5, A6, FUNCT_1:11;
hence y in rng ((F _E) * (W1 .edgeSeq())) by A7, FUNCT_1:3; :: thesis: verum
end;
hence (F .: W1) .edges() = (F _E) .: (W1 .edges()) by A1, TARSKI:2; :: thesis: verum