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