let i be natural Number ; :: thesis: for D being non empty set
for q being FinSequence
for f being sequence of D st q = f | (Seg i) holds
len q = i
let D be non empty set ; :: thesis: for q being FinSequence
for f being sequence of D st q = f | (Seg i) holds
len q = i
let q be FinSequence; :: thesis: for f being sequence of D st q = f | (Seg i) holds
len q = i
let f be sequence of D; :: thesis: ( q = f | (Seg i) implies len q = i )
reconsider i = i as Element of NAT by ORDINAL1:def 12;
dom (f | (Seg i)) = Seg i by FUNCT_2:def 1;
hence ( q = f | (Seg i) implies len q = i ) by FINSEQ_1:def 3; :: thesis: verum