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()) and
A3: for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) and
A4: len IT2 = len (W .edgeSeq()) and
A5: for n being Nat st 1 <= n & n <= len IT2 holds
IT2 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ; :: thesis: IT1 = IT2
now :: thesis: for n being Nat st 1 <= n & n <= len IT1 holds
IT1 . n = IT2 . n
let n be Nat; :: thesis: ( 1 <= n & n <= len IT1 implies IT1 . n = IT2 . n )
assume A6: ( 1 <= n & n <= len IT1 ) ; :: thesis: IT1 . n = IT2 . n
hence IT1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) by A3
.= IT2 . n by A2, A4, A5, A6 ;
:: thesis: verum
end;
hence IT1 = IT2 by A2, A4, FINSEQ_1:14; :: thesis: verum