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