let D be non empty set ; :: thesis: for a being Element of D
for m being non zero Nat
for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
let a be Element of D; :: thesis: for m being non zero Nat
for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
let m be non zero Nat; :: thesis: for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
let g be FinSequence of D; :: thesis: ( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )

hereby :: thesis: ( g = m |-> a implies ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) )

assume that
A1: len g = m and
A2: for i being Nat st i in dom g holds
g . i = a ; :: thesis: g = m |-> a
( dom g = dom (m |-> a) & ( for i being Nat st i in dom g holds
g . i = (m |-> a) . i ) )

proof

thus dom g = Seg m by A1, FINSEQ_1:def 3
.= dom (m |-> a) by FUNCOP_1:13 ; :: thesis: for i being Nat st i in dom g holds
g . i = (m |-> a) . i
let i be Nat; :: thesis: ( i in dom g implies g . i = (m |-> a) . i )
assume A3: i in dom g ; :: thesis: g . i = (m |-> a) . i
A4: i in Seg m by A1, A3, FINSEQ_1:def 3;
thus g . i = a by A2, A3
.= (m |-> a) . i by A4, FINSEQ_2:57 ; :: thesis: verum

end;

hence g = m |-> a by FINSEQ_1:13; :: thesis: verum

end;

assume A5: g = m |-> a ; :: thesis: ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) )
then dom g = Seg m by FUNCOP_1:13;
hence ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) by A5, CARD_1:def 7, FINSEQ_2:57; :: thesis: verum