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