let X be non-empty FinSequence; :: thesis: for x being set st x in product X holds
x is FinSequence
let x be set ; :: thesis: ( x in product X implies x is FinSequence )
assume x in product X ; :: thesis: x is FinSequence
then consider g being Function such that
A1: ( x = g & dom g = dom X & ( for i being object st i in dom X holds
g . i in X . i ) ) by CARD_3:def 5;
dom g = Seg (len X) by A1, FINSEQ_1:def 3;
hence x is FinSequence by A1, FINSEQ_1:def 2; :: thesis: verum