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