consider L being LexBFS:Labeling of G;
deffunc H₁( set ) -> LexBFS:Labeling of G = L;
consider f being ManySortedSet of NAT such that
A1: 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 LexBFS:Labeling of G
let n be Nat; :: thesis: f . n is LexBFS:Labeling of G
n in NAT by ORDINAL1:def 13;
hence f . n is LexBFS:Labeling of G by A1; :: thesis: verum