let p be FinSequence; :: thesis: for a being object holds
( p = (len p) |-> a iff for k being object st k in dom p holds
p . k = a )
let a be object ; :: thesis: ( p = (len p) |-> a iff for k being object st k in dom p holds
p . k = a )
thus ( p = (len p) |-> a implies for k being object st k in dom p holds
p . k = a ) :: thesis: ( ( for k being object st k in dom p holds
p . k = a ) implies p = (len p) |-> a )

proof

assume A2: p = (len p) |-> a ; :: thesis: for k being object st k in dom p holds
p . k = a
let k be object ; :: thesis: ( k in dom p implies p . k = a )
assume k in dom p ; :: thesis: p . k = a
then k in Seg (len p) by FINSEQ_1:def 3;
hence p . k = a by A2, FINSEQ_2:57; :: thesis: verum

end;

assume for k being object st k in dom p holds
p . k = a ; :: thesis: p = (len p) |-> a
then p = (dom p) --> a by FUNCOP_1:11;
hence p = (len p) |-> a by FINSEQ_1:def 3; :: thesis: verum