set L = the MCS:Labeling of G;

deffunc H_{1}( object ) -> MCS:Labeling of G = the MCS:Labeling of G;

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 n being Nat holds f . n is MCS:Labeling of G

let n be Nat; :: thesis: f . n is MCS:Labeling of G

n in NAT by ORDINAL1:def 12;

hence f . n is MCS:Labeling of G by A1; :: thesis: verum

deffunc H

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 n being Nat holds f . n is MCS:Labeling of G

let n be Nat; :: thesis: f . n is MCS:Labeling of G

n in NAT by ORDINAL1:def 12;

hence f . n is MCS:Labeling of G by A1; :: thesis: verum