let x be Element of dom <*G*>; :: according to GLIB_000:def 67 :: thesis: <*G*> . x is loopless
x in dom <*G*> ;
then x in Seg 1 by FINSEQ_1:def 8;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <*G*> . x is loopless ; :: thesis: verum