let n be non zero Nat; :: thesis: for f being Function
for X being n -element FinSequence st f in product X holds
f is n -element FinSequence
let f be Function; :: thesis: for X being n -element FinSequence st f in product X holds
f is n -element FinSequence
let X be n -element FinSequence; :: thesis: ( f in product X implies f is n -element FinSequence )
assume A1: f in product X ; :: thesis: f is n -element FinSequence
A2: dom X = Seg n by FINSEQ_1:89;
then dom f = Seg n by A1, CARD_3:9;
then reconsider f = f as FinSequence by FINSEQ_1:def 2;
dom f is n -element by A1, A2, CARD_3:9;
then card (dom f) = n by CARD_1:def 7;
then card f = n by CARD_1:62;
hence f is n -element FinSequence by CARD_1:def 7; :: thesis: verum