set L = the MCS:Labeling of G;
deffunc H₁( 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₁(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