H: dom r = the carrier of F by defr;
then reconsider e = r . (1. F) as Element of rng r by FUNCT_1:3;
reconsider o = r . (0. F) as Element of rng r by H, FUNCT_1:3;
take doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) ; :: thesis: ( the carrier of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = rng r & the addF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = ren_add r & the multF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = ren_mult r & the OneF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = r . (1. F) & the ZeroF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = r . (0. F) )
thus ( the carrier of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = rng r & the addF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = ren_add r & the multF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = ren_mult r & the OneF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = r . (1. F) & the ZeroF of doubleLoopStr(# (rng r),(ren_add r),(ren_mult r),e,o #) = r . (0. F) ) ; :: thesis: verum