consider L being MCS:Labeling of G;
deffunc H₁( set ) -> MCS:Labeling of G = L;
consider f being ManySortedSet of such that
A: for i being set 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 13;
hence f . n is MCS:Labeling of G by A; :: thesis: verum