take NAT --> ((the_Edges_of G) --> 0) ; :: thesis: for n being Nat holds (NAT --> ((the_Edges_of G) --> 0)) . n is FF:ELabeling of G
let n be Nat; :: thesis: (NAT --> ((the_Edges_of G) --> 0)) . n is FF:ELabeling of G
n in NAT by ORDINAL1:def 12;
hence (NAT --> ((the_Edges_of G) --> 0)) . n is FF:ELabeling of G by FUNCOP_1:7; :: thesis: verum