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

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