Theorem frexr

Description: A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypothesis	frexr.1	|- ( ph -> F : A --> RR )
Assertion	frexr	|- ( ph -> F : A --> RR* )

Proof

Step	Hyp	Ref	Expression
1		frexr.1	|- ( ph -> F : A --> RR )
2		ressxr	|- RR C_ RR*
3	2	a1i	|- ( ph -> RR C_ RR* )
4	1 3	fssd	|- ( ph -> F : A --> RR* )