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