let i be Nat; :: thesis: for D being non empty set
for q being FinSequence
for f being Function of NAT ,D st q = f | (Seg i) holds
len q = i
let D be non empty set ; :: thesis: for q being FinSequence
for f being Function of NAT ,D st q = f | (Seg i) holds
len q = i
let q be FinSequence; :: thesis: for f being Function of NAT ,D st q = f | (Seg i) holds
len q = i
let f be Function of NAT ,D; :: thesis: ( q = f | (Seg i) implies len q = i )
reconsider i = i as Element of NAT by ORDINAL1:def 13;
f | (Seg i) is Function of (Seg i),D by FUNCT_2:38;
then 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