let G be _Graph; :: thesis: rng H₃(G) misses rng H₄(G)
assume rng H₃(G) meets rng H₄(G) ; :: thesis: contradiction
then consider z being object such that
A1: ( z in rng H₃(G) & z in rng H₄(G) ) by XBOOLE_0:3;
consider z0 being object such that
A2: ( z0 in dom H₃(G) & H₃(G) . z0 = z ) by A1, FUNCT_1:def 3;
consider z1 being object such that
A3: ( z1 in dom H₄(G) & H₄(G) . z1 = z ) by A1, FUNCT_1:def 3;
z0 in [:(the_Edges_of G),{0}:] by A2, Lm5;
then consider x0, y0 being object such that
A4: ( x0 in the_Edges_of G & y0 in {0} & z0 = [x0,y0] ) by ZFMISC_1:def 2;
z1 in [:(the_Edges_of G),{1}:] by A3, Lm5;
then consider x1, y1 being object such that
A5: ( x1 in the_Edges_of G & y1 in {1} & z1 = [x1,y1] ) by ZFMISC_1:def 2;
A6: ( x0 in dom H₁(G) & y0 in dom (id {0}) ) by A4, Lm4;
A7: ( x1 in dom H₂(G) & y1 in dom (id {1}) ) by A5, Lm4;
A8: [(H₁(G) . x0),((id {0}) . y0)] = H₃(G) . (x0,y0) by A6, FUNCT_3:def 8
.= z by A2, A4, BINOP_1:def 1
.= H₄(G) . (x1,y1) by A3, A5, BINOP_1:def 1
.= [(H₂(G) . x1),((id {1}) . y1)] by A7, FUNCT_3:def 8 ;
A9: ( y0 = 0 & y1 = 1 ) by A4, A5, TARSKI:def 1;
then 0 = (id {0}) . y0 by A4, FUNCT_1:18
.= (id {1}) . y1 by A8, XTUPLE_0:1
.= 1 by A5, A9, FUNCT_1:18 ;
hence contradiction ; :: thesis: verum