let a be FinSequence of NAT ; :: thesis: ( a = n |-> i iff ( len a = n & ( for j being Element of NAT st 1 <= j & j <= n holds
a . j = i ) ) )

hereby :: thesis: ( len a = n & ( for j being Element of NAT st 1 <= j & j <= n holds
a . j = i ) implies a = n |-> i )

assume A1: a = n |-> i ; :: thesis: ( len a = n & ( for j being Element of NAT st 1 <= j & j <= n holds
a . j = i ) )
hence len a = n by CARD_1:def 7; :: thesis: for j being Element of NAT st 1 <= j & j <= n holds
a . j = i
thus for j being Element of NAT st 1 <= j & j <= n holds
a . j = i :: thesis: verum

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j <= n implies a . j = i )
assume ( 1 <= j & j <= n ) ; :: thesis: a . j = i
then j in Seg n by FINSEQ_1:1;
hence a . j = i by A1, FUNCOP_1:7; :: thesis: verum

end;

end;

assume that
A2: len a = n and
A3: for j being Element of NAT st 1 <= j & j <= n holds
a . j = i ; :: thesis: a = n |-> i
A4: dom a = Seg n by A2, FINSEQ_1:def 3;

now

let z be set ; :: thesis: ( z in dom a implies a . z = i )
assume A5: z in dom a ; :: thesis: a . z = i
then reconsider z9 = z as Element of NAT ;
( 1 <= z9 & z9 <= n ) by A4, A5, FINSEQ_1:1;
hence a . z = i by A3; :: thesis: verum

end;

hence a = n |-> i by A4, FUNCOP_1:11; :: thesis: verum