let a be Complex; :: thesis: for f being FinSequence
for k being Nat st k in dom f holds
((len f) |-> a) . k = a
let f be FinSequence; :: thesis: for k being Nat st k in dom f holds
((len f) |-> a) . k = a
let k be Nat; :: thesis: ( k in dom f implies ((len f) |-> a) . k = a )
assume k in dom f ; :: thesis: ((len f) |-> a) . k = a
then ( len f >= k & k >= 1 ) by FINSEQ_3:25;
then k in Seg (len f) ;
hence ((len f) |-> a) . k = a by FINSEQ_2:57; :: thesis: verum