for i, j being object st i in dom (n |-> a) & j in dom (n |-> a) holds
(n |-> a) . i = (n |-> a) . j

proof

let i, j be object ; :: thesis: ( i in dom (n |-> a) & j in dom (n |-> a) implies (n |-> a) . i = (n |-> a) . j )
assume A1: ( i in dom (n |-> a) & j in dom (n |-> a) ) ; :: thesis: (n |-> a) . i = (n |-> a) . j
reconsider i = i as Nat by A1;
reconsider j = j as Nat by A1;
dom (n |-> a) = Seg (len (n |-> a)) by FINSEQ_1:def 3;
then ( (n |-> a) . i = a & (n |-> a) . j = a ) by A1, FINSEQ_2:57;
hence (n |-> a) . i = (n |-> a) . j ; :: thesis: verum

end;

hence n |-> a is constant by FUNCT_1:def 10; :: thesis: verum