reconsider f = F _V , g = F _E as one-to-one Function ;

let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis: ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) & ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 implies e DJoins v,w,G2 )

assume ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) ) ; :: thesis: ( not ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 or e DJoins v,w,G2 )

then A1: ( e in rng g & v in rng f & w in rng f ) by FUNCT_1:33;

then consider e0 being object such that

A2: ( e0 in dom g & g . e0 = e ) by FUNCT_1:def 3;

consider v0 being object such that

A3: ( v0 in dom f & f . v0 = v ) by A1, FUNCT_1:def 3;

consider w0 being object such that

A4: ( w0 in dom f & f . w0 = w ) by A1, FUNCT_1:def 3;

assume ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 ; :: thesis: e DJoins v,w,G2

then (g ") . (g . e0) DJoins (f ") . (f . v0),w0,G1 by A2, A3, A4, FUNCT_1:34;

then (g ") . (g . e0) DJoins v0,w0,G1 by A3, FUNCT_1:34;

then e0 DJoins v0,w0,G1 by A2, FUNCT_1:34;

hence e DJoins v,w,G2 by A2, A3, A4, Th16; :: thesis: verum

let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis: ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) & ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 implies e DJoins v,w,G2 )

assume ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) ) ; :: thesis: ( not ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 or e DJoins v,w,G2 )

then A1: ( e in rng g & v in rng f & w in rng f ) by FUNCT_1:33;

then consider e0 being object such that

A2: ( e0 in dom g & g . e0 = e ) by FUNCT_1:def 3;

consider v0 being object such that

A3: ( v0 in dom f & f . v0 = v ) by A1, FUNCT_1:def 3;

consider w0 being object such that

A4: ( w0 in dom f & f . w0 = w ) by A1, FUNCT_1:def 3;

assume ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 ; :: thesis: e DJoins v,w,G2

then (g ") . (g . e0) DJoins (f ") . (f . v0),w0,G1 by A2, A3, A4, FUNCT_1:34;

then (g ") . (g . e0) DJoins v0,w0,G1 by A3, FUNCT_1:34;

then e0 DJoins v0,w0,G1 by A2, FUNCT_1:34;

hence e DJoins v,w,G2 by A2, A3, A4, Th16; :: thesis: verum