A: the carrier of (f . 0) in { the carrier of (f . i) where i is Element of NAT : verum } ;
reconsider o = 1. (f . 0) as Element of Carrier f by A, TARSKI:def 4;
reconsider z = 0. (f . 0) as Element of Carrier f by A, TARSKI:def 4;
take doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) ; :: thesis: ( the carrier of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = Carrier f & the addF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = addseq f & the multF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = multseq f & the OneF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = 1. (f . 0) & the ZeroF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = 0. (f . 0) )
thus ( the carrier of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = Carrier f & the addF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = addseq f & the multF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = multseq f & the OneF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = 1. (f . 0) & the ZeroF of doubleLoopStr(# (Carrier f),(addseq f),(multseq f),o,z #) = 0. (f . 0) ) ; :: thesis: verum