let x be Element of (product <*G1,G2*>); :: thesis: x is FinSequence-like
reconsider y = x as Element of product (Carrier <*G1,G2*>) by Def2;
y is FinSequence-like ;
hence x is FinSequence-like ; :: thesis: verum