let n be Element of NAT ; 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; 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 ; ( 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 )
; (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; verum