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_1:38;
then ex p3 being FinSequence of K st
( p3 = (1. K,n) . i & (1. K,n) * i,j = p3 . j ) by MATRIX_1:def 6;
hence (1. K,n) * i,j = (Base_FinSeq K,n,i) . j by A1, Th26; :: thesis: verum