let n be Nat; :: thesis: for X being non empty set
for f being Function st f = (Seg n) --> X holds
f is non-empty n -element FinSequence
let X be non empty set ; :: thesis: for f being Function st f = (Seg n) --> X holds
f is non-empty n -element FinSequence
let f be Function; :: thesis: ( f = (Seg n) --> X implies f is non-empty n -element FinSequence )
assume A1: f = (Seg n) --> X ; :: thesis: f is non-empty n -element FinSequence
card f = card (dom f) by CARD_1:62;
then card f = card (Seg n) by A1, FUNCOP_1:13;
then card f = card n by FINSEQ_1:55;
hence f is non-empty n -element FinSequence by A1, CARD_1:def 7; :: thesis: verum