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 A1: ( 1 <= i & i <= n & 1 <= j & j <= n ) ; :: thesis: (1. K,n) * i,j = (Base_FinSeq K,n,i) . j
then [i,j] in Indices (1. K,n) by 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, AA1200; :: thesis: verum