let X be set ; :: thesis: for fs being FinSequence of X
for fss being Subset of fs
for m being Element of NAT st m in dom (Seq fss) holds
ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fs be FinSequence of X; :: thesis: for fss being Subset of fs
for m being Element of NAT st m in dom (Seq fss) holds
ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fss be Subset of fs; :: thesis: for m being Element of NAT st m in dom (Seq fss) holds
ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let m be Element of NAT ; :: thesis: ( m in dom (Seq fss) implies ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n ) )

set f = Sgm (dom fss);
set n = (Sgm (dom fss)) . m;
consider k being Nat such that
A1: dom fss c= Seg k by FINSEQ_1:def 12;
assume A2: m in dom (Seq fss) ; :: thesis: ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )

then A3: m in dom (fss * (Sgm (dom fss))) by FINSEQ_1:def 14;
then A4: (Sgm (dom fss)) . m in dom fss by FUNCT_1:11;
Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;
then (Seq fss) . m = fss . ((Sgm (dom fss)) . m) by ;
then A5: [((Sgm (dom fss)) . m),((Seq fss) . m)] in fss by ;
then A6: (Sgm (dom fss)) . m in dom fs by FUNCT_1:1;
A7: m in dom (Sgm (dom fss)) by ;
A8: (Seq fss) . m = fs . ((Sgm (dom fss)) . m) by ;
k in NAT by ORDINAL1:def 12;
hence ex n being Element of NAT st
( n in dom fs & m <= n & (Seq fss) . m = fs . n ) by ; :: thesis: verum