let K be Field; :: thesis: for p being FinSequence of K holds (1_ K) * p = p
let p be FinSequence of K; :: thesis: (1_ K) * p = p
A1: dom p = Seg (len p) by FINSEQ_1:def 3;
A2: ( Seg (len ((1_ K) * p)) = Seg (len p) & dom ((1_ K) * p) = Seg (len ((1_ K) * p)) ) by FINSEQ_1:def 3, MATRIXR1:16;
for i being Nat st i in dom p holds
((1_ K) * p) . i = p . i

proof

let i be Nat; :: thesis: ( i in dom p implies ((1_ K) * p) . i = p . i )
A3: rng p c= the carrier of K by FINSEQ_1:def 4;
assume A4: i in dom p ; :: thesis: ((1_ K) * p) . i = p . i
then A5: p . i in dom ( the multF of K [;] ((1_ K),(id the carrier of K))) by A2, A1, FUNCT_1:11;
p . i in rng p by A4, FUNCT_1:3;
then reconsider b = p . i as Element of K by A3;
((1_ K) * p) . i = ((1_ K) multfield) . (p . i) by A4, FUNCT_1:13
.= the multF of K . ((1_ K),((id the carrier of K) . (p . i))) by A5, FUNCOP_1:32
.= (1_ K) * b
.= p . i ;
hence ((1_ K) * p) . i = p . i ; :: thesis: verum

end;

hence (1_ K) * p = p by A2, A1, FINSEQ_1:13; :: thesis: verum