let G be _Graph; :: thesis: rng H₅(G) = union H₈(G)

now :: thesis: for y being object holds
( ( y in union H₈(G) implies ex x being object st
( x in dom H₅(G) & y = H₅(G) . x ) ) & ( ex x being object st
( x in dom H₅(G) & y = H₅(G) . x ) implies y in union H₈(G) ) )

let y be object ; :: thesis: ( ( y in union H₈(G) implies ex x being object st
( x in dom H₅(G) & y = H₅(G) . x ) ) & ( ex x being object st
( x in dom H₅(G) & y = H₅(G) . x ) implies b₁ in union H₈(G) ) )

hereby :: thesis: ( ex x being object st
( x in dom H₅(G) & y = H₅(G) . x ) implies b₁ in union H₈(G) )

assume y in union H₈(G) ; :: thesis: ex x being object st
( x in dom H₅(G) & y = H₅(G) . x )
then consider Y being set such that
A1: ( y in Y & Y in H₈(G) ) by TARSKI:def 4;
consider v being Vertex of G such that
A2: ( Y = H₆(G,v) \/ H₇(G,v) & not v is isolated ) by A1;
thus ex x being object st
( x in dom H₅(G) & y = H₅(G) . x ) :: thesis: verum

proof

per cases ( y in H₆(G,v) or y in H₇(G,v) ) by A1, A2, XBOOLE_0:def 3;

suppose y in H₆(G,v) ; :: thesis: ex x being object st
( x in dom H₅(G) & y = H₅(G) . x )

then consider v0, e0, y0 being object such that
A3: ( v0 in {v} & e0 in v .edgesOut() & y0 in {0} & y = [v0,e0,y0] ) by MCART_1:68;
take [e0,0] ; :: thesis: ( [e0,0] in dom H₅(G) & y = H₅(G) . [e0,0] )
A4: ( e0 in the_Edges_of G & 0 in {0,1} ) by A3, TARSKI:def 2;
dom H₅(G) = [:(the_Edges_of G),{0,1}:] by Lm9;
hence [e0,0] in dom H₅(G) by A4, ZFMISC_1:def 2; :: thesis: y = H₅(G) . [e0,0]
A5: y0 = 0 by A3, TARSKI:def 1;
( dom H₃(G) = [:(the_Edges_of G),{0}:] & dom H₄(G) = [:(the_Edges_of G),{1}:] ) by Lm5;
then A6: [e0,0] in dom H₃(G) by A3, A5, ZFMISC_1:def 2;
A7: dom H₁(G) = the_Edges_of G by Lm4;
v0 = v by A3, TARSKI:def 1;
then A8: (the_Source_of G) . e0 = v0 by A3, GLIB_000:58;
A9: dom (the_Source_of G) = the_Edges_of G by FUNCT_2:def 1;
A10: ( dom (id (the_Edges_of G)) = the_Edges_of G & dom (id {0}) = {0} ) ;
A11: dom H₃(G) misses dom H₄(G) by Lm6;
thus y = [[v0,e0],0] by A3, A5, XTUPLE_0:def 4
.= [[((the_Source_of G) . e0),((id (the_Edges_of G)) . e0)],0] by A4, A8, FUNCT_1:18
.= [(H₁(G) . e0),0] by A4, A9, A10, FUNCT_3:49
.= [(H₁(G) . e0),((id {0}) . y0)] by A3, A5, FUNCT_1:18
.= H₃(G) . (e0,y0) by A3, A7, A10, FUNCT_3:def 8
.= H₃(G) . [e0,0] by A5, BINOP_1:def 1
.= H₅(G) . [e0,0] by A6, A11, FUNCT_4:16 ; :: thesis: verum

end;

suppose y in H₇(G,v) ; :: thesis: ex x being object st
( x in dom H₅(G) & y = H₅(G) . x )

then consider v1, e1, y1 being object such that
A12: ( v1 in {v} & e1 in v .edgesIn() & y1 in {1} & y = [v1,e1,y1] ) by MCART_1:68;
take [e1,1] ; :: thesis: ( [e1,1] in dom H₅(G) & y = H₅(G) . [e1,1] )
A13: ( e1 in the_Edges_of G & 1 in {0,1} ) by A12, TARSKI:def 2;
dom H₅(G) = [:(the_Edges_of G),{0,1}:] by Lm9;
hence [e1,1] in dom H₅(G) by A13, ZFMISC_1:def 2; :: thesis: y = H₅(G) . [e1,1]
A14: y1 = 1 by A12, TARSKI:def 1;
( dom H₃(G) = [:(the_Edges_of G),{0}:] & dom H₄(G) = [:(the_Edges_of G),{1}:] ) by Lm5;
then A15: [e1,1] in dom H₄(G) by A12, A14, ZFMISC_1:def 2;
A16: dom H₂(G) = the_Edges_of G by Lm4;
v1 = v by A12, TARSKI:def 1;
then A17: (the_Target_of G) . e1 = v1 by A12, GLIB_000:56;
A18: dom (the_Target_of G) = the_Edges_of G by FUNCT_2:def 1;
A19: ( dom (id (the_Edges_of G)) = the_Edges_of G & dom (id {1}) = {1} ) ;
thus y = [[v1,e1],1] by A12, A14, XTUPLE_0:def 4
.= [[((the_Target_of G) . e1),((id (the_Edges_of G)) . e1)],1] by A13, A17, FUNCT_1:18
.= [(H₂(G) . e1),1] by A13, A18, A19, FUNCT_3:49
.= [(H₂(G) . e1),((id {1}) . y1)] by A12, A14, FUNCT_1:18
.= H₄(G) . (e1,y1) by A12, A16, A19, FUNCT_3:def 8
.= H₄(G) . [e1,1] by A14, BINOP_1:def 1
.= H₅(G) . [e1,1] by A15, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

