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