Theorem iswrddm0

Description: A function with empty domain is a word. (Contributed by AV, 13-Oct-2018)

	Ref	Expression
Assertion	iswrddm0	⊢ ( 𝑊 : ∅ ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		fzo0	⊢ ( 0 ..^ 0 ) = ∅
2	1	feq2i	⊢ ( 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 ↔ 𝑊 : ∅ ⟶ 𝑆 )
3		iswrdi	⊢ ( 𝑊 : ( 0 ..^ 0 ) ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )
4	2 3	sylbir	⊢ ( 𝑊 : ∅ ⟶ 𝑆 → 𝑊 ∈ Word 𝑆 )