deffunc H₁( object ) -> set = {} ;
consider f being ManySortedSet of NAT such that
A1: for i being object st i in NAT holds
f . i = H₁(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