Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
RealsStruct
x0
.
Apply Field_of_RealsStruct_2f with
x0
,
λ x1 x2 :
ι →
ι → ι
.
∀ x3 x4 .
x4
∈
omega
⟶
CRing_with_id_omega_exp
(
Field_of_RealsStruct
x0
)
x3
(
ordsucc
x4
)
=
x1
x3
(
CRing_with_id_omega_exp
(
Field_of_RealsStruct
x0
)
x3
x4
)
leaving 2 subgoals.
The subproof is completed by applying H0.
Apply CRing_with_id_omega_exp_S with
Field_of_RealsStruct
x0
.
Apply Field_of_RealsStruct_is_CRing_with_id with
x0
.
The subproof is completed by applying H0.
■