set A = the addF of S;
set M = the multF of S;
reconsider P = rng f as Preserv of the addF of S by T3;
reconsider R = rng f as Preserv of the multF of S by T4;
reconsider O = 1. S as Element of P by T1;
reconsider Z = 0. S as Element of P by T0;
reconsider MP = the multF of S || R as BinOp of P ;
take doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) ; :: thesis: ( the carrier of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = rng f & the addF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = the addF of S || (rng f) & the multF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = the multF of S || (rng f) & the OneF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = 1. S & the ZeroF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = 0. S )
thus ( the carrier of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = rng f & the addF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = the addF of S || (rng f) & the multF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = the multF of S || (rng f) & the OneF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = 1. S & the ZeroF of doubleLoopStr(# P,( the addF of S || P),MP,O,Z #) = 0. S ) ; :: thesis: verum