reconsider S = the carrier of F as Subset of E by EC_PF_1:def 1;
H: F is Subring of E by FIELD_5:12;
B: ( 0. E = 0. F & 1. E = 1. F ) by EC_PF_1:def 1;

C: now :: thesis: for a, b being Element of E st a in S & b in S holds
( a + b in S & a * b in S & - a in S )

let a, b be Element of E; :: thesis: ( a in S & b in S implies ( a + b in S & a * b in S & - a in S ) )
assume ( a in S & b in S ) ; :: thesis: ( a + b in S & a * b in S & - a in S )
then reconsider x = a, y = b as Element of F ;
a + b = x + y by H, FIELD_6:15;
hence a + b in S ; :: thesis: ( a * b in S & - a in S )
a * b = x * y by H, FIELD_6:16;
hence a * b in S ; :: thesis: - a in S
- a = - x by H, FIELD_6:17;
hence - a in S ; :: thesis: verum

end;

now :: thesis: for a being non zero Element of E st a in S holds
a " in S

let a be non zero Element of E; :: thesis: ( a in S implies a " in S )
assume a in S ; :: thesis: a " in S
then reconsider x = a as Element of F ;
a " = x " by FIELD_6:18;
hence a " in S ; :: thesis: verum

end;

hence for b₁ being Subset of E st b₁ = the carrier of F holds
b₁ is inducing_subfield by B, C; :: thesis: verum