deffunc H₁( Nat) -> set = (the_Weight_of G) . ((W .edgeSeq()) . $1);
consider IT being FinSequence such that
A1: ( len IT = len (W .edgeSeq()) & ( for k being Nat st k in dom IT holds
IT . k = H₁(k) ) ) from FINSEQ_1:sch 2();
take IT ; :: thesis: ( len IT = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len IT holds
IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) )
thus len IT = len (W .edgeSeq()) by A1; :: thesis: for n being Nat st 1 <= n & n <= len IT holds
IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n)
let n be Nat; :: thesis: ( 1 <= n & n <= len IT implies IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) )
assume ( 1 <= n & n <= len IT ) ; :: thesis: IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n)
then n in dom IT by FINSEQ_3:25;
hence IT . n = (the_Weight_of G) . ((W .edgeSeq()) . n) by A1; :: thesis: verum