1. F <> x by Def2;
then not 1. F in {x} by TARSKI:def 1;
then 1. F in ([#] F) \ {x} by XBOOLE_0:def 5;
then reconsider e = 1. F as Element of carr (x,o) by XBOOLE_0:def 3;
0. F <> x by Def2;
then not 0. F in {x} by TARSKI:def 1;
then 0. F in ([#] F) \ {x} by XBOOLE_0:def 5;
then reconsider u = 0. F as Element of carr (x,o) by XBOOLE_0:def 3;
take doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) ; :: thesis: ( the carrier of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = carr (x,o) & the addF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = addR (x,o) & the multF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = multR (x,o) & the OneF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = 1. F & the ZeroF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = 0. F )
thus ( the carrier of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = carr (x,o) & the addF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = addR (x,o) & the multF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = multR (x,o) & the OneF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = 1. F & the ZeroF of doubleLoopStr(# (carr (x,o)),(addR (x,o)),(multR (x,o)),e,u #) = 0. F ) ; :: thesis: verum