let L1 be non empty doubleLoopStr ; :: thesis: L1,L1 are_isomorphic
take id L1 ; :: according to QUOFIELD:def 26 :: thesis: id L1 is RingIsomorphism
thus id L1 is RingHomomorphism ; :: according to QUOFIELD:def 23,QUOFIELD:def 24 :: thesis: ( id L1 is one-to-one & id L1 is RingEpimorphism )
thus id L1 is one-to-one ; :: thesis: id L1 is RingEpimorphism
thus id L1 is RingHomomorphism ; :: according to QUOFIELD:def 22 :: thesis: K840(the carrier of L1,the carrier of L1,(id L1)) = the carrier of L1
thus rng (id L1) = [#] L1 by TOPGRP_1:1
.= the carrier of L1 ; :: thesis: verum