deffunc H_{1}( object ) -> set = {} ;

consider f being ManySortedSet of NAT such that

A1: for i being object st i in NAT holds

f . i = H_{1}(i)
from PBOOLE:sch 4();

take f ; :: thesis: for i being Nat holds f . i is PartFunc of (the_Vertices_of G),NAT

let i be Nat; :: thesis: f . i is PartFunc of (the_Vertices_of G),NAT

i in NAT by ORDINAL1:def 12;

then f . i = {} by A1;

hence f . i is PartFunc of (the_Vertices_of G),NAT by RELSET_1:12; :: thesis: verum

consider f being ManySortedSet of NAT such that

A1: for i being object st i in NAT holds

f . i = H

take f ; :: thesis: for i being Nat holds f . i is PartFunc of (the_Vertices_of G),NAT

let i be Nat; :: thesis: f . i is PartFunc of (the_Vertices_of G),NAT

i in NAT by ORDINAL1:def 12;

then f . i = {} by A1;

hence f . i is PartFunc of (the_Vertices_of G),NAT by RELSET_1:12; :: thesis: verum