let F be Field; :: thesis: doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) is Subfield of F
set G = doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #);
( the addF of doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) = the addF of F || the carrier of doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) & the multF of doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) = the multF of F || the carrier of doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) & 1. F = 1. doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) & 0. F = 0. doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) ) ;
hence doubleLoopStr(# the carrier of F, the addF of F, the multF of F, the OneF of F, the ZeroF of F #) is Subfield of F by EC_PF_1:def 1; :: thesis: verum