Theorem psr1basf

Description: Univariate power series base set elements are functions. (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypotheses	psr1rcl.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
	psr1rcl.b	$$⊢B={\mathrm{Base}}_P$$
	psr1basf.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	psr1basf	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$

Proof

Step	Hyp	Ref	Expression
1		psr1rcl.p	$$⊢P={\mathrm{PwSer}}_1\left(R\right)$$
2		psr1rcl.b	$$⊢B={\mathrm{Base}}_P$$
3		psr1basf.k	$$⊢K={\mathrm{Base}}_R$$
4		elmapi	$$⊢F\in \left(K^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}\right)\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$
5	1 2 3	psr1bas	$$⊢B=K^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}$$
6	4 5	eleq2s	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶K$$