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