end;

given x being object such that A20: ( x in dom H₅(G) & y = H₅(G) . x ) ; :: thesis: b₁ in union H₈(G)
x in [:(the_Edges_of G),{0,1}:] by A20, Lm9;
then consider e, z being object such that
A21: ( e in the_Edges_of G & z in {0,1} & x = [e,z] ) by ZFMISC_1:def 2;

per cases ( z = 0 or z = 1 ) by A21, TARSKI:def 2;

suppose A22: z = 0 ; :: thesis: b₁ in union H₈(G)

then A23: ( z in {0} & z in dom (id {0}) ) by TARSKI:def 1;
A24: dom H₁(G) = the_Edges_of G by Lm4;
A25: ( dom (id (the_Edges_of G)) = the_Edges_of G & dom (the_Source_of G) = the_Edges_of G ) by FUNCT_2:def 1;
[e,z] in [:(the_Edges_of G),{0}:] by A21, A23, ZFMISC_1:def 2;
then ( [e,z] in dom H₃(G) & dom H₃(G) misses dom H₄(G) ) by Lm5, Lm6;
then A26: y = H₃(G) . [e,z] by A20, A21, FUNCT_4:16
.= H₃(G) . (e,z) by BINOP_1:def 1
.= [(H₁(G) . e),((id {0}) . z)] by A21, A23, A24, FUNCT_3:def 8
.= [(H₁(G) . e),z] by A23, FUNCT_1:18
.= [[((the_Source_of G) . e),((id (the_Edges_of G)) . e)],0] by A21, A22, A25, FUNCT_3:49
.= [[((the_Source_of G) . e),e],0] by A21, FUNCT_1:18
.= [((the_Source_of G) . e),e,0] by XTUPLE_0:def 4 ;
(the_Source_of G) . e in rng (the_Source_of G) by A21, A25, FUNCT_1:3;
then reconsider v = (the_Source_of G) . e as Vertex of G ;
A27: ( v in {v} & e in v .edgesOut() ) by A21, GLIB_000:58, TARSKI:def 1;
then A28: not v is isolated by GLIB_000:155;
[v,e,0] in H₆(G,v) by A22, A23, A27, MCART_1:69;
then A29: y in H₆(G,v) \/ H₇(G,v) by A26, XBOOLE_0:def 3;
H₆(G,v) \/ H₇(G,v) in H₈(G) by A28;
hence y in union H₈(G) by A29, TARSKI:def 4; :: thesis: verum

end;

suppose A30: z = 1 ; :: thesis: b₁ in union H₈(G)

then A31: ( z in {1} & z in dom (id {1}) ) by TARSKI:def 1;
A32: dom H₂(G) = the_Edges_of G by Lm4;
A33: ( dom (id (the_Edges_of G)) = the_Edges_of G & dom (the_Target_of G) = the_Edges_of G ) by FUNCT_2:def 1;
[e,z] in [:(the_Edges_of G),{1}:] by A21, A31, ZFMISC_1:def 2;
then [e,z] in dom H₄(G) by Lm5;
then A34: y = H₄(G) . [e,z] by A20, A21, FUNCT_4:13
.= H₄(G) . (e,z) by BINOP_1:def 1
.= [(H₂(G) . e),((id {1}) . z)] by A21, A31, A32, FUNCT_3:def 8
.= [(H₂(G) . e),z] by A31, FUNCT_1:18
.= [[((the_Target_of G) . e),((id (the_Edges_of G)) . e)],1] by A21, A30, A33, FUNCT_3:49
.= [[((the_Target_of G) . e),e],1] by A21, FUNCT_1:18
.= [((the_Target_of G) . e),e,1] by XTUPLE_0:def 4 ;
(the_Target_of G) . e in rng (the_Target_of G) by A21, A33, FUNCT_1:3;
then reconsider v = (the_Target_of G) . e as Vertex of G ;
A35: ( v in {v} & e in v .edgesIn() ) by A21, GLIB_000:56, TARSKI:def 1;
then A36: not v is isolated by GLIB_000:155;
[v,e,1] in H₇(G,v) by A30, A31, A35, MCART_1:69;
then A37: y in H₆(G,v) \/ H₇(G,v) by A34, XBOOLE_0:def 3;
H₆(G,v) \/ H₇(G,v) in H₈(G) by A36;
hence y in union H₈(G) by A37, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence rng H₅(G) = union H₈(G) by FUNCT_1:def 3; :: thesis: verum