let R1, R2, R3 be Ring; :: thesis: ( R1 == R2 & R2 == R3 implies R1 == R3 )
assume ( R1 == R2 & R2 == R3 ) ; :: thesis: R1 == R3
then ( doubleLoopStr(# the carrier of R1, the addF of R1, the multF of R1, the OneF of R1, the ZeroF of R1 #) = doubleLoopStr(# the carrier of R2, the addF of R2, the multF of R2, the OneF of R2, the ZeroF of R2 #) & doubleLoopStr(# the carrier of R2, the addF of R2, the multF of R2, the OneF of R2, the ZeroF of R2 #) = doubleLoopStr(# the carrier of R3, the addF of R3, the multF of R3, the OneF of R3, the ZeroF of R3 #) ) by FIELD_7:def 1;
hence R1 == R3 by FIELD_7:def 1; :: thesis: verum