let IT1, IT2 be FinSequence; :: thesis: ( len IT1 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) ) & len IT2 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len IT2 holds
IT2 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) ) implies IT1 = IT2 )
assume that
A2: ( len IT1 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) ) ) and
A3: ( len IT2 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len IT2 holds
IT2 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) ) ) ; :: thesis: IT1 = IT2

now

let n be Nat; :: thesis: ( 1 <= n & n <= len IT1 implies IT1 . n = IT2 . n )
assume A4: ( 1 <= n & n <= len IT1 ) ; :: thesis: IT1 . n = IT2 . n
hence IT1 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) by A2
.= IT2 . n by A2, A3, A4 ;
:: thesis: verum

end;

hence IT1 = IT2 by A2, A3, FINSEQ_1:18; :: thesis: verum