let n be Element of NAT ; :: thesis: for K being Field
for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
(1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j
let K be Field; :: thesis: for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds
(1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= n & 1 <= j & j <= n implies (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j )
assume that
A1: ( 1 <= i & i <= n ) and
A2: ( 1 <= j & j <= n ) ; :: thesis: (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j
[i,j] in Indices (1. (K,n)) by A1, A2, MATRIX_0:31;
then ex p3 being FinSequence of K st
( p3 = (1. (K,n)) . i & (1. (K,n)) * (i,j) = p3 . j ) by MATRIX_0:def 5;
hence (1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j by A1, Th26; :: thesis: verum