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

for W1 being b_{1} -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()) )

for W1 being b

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

hence
(F .: W1) .edges() = (F _E) .: (W1 .edges())
by A1, TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in rng ((F _E) * (W1 .edgeSeq())) iff y in (F _E) .: (W1 .edges()) )

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;hereby :: thesis: ( y in (F _E) .: (W1 .edges()) implies y in rng ((F _E) * (W1 .edgeSeq())) )

assume
y in (F _E) .: (W1 .edges())
; :: thesis: 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;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

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