let x be Element of product (Carrier <*G1*>); :: thesis: x is FinSequence-like
take 1 ; :: according to FINSEQ_1:def 2 :: thesis: proj1 x = Seg 1
thus dom x = dom (Carrier <*G1*>) by CARD_3:9
.= Seg 1 by FINSEQ_1:2, PARTFUN1:def 2 ; :: thesis: verum