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

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