Theorem seq1i

Description: Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypotheses	seq1i.1	|- M e. ZZ
	seq1i.2	|- ( ph -> ( F ` M ) = A )
Assertion	seq1i	|- ( ph -> ( seq M ( .+ , F ) ` M ) = A )

Proof

Step	Hyp	Ref	Expression
1		seq1i.1	|- M e. ZZ
2		seq1i.2	|- ( ph -> ( F ` M ) = A )
3		seq1	|- ( M e. ZZ -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
4	1 3	ax-mp	|- ( seq M ( .+ , F ) ` M ) = ( F ` M )
5	4 2	syl5eq	|- ( ph -> ( seq M ( .+ , F ) ` M ) = A )