let L1 be non empty doubleLoopStr ; :: thesis: R86(L1,L1)
take id L1 ; :: according to QUOFIELD:def 23 :: thesis: id L1 is RingIsomorphism
thus id L1 is RingHomomorphism ; :: according to MOD_4:def 8,MOD_4:def 12 :: thesis: ( id L1 is one-to-one & id L1 is V32( the carrier of L1) )
thus id L1 is one-to-one ; :: thesis: id L1 is V32( the carrier of L1)
thus rng (id L1) = [#] L1 by TOPGRP_1:1
.= the carrier of L1 ; :: according to FUNCT_2:def 3 :: thesis: verum