let n be Nat; :: thesis: for i1, i2 being Nat st 1 <= i1 & i1 <= n & 1 <= i2 & i2 <= n & Base_FinSeq n,i1 = Base_FinSeq n,i2 holds
i1 = i2
let i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 <= n & 1 <= i2 & i2 <= n & Base_FinSeq n,i1 = Base_FinSeq n,i2 implies i1 = i2 )
assume A1: ( 1 <= i1 & i1 <= n & 1 <= i2 & i2 <= n & Base_FinSeq n,i1 = Base_FinSeq n,i2 ) ; :: thesis: i1 = i2
then (Base_FinSeq n,i1) . i1 = 1 by MATRIXR2:75;
hence i1 = i2 by A1, MATRIXR2:76; :: thesis: verum